arXiv cs.AI· Mat\v{e}j Kripner, Milan Straka·· 9 天前AI 评分33
NanoProof：开源高效的 Lean 4 自动定理证明器
NanoProof: Open and Efficient Automated Theorem Proving in Lean 4
AI 导读
NanoProof 是首个完全开源的因子化执行引导定理证明器，训练数据、提取工具、训练流程与权重全部公开，可在 Lean 4 中端到端复现。它在 MiniF2F-Test 上取得 50.8% pass@16，算力消耗比 HyperTree Proof Search 和 ABEL 分别低约 90 倍和 7 倍，比 AlphaProof 低逾四个数量级。
正文 · AI 翻译
摘要：我们推出 NanoProof，据我们所知，这是 Lean 4 中首个分解式执行引导定理证明器，其训练数据、提取工具、训练流程和权重均已发布，使其能够使用开源资源实现端到端复现。为此，我们构建并发布了一个结构化证明树数据集，以及一个用于在 Lean 4 形式化验证器内进行程序化交互和数据提取的工具。为支持可持续研究，我们专注于计算效率，以促进可及的训练和评估。NanoProof 在 MiniF2F-Test 上达到 50.8% pass@16，超越同类中最接近的两个系统 HyperTree Proof Search 和 ABEL，计算量分别约少 90 倍和 7 倍，且使用的计算量比 AlphaProof 少四个数量级以上。存在更强的开放权重证明器，但它们是从大型预训练语言模型微调而来，既不发布训练数据也不发布流程；NanoProof 表明，分解式执行引导类证明器可以用适度的资源从零重建。
| 评论： | 18 页，8 幅图。代码：此 https URL |
| 主题： | 机器学习（cs.LG）；人工智能（cs.AI） |
| 引用为： | arXiv:2610.11605 [cs.LG] |
| （或 arXiv:2610.11605v1 [cs.LG] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.11605 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Matěj Kripner [查看电子邮件]
[v1]
2026 年 10 月 8 日星期四 09:49:39 UTC（486 KB）
来源：arXiv cs.AI · arxiv.org