让AI智能体翻译网络，而非对网络进行推理

形式化模型使验证可达性、定位中断故障或预判一次变更的影响半径成为可能。然而几乎没有生产网络拥有这样的模型，因为手工编写模型需要稀缺的专业知识，而且在网络频繁变化时难以保持最新。从本质上看，网络建模是一项“誊写式”工作：它把网络工件（如配置、拓扑和路由状态）翻译成形式逻辑中的规则。这类翻译正是当今大语言模型（LLM）擅长之事。与自由形式的AI推理不同，这种翻译可以被形式化验证。一旦建模不再是瓶颈，再让AI去对大型复杂网络做推理就说不过去了。因此，我们的立场与当前让自主AI智能体端到端负责的竞赛相悖。我们转而把AI限定于翻译，并依靠求解器完成可靠的长程推理：先构建一个关于一般网络行为的可复用形式化模型，再将其特化到具体任务，例如根因分析（RCA）。我们构建了TypoNet，它从网络自身的工件出发构建并验证一个生产规模WAN仿真环境的符号模型。初步评估显示TypoNet在两方面有帮助。就其本身而言，TypoNet比LLM更快、更便宜且更可靠地回答运维问题（如可达性验证与变更影响分析）。作为AI智能体的工具，TypoNet以更低成本增强故障定位。这一结果为如下路线提供了论据：让AI构建可验证的网络模型，并依靠求解器完成可靠的长程推理。