NanoProof：Lean 4 中开放且高效的自动定理证明

arXiv:2610.11605v1 公告类型：新 摘要：我们推出了 NanoProof，据我们所知，这是 Lean 4 中首个因子化执行引导式定理证明器，其训练数据、提取工具、训练流程和权重均已发布，因此可使用开源资源实现端到端复现。为此，我们构建并发布了一个结构化证明树数据集，以及一个用于在 Lean 4 形式化验证器中进行程序化交互和数据提取的工具。为支持可持续研究，我们专注于计算效率，以促进易于获取的训练与评估。NanoProof 在 MiniF2F-Test 上达到 50.8% 的 pass@16，其性能超过同类中最接近的两个系统 HyperTree Proof Search 和 ABEL，而所需计算量约分别少 90 倍和 7 倍；与 AlphaProof 相比，所需计算量则少了四个数量级以上。虽然存在更强的开放权重定理证明器，但它们都是基于大型预训练语言模型进行微调的，且既不发布训练数据，也不发布训练流程；NanoProof 表明，因子化执行引导式定理证明器这一类别可以利用适度资源从头重建。