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 低逾四个数量级。
正文 · 原文
Abstract:We introduce NanoProof, to our knowledge the first factorized execution-guided theorem prover in Lean 4 whose training data, extraction tooling, training pipeline, and weights are all released, making it end-to-end reproducible using open-source resources. To this end, we build and release a dataset of structured proof trees, as well as a tool for programmatic interaction and data extraction within the Lean 4 formal verifier. To support sustainable research, we focus on compute efficiency to facilitate accessible training and evaluation. NanoProof achieves 50.8% pass@16 on MiniF2F-Test, exceeding the two closest systems of its class, HyperTree Proof Search and ABEL, at roughly 90x and 7x less compute, and using more than four orders of magnitude less compute than AlphaProof. Stronger open-weight provers exist, but they are fine-tuned from large pretrained language models and release neither training data nor pipeline; NanoProof shows that the factorized execution-guided class of provers can be rebuilt from scratch with modest resources.
| Comments: | 18 pages, 8 figures. Code: this https URL |
| Subjects: | Machine Learning (cs.LG); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.11605 [cs.LG] |
| (or arXiv:2610.11605v1 [cs.LG] for this version) | |
| https://doi.org/10.48550/arXiv.2610.11605 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Matěj Kripner [view email]
[v1]
Thu, 8 Oct 2026 09:49:39 UTC (486 KB)
来源：arXiv cs.AI · arxiv.org