Formal（形式化方法）指用严格的数学语言和机器可验证的语法来描述、推导和检验系统行为的技术路线，涵盖形式语言、形式语法验证与形式数学证明等方向。随着大语言模型能力提升，formal 方法的价值被重新审视：它为 AI 生成的代码和证明提供了可执行、可核验的判定标准，成为连接生成能力与可靠性保障的关键桥梁。
Formal 定理证明的快速跃升
形式数学证明（formal theorem proving）是近期进展最集中的方向。据 AI Will 报道，Google LEAP 项目将通用大语言模型的形式数学证明成功率从 10% 提升至 70%，这种量级的提升显示通用模型在无需大量领域专用数据的情况下也能胜任严格证明任务。配套的研究也在基础设施层面展开：Lean Graph Search for Formal Theorem Proving 通过图搜索结构改进了在 Lean 4 证明环境中的检索与推导路径；IneqAgent: Agentic Inequality Proving in Lean with Symbolic Computation 则结合智能体循环与符号计算，专门攻克不等式类证明。这些工作共同表明，LLM 与形式验证器的闭环协作正成为主流范式。
形式化向运行时验证与代码生成延伸
formal 思路也在向安全关键场景迁移。Formal, Executable and Explainable Runtime Monitoring of Spoken Air Traffic Control Operational Procedures 探索对空管口语操作规程进行可执行、可解释的运行时形式监控，说明形式方法能够约束自然语言驱动的实际系统。在代码生成侧，WoFT：结合形式语法验证与结构学习的代码生成新范式 将形式语法验证嵌入生成流程，用结构先验降低模型输出的语法与语义错误率。
理论溯源与建模融合的新探索
讨论也回到了理论源头。David Ha 提及 Schmidhuber 在 2009 年提出的"趣味与创造力形式理论"再度引发讨论，试图为内在动机给出形式化刻画。建模层面，TANGO: Token-Aggregated Nonlinear Gating Operators for Natural and Formal Language Modeling 来自 Google DeepMind，尝试在统一架构中同时建模自然语言与形式语言，反映两条语言形态趋于融合的趋势。
当前焦点与观察点
当前的争议与观察点集中在三处：其一，形式证明成功率的大幅提升（如从 10% 到 70%）是否依赖对训练评测数据的隐性拟合，仍需独立基准检验；其二，Lean 等证明助手生态的可扩展性问题，Erdős-Selfridge 类经典难题的形式化排除工作（如 Lean 4 形式化排除：lcm 超过 10000）提示部分问题的形式化成本依旧高昂；其三，formal 验证能否在 ARC Prize 等面向通用推理的评测体系中扮演裁判角色，值得关注后续 ARC Prize Research Summit 2026 的讨论走向。总体看，formal 方法正从学术工具演变为 AI 可靠性工程的基础组件。