一种形式化模型可支持验证连通性、定位故障或预估变更的影响范围（blast radius）。然而，几乎没有任何生产网络具备此类模型，因为手工编写模型需要稀缺的专业知识，且难以随网络频繁变更而持续更新。本质上，网络建模是一项排版式（typographical）任务：它将网络制品（例如配置、拓扑与路由状态）翻译为形式逻辑中的规则。此类翻译正是当前大语言模型（LLM）所擅长的任务。与自由形式的 AI 推理不同，此类翻译可被形式化验证。一旦建模不再成为瓶颈，便无需再依赖 AI 对大规模复杂网络执行端到端推理。因此，本文立场与当前主流趋势——即竞相部署全自主 AI Agent——截然相反。我们主张将 AI 限定于翻译任务，而将可靠、长时程的推理交由求解器（solver）完成，并构建一个可复用的通用网络行为形式化模型，再针对具体任务（如根因分析，RCA）进行特化。为此，我们构建了 TypoNet，它能基于网络自身的制品，构建并验证一个符号化模型，该模型对应于仿真环境下的生产级广域网（WAN）。初步评估表明，TypoNet 在两方面带来提升：其一，独立运行时，TypoNet 在回答运维问题（如连通性验证与变更影响分析）上，比 LLM 更快、更廉价且更可靠；其二，作为 AI Agent 的工具，TypoNet 能以更低开销提升故障定位能力。本工作论证了这样一种 AI 范式：构建可验证的网络模型，并依托求解器实现可靠的长时程推理。

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.