超越库：面向研究数学自动形式化的智能体框架

虽然大型语言模型 (LLM) 在数学推理方面表现出了卓越的能力，但它们经常会产生难以察觉的细微错误。像 Lean 4 这样的形式数学语言提供了机械证明检查，强烈激发了对自动形式化的需求：将自然语言数学自动翻译成可验证的代码。最近的趋势表明，针对标准编程进行了大量优化的通用大语言模型现在的表现优于针对Lean明确微调的较小模型。利用这一转变，我们引入了 *Theo*，这是一个由通用编码 LLM 提供支持的代理自动形式化框架。我们系统的核心是一个协调器，它管理为研究级数学量身定制的多代理管道。由于前沿研究经常依赖于 Mathlib 等现有库范围之外的概念，因此我们的系统动态扩展必要的类型定义，并在形式化主要定理之前通过新颖的辅助引理技术对其进行验证。我们将我们的方法应用于 PutnamBench，为 32 个问题的随机样本生成经过机器检查的Lean证明。此外，我们还根据七篇研究论文（其中五篇来自 ACM 计算理论研讨会 (STOC)）和最近的两篇 OpenAI 手稿（涵盖组合学、通信复杂性、机制设计、学习理论、数论、离散几何和图论）评估了我们的系统。我们成功地形式化了他们的主要定理和证明，并与人类专家验证了生成的形式化；值得注意的是，两项发展不需要超出Lean核心的公理。我们所有的形式化都可以在 https://beyondthelibrary.github.io/formal_arxiv/ 上找到。