从单条定理到完整理论库：自动形式化的新拐点

导语

自动形式化（Autoformalization）一直被视为连接自然语言数学、程序验证与机器证明的重要桥梁。过去许多研究更关注一个相对清晰的任务：把一句非形式化的命题，翻译成 Lean、Coq、Isabelle 等形式系统能够检查的表达。然而，arXiv 新论文《Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases》认为，这种“单句级”视角并不足以覆盖真实的形式化工作。

作者提出的核心观点是：真正有价值的自动形式化，应从孤立陈述转向“理论级”构建。也就是说，AI 不只是翻译某个目标定理，而是帮助建立一整套包含定义、公理、引理、命题及其相互依赖关系的结构化库。

核心要点

• 形式化不是单点翻译：在真实数学或程序语言理论中，一个定理往往必须依赖大量预备定义和中间结论。没有这些上下文，目标命题甚至无法被准确表述。
• 理论库才是可复用资产：单个形式化结果的价值有限，而成体系的知识库可以被后续证明、教学、验证工具和自动推理系统反复调用。
• 任务边界需要重新定义：如果目标变成“形式化完整理论”，模型就需要处理命名规范、模块组织、依赖图、概念一致性和库内复用等问题。
• 评估方式也要升级：只检查某条翻译是否通过类型检查，无法衡量整个理论库是否结构合理、覆盖充分、可维护或便于扩展。
• 作者提出未来路径：论文作为立场性文章，梳理了该方向的重要性、不同观点、开放挑战，并提出若干可推进理论级自动形式化的研究路线。

意义与影响

这一转向的意义在于，它把自动形式化从“语言转换任务”推向“知识工程任务”。对 AI for Science 而言，未来模型若能协助把教材、论文或领域文档转化为可验证的形式化库，就可能加速数学知识整理、科学理论验证和高可靠软件开发。

同时，这也提醒研究者：大模型在形式化领域的瓶颈不只在语法正确率，还在长期上下文、抽象层次、依赖管理和与现有库的衔接能力。理论级自动形式化更接近人类专家的工作流，也更能检验 AI 是否真正理解一个领域的结构。

当然，这篇论文并非宣布某个系统已经解决了问题，而是提出研究议程。它的价值在于把社区注意力从“翻译一条定理”引向“构建统一、可验证、可扩展的形式知识基础”。如果这一方向成熟，自动形式化可能成为科学知识数字化的重要基础设施。

来源：arXiv