EvolProver: 対称性と難易度を活用した形式化問題の進化による自動定理証明の推進

EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty

October 1, 2025

著者: Yuchen Tian, Ruiyuan Huang, Xuanwu Wang, Jing Ma, Zengfeng Huang, Ziyang Luo, Hongzhan Lin, Da Zheng, Lun Du

cs.AI

要旨

形式的定理証明における大規模言語モデル（LLMs）は大きな可能性を示しているものの、一般化能力に欠け、問題文の些細な変更に対しても脆弱であることが多い。この制限に対処するため、我々はモデルの頑健性を対称性と難易度の2つの観点から向上させる新しいデータ拡張パイプラインを提案する。対称性の観点から、構文的対称性を対象として意味的に等価な問題変種を生成するAbstract Syntax Tree（AST）ベースの手法であるEvolASTと、LLMsを活用して数学的領域間で定理を翻訳することで意味的対称性に対処するEvolDomainという2つの補完的な手法を提案する。難易度の観点からは、慎重に設計された進化的指示を用いてLLMsを導き、より広範な難易度の新しい定理を生成するEvolDifficultyを提案する。その後、進化させたデータを用いて、7Bパラメータの非推論型定理証明器であるEvolProverを訓練する。EvolProverは、FormalMATH-Liteにおいて53.8%のpass@32率を達成し、推論ベースのモデルを含む同規模のすべてのモデルを凌駕し、新たなstate-of-the-art（SOTA）を確立した。また、MiniF2F-Test（69.8% pass@32）、Ineq-Comp-Seed（52.2% pass@32）、Ineq-Comp-Transformed（34.0% pass@32）においても、非推論型モデルとして新たなSOTA記録を樹立した。アブレーション研究は、複数のベンチマークにおいて我々のデータ拡張パイプラインの有効性をさらに裏付けるものである。

English

Large Language Models (LLMs) for formal theorem proving have shown significant promise, yet they often lack generalizability and are fragile to even minor transformations of problem statements. To address this limitation, we introduce a novel data augmentation pipeline designed to enhance model robustness from two perspectives: symmetry and difficulty. From the symmetry perspective, we propose two complementary methods: EvolAST, an Abstract Syntax Tree (AST) based approach that targets syntactic symmetry to generate semantically equivalent problem variants, and EvolDomain, which leverages LLMs to address semantic symmetry by translating theorems across mathematical domains. From the difficulty perspective, we propose EvolDifficulty, which uses carefully designed evolutionary instructions to guide LLMs in generating new theorems with a wider range of difficulty. We then use the evolved data to train EvolProver, a 7B-parameter non-reasoning theorem prover. EvolProver establishes a new state-of-the-art (SOTA) on FormalMATH-Lite with a 53.8% pass@32 rate, surpassing all models of comparable size, including reasoning-based models. It also sets new SOTA records for non-reasoning models on MiniF2F-Test (69.8% pass@32), Ineq-Comp-Seed (52.2% pass@32), and Ineq-Comp-Transformed (34.0% pass@32). Ablation studies further confirm our data augmentation pipeline's effectiveness across multiple benchmarks.