arXiv:2502.04671v2 宣告类型: 替换 摘要：神经网络在交互式证明助手（ITPs）如Lean和Coq中的自动定理证明方面展现出了巨大的潜力。然而，大多数神经定理证明模型仅限于特定的ITPs，这限制了不同ITPs之间的跨语言迁移。我们通过一个名为${\rm P{\small ROOF}W{\small ALA}}$的多语言证明框架解决了这一问题，该框架允许神经定理证明器与两个已建立的ITPs（Coq和Lean）进行标准化交互。它能够收集多语言证明步骤数据——即在ITP状态上执行证明操作的结果数据——用于训练神经证明器。${\rm P{\small ROOF}W{\small ALA}}$允许通过高效并行证明搜索算法系统地评估模型在不同ITPs和问题领域中的性能。我们展示了${\rm P{\small ROOF}W{\small ALA}}$支持的多语言训练可以实现ITPs之间的成功迁移。具体来说，基于${\rm P{\small ROOF}W{\small ALA}}$生成的Coq和Lean数据的混合训练模型，在标准的prove-at-$k$指标上优于仅使用Coq或仅使用Lean的数据训练的模型。我们开源了所有代码，包括${\rm P{\small ROOF}W{\small ALA}}$框架的代码（https://github.com/trishullab/proof-wala）和多语言ITP交互框架的代码（https://github.com/trishullab/itp-interface）。