ITPEval：交互式定理证明器间形式化翻译基准测试

英文标题：ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

ITPEval 是一项面向交互式定理证明器之间形式化翻译的基准测试工作。该研究指出，形式化定理证明是机器学习的重要前沿挑战，但当前生态系统高度碎片化，证明内容分散在彼此不兼容的系统中。系统间不兼容限制了基于学习的证明器可用训练数据的规模，也削弱了已验证证明的可移植性。该基准有望为跨证明器转换能力的评估，以及更可复用的形式化验证工具链提供参考。

2.1 KB 640 B 612 B 380 B 9.1 KB 32.7 KB 22.8 KB 24.2 KB 34.7 KB