ITPEval：跨交互式定理证明器的形式化翻译基准

形式化定理证明已成为机器学习的前沿挑战，但生态系统碎片化：证明孤悬在不兼容的系统中，既限制学习型证明器的训练数据，也限制经验证结果的可移植性。我们提出ITPEval，首个评估跨四大ITP（Lean 4、Rocq、Isabelle与HOL Light）、横跨两种不同逻辑基础的自动形式化证明翻译的基准。基准含1,560个源文件与6,848个定理，组织为隔离基础翻译难度的受控层（公理化文件）与暴露API及证明风格错配的生态层（取自真实库）。我们发布itpeval——统一的多ITP验证基础设施，带状态隔离的暖后端，保留每工件的原生检查语义。我们在12个有向翻译对上评估五个前沿与开放权重LLM的陈述与证明翻译：陈述翻译峰值29.1% pass@1、证明翻译10.5%；受控定理达29.7%证明pass@1，对比生态级翻译的5.2%——确认库错配是主导瓶颈。此外，确定性Lean 4 BEq检查为54.0%的经验证源到Lean 4 miniF2F陈述翻译建立等价，表明仅原生类型检查会大幅高估语义保真；在自动形式化/自动非形式化的往返研究中，Rocq与HOL Light是比Lean 4与Isabelle更容易的形式化目标，而多ITP上下文把合并的Lean 4成功率从4.8%提高到10.6%。基准、验证基础设施与评估管线已公开。