发表机构
Princeton University（普林斯顿大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究针对生产网络缺乏形式模型的问题，提出将人工智能局限于网络工件到形式逻辑规则的翻译，依靠求解器推理，构建TypoNet验证模拟广域网符号模型，能快速可靠回答操作问题及促进故障定位。
AI 中文摘要
形式模型有助于验证可达性、定位故障或预测变更的影响范围，但实际生产网络中几乎没有。手动编写模型需要稀缺专业知识且难以随网络变化更新。网络建模本质是将网络工件转换为形式逻辑规则，这是大语言模型擅长的，且可形式验证。我们反对让自主人工智能代理端到端负责，将人工智能局限于翻译，依靠求解器进行可靠的长期推理，构建通用网络行为的可重用形式模型并专门用于特定任务，如根本原因分析。我们构建了TypoNet，从网络工件构建并验证模拟生产规模广域网的符号模型。初步评估表明，TypoNet能更快、更便宜且更可靠地回答操作问题，作为人工智能代理工具能以更低成本促进故障定位。
英文摘要
A formal model enables verifying reachability, localizing an outage, or anticipating the blast radius of a change. Yet, virtually no production network has one, since writing a model by hand demands rare expertise and is hard to keep current as the network changes frequently. At its core, network modeling is a typographical exercise: it translates network artifacts (e.g., configurations, topology, and routing state) into rules in formal logic. Translation of this kind is what large language models (LLMs) nowadays do well. Unlike free-form AI reasoning, such translation can be formally verified. Once modeling is no longer the bottleneck, trusting AI to reason over large, complex networks no longer makes sense. Our position therefore cuts against the prevailing race to put autonomous AI agents in charge end-to-end. We instead confine AI to translation and rely on a solver for reliable long-horizon reasoning, building a reusable formal model of general network behavior that can then be specialized to specific tasks, e.g., root-cause analysis (RCA). We build TypoNet that constructs and validates a symbolic model of an emulated production-scale WAN from the network's own artifacts. Our preliminary evaluation shows TypoNet helps in two ways. On its own, TypoNet answers operational questions (e.g., reachability verification and change-impact analysis) faster, more cheaply, and more reliably than an LLM. As a tool for an AI agent, TypoNet boosts fault localization at lower cost. The result makes the case for AI that builds verifiable network models and relies on a solver for reliable long-horizon reasoning.
Comments8 pages, 3 figures, 1 table
