摘要
形式定理证明已成为机器学习的前沿挑战，但其生态系统仍然分散：证明在不兼容的系统之间孤立，限制了基于学习的证明器的训练数据和验证结果的可移植性。我们提出了ITPEval，这是第一个用于评估跨四个主要互动定理证明器（Lean 4、Rocq、Isabelle和HOL Light）自动形式证明翻译的基准测试，涵盖两个不同的逻辑基础。
我们的基准测试包含1,560个源文件和6,848个定理，分为控制层和生态系统层。控制层的公理化文件隔离了基础翻译的难度，而生态系统层则源于真实库，暴露了API和证明风格的不匹配。
我们发布了itpeval，这是一个统一的多互动定理证明器验证基础设施，具有状态隔离的温暖后端，保持每个工件的本地检查语义。我们评估了五个前沿和开放权重的LLM在12对定向翻译上的语句和证明翻译：语句翻译的通过率最高为29.1%，而证明翻译为10.5%；控制定理的证明通过率达到29.7%，而生态系统级翻译则为5.2%，确认库不匹配是主要瓶颈。
除了pass@k评估外，确定性Lean 4 BEq检查确认了54.0%的经过验证的源到Lean 4 miniF2F语句翻译的等价性，表明仅依靠本地类型检查可能大大高估语义的保真度。在自动形式化/自动非形式化的往返研究中，Rocq和HOL Light是比Lean 4和Isabelle更容易的形式化目标，而多互动定理证明器上下文将Lean 4的成功率从4.8%提高到10.6%。我们的基准测试、验证基础设施和评估管道均已公开发布。
博主点评： ITPEval的推出为形式定理证明的研究提供了重要的基准，尤其是其在不同逻辑基础之间的翻译能力评估。这不仅有助于推动相关领域的研究进展，也为未来的机器学习模型在形式验证中的应用提供了新的方向。通过对生态系统不匹配的深入分析，ITPEval将为提升模型的性能提供宝贵数据。