Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
作者: Arshia Soltani Moakhar, Iman Gholami, Max Springer, Mahdi JafariRaviz, MohammadTaghi Hajiaghayi
分类: cs.AI
发布日期: 2026-07-05
💡 一句话要点
提出代理框架以实现研究数学的自动形式化
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自动形式化 数学推理 大型语言模型 Lean 4 多代理系统 辅助引理 研究级数学
📋 核心要点
- 现有的数学自动形式化方法常常无法处理研究级数学中的复杂概念，导致形式化结果的准确性和有效性不足。
- 本文提出的框架通过利用通用编码LLMs，动态扩展类型定义并验证，旨在提高自动形式化的准确性和效率。
- 实验结果表明，该方法在PutnamBench上成功生成了机器检查的Lean证明，并在五篇STOC论文中形式化了主要定理，验证了其有效性。
📝 摘要（中文）
尽管大型语言模型（LLMs）在数学推理方面表现出色，但它们常常会产生细微的错误，难以被人类发现。正式的数学语言如Lean 4提供了机械证明检查，强烈推动了自动形式化的需求，即将自然语言数学自动翻译为可验证的代码。本文提出了一种基于通用编码LLMs的代理自动形式化框架，核心是一个管理多代理管道的调度器，专为研究级数学设计。我们的系统动态扩展必要的类型定义，并通过新颖的辅助引理技术进行验证，随后再形式化主要定理。我们在PutnamBench上应用了该方法，为32个问题生成了机器检查的Lean证明，并在五篇ACM理论计算机科学研讨会论文上成功形式化了主要定理，所有形式化结果均可在线获取。
🔬 方法详解
问题定义：本文旨在解决现有自动形式化方法在处理复杂数学概念时的不足，尤其是在研究级数学中，现有库如Mathlib无法满足需求。
核心思路：通过引入一个调度器来管理多代理管道，利用通用编码LLMs的能力，动态扩展必要的类型定义并进行验证，从而实现高效的自动形式化。
技术框架：整体架构包括一个调度器、多个代理和一个验证模块。调度器负责协调各个代理的工作，代理则负责具体的形式化任务，验证模块则确保生成的形式化结果的正确性。
关键创新：最重要的创新在于引入了辅助引理技术，能够在形式化主要定理之前，动态验证扩展的类型定义，显著提高了形式化的准确性和可靠性。
关键设计：在参数设置上，系统能够根据具体问题动态调整类型定义，并采用了特定的损失函数来优化生成的代码质量，确保与Lean 4的兼容性。整体网络结构设计上，采用了多层次的代理机制，以便于处理复杂的数学推理任务。
🖼️ 关键图片
📊 实验亮点
实验结果显示，本文的方法在PutnamBench上成功生成了32个问题的机器检查Lean证明，并在五篇STOC论文中形式化了主要定理，所有形式化结果均得到了人类专家的验证。其中两篇定理的证明仅依赖于Lean的核心公理，显示出该方法的强大能力。
🎯 应用场景
该研究的潜在应用领域包括数学研究、教育和自动化证明系统。通过实现高效的自动形式化，能够帮助研究人员快速验证复杂的数学定理，提高研究效率，并为教育领域提供更为可靠的数学教学工具。未来，该框架有望在其他领域如计算机科学和工程中得到应用，推动相关领域的自动化发展。
📄 摘要（原文）
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 atthis https URL.