論文の概要: EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty

• arxiv url: http://arxiv.org/abs/2510.00732v1
• Date: Wed, 01 Oct 2025 10:15:27 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-03 16:59:20.507897
• Title: EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty
• Title（参考訳）: EvolProver: 対称性と難易度による形式的問題を進化させることによる自動定理証明の促進
• Authors: Yuchen Tian, Ruiyuan Huang, Xuanwu Wang, Jing Ma, Zengfeng Huang, Ziyang Luo, Hongzhan Lin, Da Zheng, Lun Du,
• Abstract要約: 形式定理の証明のための大規模言語モデル(LLM)は、しばしば一般化性に欠け、問題文の小さな変換にも脆弱である。 対称性と難易度という2つの観点からモデルロバスト性を高めるために設計された新しいデータ拡張パイプラインを導入する。 EvolProverは、FormalMATH-Lite上で53.8%のpass@32レートで新しい最先端(SOTA)を確立する。
• 参考スコア（独自算出の注目度）: 45.584089391538015
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.
• Abstract（参考訳）: 形式定理の証明のための大規模言語モデル(LLM)は大きな可能性を示しているが、しばしば一般化性に欠け、問題文の小さな変換にも脆弱である。 この制限に対処するために,対称性と難易度という2つの視点からモデルロバスト性を高めるために設計された,新しいデータ拡張パイプラインを導入する。 対称性の観点からは, 抽象構文木 (AST) をベースとした構文対称性を目標とする手法である EvolAST と, 数学的領域をまたいだ定理の翻訳により, LLM を利用して意味対称性に対処する EvolDomain の2つの相補的手法を提案する。 難易度の観点からは, LLMを誘導する進化的命令を慎重に設計し, より広い範囲の難易度で新たな定理を生成するEvolDifficultyを提案する。 次に、進化したデータを用いて、7Bパラメータの非推論定理証明器であるEvolProverを訓練する。 EvolProverは、FormalMATH-Lite上で53.8%パス@32レートで新しい最先端(SOTA)を確立する。 また、MiniF2F-Test(69.8% pass@32)、Ineq-Comp-Seed(52.2% pass@32)、Ineq-Comp-Transformed(34.0% pass@32)の非推論モデルのための新しいSOTAレコードも設定している。 アブレーション研究は、複数のベンチマークでデータ拡張パイプラインの有効性をさらに確認します。

関連論文リスト

• Long-Short Chain-of-Thought Mixture Supervised Fine-Tuning Eliciting Efficient Reasoning in Large Language Models [23.34070841541423]
  LS-Mixture SFT(Long-Short Chain-of-Thought Mixture Supervised Fine-Tuning)を提案する。 LS-Mixture SFTでトレーニングしたモデルと直接SFTでトレーニングしたモデルでは,平均精度が2.3%向上した。 この研究は、教師付き微調整によって推論能力を持つ非推論モデルを実現するアプローチを提供する。
  論文  参考訳（メタデータ） (2025-05-06T12:18:11Z)
• Self-Evolved Preference Optimization for Enhancing Mathematical Reasoning in Small Language Models [17.673293240849787]
  我々は、小言語モデル(SLM)における推論を強化する自己進化型データ生成パイプラインSPHEREを紹介する。 SPHEREは、 (i) 自己生成(Self-Generation)、 (ii) 自己補正(Self-Correction)、 (iii) 多様性誘導(diversity induction)、そして、複数の有効な推論軌道を通じて堅牢性を改善する。 本研究では,SPHERE学習モデルがベースバージョンよりも大幅に向上し,特定のベンチマークでGPT-4oにマッチすることを示す。
  論文  参考訳（メタデータ） (2025-03-04T14:43:25Z)
• OptMATH: A Scalable Bidirectional Data Synthesis Framework for Optimization Modeling [9.617742955894247]
  高品質な最適化モデリングデータセットの欠如は、大きな言語モデルを悩ませます。 本稿では,OptMATHという高品質なデータセットを合成するためのスケーラブルなフレームワークを提案する。 我々は,OptMATHでトレーニングした様々なサイズのモデルが,複数のモデリングベンチマークにおいて優れた結果が得られることを実証した。
  論文  参考訳（メタデータ） (2025-02-16T12:38:37Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• A Unified Approach to Learning Ising Models: Beyond Independence and Bounded Width [7.605563562103568]
  我々はIsingモデルの基本パラメータをデータから効率的に学習する問題を再考する。 ノード単位のロジスティック回帰に基づく単純な既存手法が、いくつかの新しい設定で基盤モデルの回復に成功していることを示す。
  論文  参考訳（メタデータ） (2023-11-15T18:41:19Z)
• FAENet: Frame Averaging Equivariant GNN for Materials Modeling [123.19473575281357]
  データ変換による任意のモデルE(3)-同変や不変化を実現するために,フレームアラグリング(SFA)に依存したフレキシブルなフレームワークを導入する。 本手法の有効性を理論的および実験的に証明し, 材料モデリングにおける精度と計算スケーラビリティを実証する。
  論文  参考訳（メタデータ） (2023-04-28T21:48:31Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。