arXiv:2502.04671v1 新闻类型: 新 摘要: 神经网络在交互式证明助手（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 ProofWala\; Framework}$的代码，以及${\rm Multilingual\; ITP\; interaction\; framework}$的代码。