arXiv cs.AI· Tomas Ortega, Simon Park, Ayush Khaitan, Liam Fowl, Alex Kontorovich, Sanjeev Arora·· 3 天前AI 评分32
mini-Lean-agent：面向 Lean 的编码智能体基线，定理证明器需要定理证明智能体吗？
Do Theorem Provers Need Theorem-Proving Agents? mini-Lean-agent: A Coding-Agent Baseline for Lean
AI 导读
研究者提出 mini-Lean-agent，一个仅向模型暴露 bash 工具的极简 Lean 智能体，由独立可信评估器验证最终产物。
正文 · AI 翻译
摘要：通用编码智能体使用标准的 shell 和文件交互，而形式化定理证明智能体往往依赖专门的、临时性的工具。这使得人们难以确定定理证明智能体的哪些组件带来了基准测试性能提升：是改进的基础模型、专门的运行框架、特定的工具，还是其中任意几者的组合。我们提出 mini-Lean-agent，一个刻意保持极简的 Lean 任务智能体，其唯一对模型可见的工具是 bash。模型必须使用 bash 来检查和编辑代码库、搜索本地库、调用 Lean，并管理自己的中间工作，同时由一个独立的可信评估器验证最终产物。我们在 Putnam 2025 基准上比较 mini-Lean-agent 与 AxProverBase 和 Numina-Lean-Agent。以 Gemini 3.8 Flash 作为基础模型的实验表明，在每题 \$2 的成本限制下，mini-Lean-agent 解决了 7/12 道题，而 AxProverBase 为 4/12。以 Astra 作为基础模型时，mini-Lean-agent 解决了 12/12 道题，平均每题成本为 \$1.28。这表明，一个带有极简运行框架的通用编码智能体已经可以在 Lean 基准上取得强劲表现。我们的结果支持将 mini-Lean-agent 用作评估定理证明基础设施时的标准基线。
| 评论： | 被第 6 届数学推理与 AI 研讨会（NeurIPS 2026）接收 |
| 主题： | 人工智能（cs.AI）；计算机科学中的逻辑（cs.LO） |
| MSC 分类： | 68V15 |
| ACM 分类： | I.2.3; I.2.8; F.4.1 |
| 引用为： | arXiv:2610.17331 [cs.AI] |
| （或本版本使用 arXiv:2610.17331v1 [cs.AI]） | |
| https://doi.org/10.48550/arXiv.2610.17331 arXiv 通过 DataCite 颁发的 DOI（待注册） |
提交历史
来自：Tomàs Ortega [查看邮箱]
[v1]
2026 年 10 月 12 日星期一 19:40:30 UTC（35 KB）
来源：arXiv cs.AI · arxiv.org