Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
作者: Arshia Soltani Moakhar, Iman Gholami, Max Springer, Mahdi JafariRaviz, MohammadTaghi Hajiaghayi
分类: cs.AI
发布日期: 2026-06-30
备注: preprint
🔗 代码/项目: PROJECT_PAGE
💡 一句话要点
提出基于通用编码LLM的自动形式化框架以解决数学研究问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自动形式化 大型语言模型 数学证明 Lean 4 多代理系统 类型扩展 辅助引理技术
📋 核心要点
- 现有的数学形式化方法常常依赖于有限的库，难以处理前沿研究中的新概念，导致自动形式化的需求未能得到满足。
- 本文提出了一种代理自动形式化框架，利用通用编码LLM来管理多代理管道，动态扩展类型定义并验证，从而实现自然语言数学的自动形式化。
- 在实验中，我们成功为32个问题生成了机器检查的Lean证明，并在五篇论文中形式化了主要定理，验证了生成的形式化结果的有效性。
📝 摘要（中文）
尽管大型语言模型（LLMs）在数学推理方面表现出色，但它们常常会产生细微的错误，难以被人类发现。形式化数学语言如Lean 4提供机械证明检查，促使自动形式化的需求：将自然语言数学自动翻译为可验证代码。本文提出了一种基于通用编码LLM的代理自动形式化框架，核心是一个管理多代理管道的协调器，专为研究级数学设计。该系统动态扩展必要的类型定义，并通过新颖的辅助引理技术进行验证，最终实现主要定理的形式化。我们在PutnamBench上应用该方法，为32个问题生成机器检查的Lean证明，并在五篇ACM理论计算机科学研讨会论文中成功形式化主要定理，所有形式化结果均可在https://beyondthelibrary.github.io/formal_arxiv获取。
🔬 方法详解
问题定义：本文旨在解决现有数学形式化方法在处理新概念时的局限性，尤其是在前沿研究中，现有库如Mathlib无法满足需求。
核心思路：通过引入一个协调器来管理多代理管道，利用通用编码LLM的能力，动态扩展类型定义并进行验证，从而实现自然语言数学的自动形式化。
技术框架：整体架构包括一个协调器模块和多个代理模块，协调器负责管理流程，代理模块则执行具体的形式化任务。系统首先识别所需的类型定义，然后通过辅助引理技术进行验证，最后形式化主要定理。
关键创新：最重要的技术创新在于引入了动态类型扩展和辅助引理验证技术，使得系统能够处理超出现有库的数学概念，显著提升了自动形式化的能力。
关键设计：系统设计中，关键参数包括代理的数量和类型定义的扩展策略，损失函数则侧重于形式化结果的准确性与可验证性，确保生成的代码符合Lean 4的要求。
🖼️ 关键图片
📊 实验亮点
在实验中，我们成功为32个问题生成了机器检查的Lean证明，并在五篇ACM论文中形式化了主要定理，所有形式化结果均得到了人类专家的验证，显示出系统在形式化数学研究中的有效性和可靠性。
🎯 应用场景
该研究的潜在应用领域包括数学研究、教育和自动化证明系统。通过实现自然语言数学的自动形式化，能够帮助研究人员更高效地验证和传播数学知识，推动数学领域的进步。未来，该框架还可能扩展到其他形式化验证领域，提升自动化程度。
📄 摘要（原文）
While Large Language Models (LLMs) have demonstrated exceptional capabilities in mathematical reasoning, they frequently produce subtle errors that evade human detection. Formal mathematical languages like Lean 4 offer mechanical proof checking, strongly motivating the need for autoformalization: the automatic translation of natural language mathematics into verifiable code. Recent trends indicate that general-purpose LLMs, heavily optimized for standard programming, now outperform smaller models explicitly fine-tuned for Lean. Leveraging this shift, we introduce an agentic autoformalization framework powered by general coding LLMs. At the core of our system is an orchestrator that manages a multi-agent pipeline tailored for research-level mathematics. Because cutting-edge research frequently relies on concepts outside the scope of existing libraries like Mathlib, our system dynamically extends necessary type definitions and validates them via a novel Auxiliary Lemma technique before formalizing the primary theorems. We applied our approach to PutnamBench, producing machine-checked Lean proofs for a random sample of 32 problems. Furthermore, we evaluate our system on five papers from the ACM Symposium on Theory of Computing (STOC) spanning combinatorics, communication complexity, mechanism design, and learning theory, successfully formalizing their main theorems and validating the generated formalizations with human experts; for all five we also formalize the proofs alongside the statements, and notably two of them are proved with no axioms beyond Lean's kernel. All of our formalizations are available at https://beyondthelibrary.github.io/formal_arxiv .