EvolProver：通过对称性和难度演化来推进自动定理证明
人工智能
2025-10-02 v1
摘要
大型语言模型 (LLM) 用于形式定理证明显示出显著的潜力，但它们往往缺乏通用性，并且对问题陈述的 even 小小变换都十分脆弱。为了解决这一限制，我们引入一种新颖的数据增强管道，从两个角度增强模型的鲁棒性：对称性和难度。从对称性角度，我们提出两种互补方法：EvolAST，这是一种基于抽象语法树 (AST) 的方法，旨在针对语法对称性生成在语义上等价的问题变体；EvolDomain 利用 LLM 解决语义对称性，通过在数学领域之间转换定理。从难度角度，我们提出 EvolDifficulty，该方法使用精心设计的演化指令引导 LLM 生成更广泛难度范围的新定理。我们 then 使用演化后的数据训练 EvolProver，这是一个 7B 参数的非推理定理证明器。EvolProver 在 FormalMATH-Lite 上建立了新的最先进 (SOTA) 水平，达到 53.8% 的 pass@32 率，超越了所有规模相似的模型，包括推理-based 模型。它还在 MiniF2F-Test (69.8% pass@32)、Ineq-Comp-Seed (52.2% pass@32) 和 Ineq-Comp-Transformed (34.0% pass@32) 上为非推理模型设置了新的 SOTA 记录。进一步的消融研究确认了我们数据增强管道在多个基准测试中的有效性。
引用
@article{arxiv.2510.00732,
title = {EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty},
author = {Yuchen Tian and Ruiyuan Huang and Xuanwu Wang and Jing Ma and Zengfeng Huang and Ziyang Luo and Hongzhan Lin and Da Zheng and Lun Du},
journal= {arXiv preprint arXiv:2510.00732},
year = {2025}
}