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

我们介绍 NanoProof，据我们所知，Lean 4 中第一个因式分解执行引导定理证明器，其训练数据、提取工具、训练管道和权重均已发布，使其可以使用开源资源进行端到端重现。为此，我们构建并发布了结构化证明树的数据集，以及在 Lean 4 形式验证器中进行编程交互和数据提取的工具。为了支持可持续研究，我们专注于计算效率，以促进可访问的培训和评估。 NanoProof 在 MiniF2F-Test 上实现了 50.8% pass@16，超过了同类中最接近的两个系统 HyperTree Proof Search 和 ABEL，计算量分别减少了大约 90 倍和 7 倍，并且使用的计算量比 AlphaProof 减少了四个数量级以上。存在更强大的开放权重证明器，但它们是根据大型预训练语言模型进行微调的，并且既不发布训练数据也不发布管道； NanoProof 表明，分解执行引导的证明者类可以用适度的资源从头开始重建。