論文の概要: SkillEvoLean: Mutation-enhanced skill evolution for Lean provers
- arxiv url: http://arxiv.org/abs/2610.01799v1
- Date: Thu, 01 Oct 2026 14:42:54 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-03 01:19:24.197656
- Title: SkillEvoLean: Mutation-enhanced skill evolution for Lean provers
- Title(参考訳): SkillEvoLean: リーンプロデューサのための変異によるスキル進化
- Abstract要約: スキル強化型リーンプローバー構築のための変異強化型スキル自己進化フレームワークを提案する。
我々は,MiniF2F,PatnamBench,2025 International Mathematical Olympiad (IMO 2025),および2026 USA Mathematical Olympiad (USAMO 2026)について検討した。
- 参考スコア(独自算出の注目度): 2.333676964568035
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Skill evolution offers a promising way to improve large language model agents without updating their parameters, but its use in formal theorem proving remains underexplored. Existing methods mainly target natural-language reasoning, improving skills by analyzing successful and failed trajectories and incrementally revising solving strategies. Although the Lean verifier provides reliable execution feedback, when all sampled trajectories fail, existing skill evolution methods lack successful trajectories from which to infer effective update directions. Furthermore, these methods also focus mainly on the root instruction file, thus underexploring the evolution of reference knowledge including mathematical concepts and proving techniques. To address these limitations, we propose a mutation-enhanced skill self-evolution framework for building skill-augmented Lean provers. The framework jointly evolves a high-level solving policy and its reference knowledge through progressive and mutation-based updates. Progressive evolution derives local improvements from successful and failed trajectories, while mutation is triggered when no complete proof can be generated, sampling mathematical concepts to produce and select new skill candidates under verifier feedback. We evaluate our method on MiniF2F, PutnamBench, the 2025 International Mathematical Olympiad (IMO 2025), and the 2026 USA Mathematical Olympiad (USAMO 2026). Under the same backbone model, trajectorysampling budget, and test-time compute, our method achieves proof success rates of 100.0%, 90.6%, 4/6, and 4/6, respectively, with GPT-5.5, outperforming the baseline methods. Further analysis shows that concept-guided mutation outperforms random-text-guided mutation by 6.9 and 8.2 percentage points on MiniF2F and PutnamBench, respectively, while solving one additional problem on both IMO 2025 and USAMO 2026.
- Abstract(参考訳): スキル進化は、パラメータを更新せずに大きな言語モデルエージェントを改善するための有望な方法を提供するが、公式な定理の証明での使用は未定のままである。
既存の手法は主に自然言語の推論を対象とし、成功と失敗の軌跡を分析してスキルを向上させること、問題解決戦略を漸進的に改訂することである。
リーン検証は、信頼できる実行フィードバックを提供するが、すべてのサンプルトラジェクトリが失敗した場合、既存のスキル進化手法には、効果的な更新方向を推測するための軌道が欠如している。
さらに、これらの手法は、主にルート命令ファイルに焦点を当てており、数学的概念や証明技術を含む参照知識の進化を過小評価している。
これらの制限に対処するため、我々は、スキル強化されたリーンプローバーを構築するための変異強化スキル自己進化フレームワークを提案する。
このフレームワークは、プログレッシブおよび突然変異ベースの更新を通じて、ハイレベルな解決ポリシーとその参照知識を共同で進化させる。
進歩的進化は、成功と失敗の軌跡から局所的な改善を導き、一方、完全証明が生成できないと突然変異が引き起こされ、数学的概念をサンプリングし、検証者フィードバックの下で新しいスキル候補を生成し、選択する。
我々は,MiniF2F,PatnamBench,2025 International Mathematical Olympiad (IMO 2025),および2026 USA Mathematical Olympiad (USAMO 2026)について検討した。
同じバックボーンモデル, 軌道サンプリング予算, テストタイム計算では, それぞれ100.0%, 90.6%, 4/6, 4/6の証明成功率をGPT-5.5で達成し, ベースライン法より優れていた。
さらに分析した結果、IMO 2025とUSAMO 2026において、概念誘導突然変異は、それぞれMiniF2FとPutnam Benchでランダムテキスト誘導突然変異を6.9と8.2のパーセンテージで上回った。
関連論文リスト
- Learning from Research: Toward Lifelong Agent Harness Evolution [25.703133924514884]
言語エージェントはますます複雑なタスクを解決することが期待されている。
有望なアプローチの1つは、ツールの使用、メモリ管理、タスク実行を管理するソフトウェアであるエージェントハーネスを進化させることである。
ScholarEvolveは、進化をガイドするための最先端の研究を自動的に引き出すフレームワークである。
論文 参考訳(メタデータ) (2026-09-30T17:00:38Z) - EvoGen-Harness: Learning Where and How to Evolve Image-Generation Harnesses [13.90368994038833]
EvoGen-Harnessは、マルチ責任画像生成のためのジェネレータに依存しないフレームワークである。
非パッチとホールドアウトのバリデーションは、不要または有害な更新を防ぐ。
GenEval2、T2I-CompBench++、WISE全体で、EvoGen-Harnessは、最も評価の高いベースラインを+0.2633、+0.0720、+0.0752で改善している。
論文 参考訳(メタデータ) (2026-09-30T09:30:52Z) - V-Gym: Enhancing Agentic Visual Reasoning via Skill-Data Co-Evolution [68.43599428916389]
V-Gymは、手続き的なスキルと実行軌跡からのマルチモーダルな実践データを反復的に進化させる、自律的なフレームワークである。
スキル進化の過程で、V-Gymは軌道を分析して階層的なスキルを蒸留し、洗練し、手続き的なガイダンスと適用性条件を更新する。
結果として得られた実践結果は、その後のスキル更新にフィードバックされ、継続的なスキル改善のループを閉じます。
論文 参考訳(メタデータ) (2026-09-28T09:09:24Z) - Self-Improving Large Language Models via Progressive Experience Evolution [52.03479747358687]
textbfSPEE(textbfSelf-textbfProgressive textbfExperience textbfEvolution)を提案する。
5つの数学的推論ベンチマークの実験は、SPEEが3つのモデルスケールでテスト時間とトレーニング時間の両方の自己進化ベースラインを一貫して上回っていることを示している。
論文 参考訳(メタデータ) (2026-08-03T12:27:32Z) - Escaping Confidence Trap: Evolutionary Decoding for Mathematical Reasoning in Diffusion LLMs [69.52853771994451]
我々はLLaDA 2.0の復号軌道を解析し、繰り返し拡散信頼トラップを同定する。
本稿では,拡散復号化を進化過程とみなす訓練不要なテスト時間スケーリングフレームワークである進化復号法を提案する。
論文 参考訳(メタデータ) (2026-08-01T11:48:25Z) - Teaching LLMs to Self-Evolve: Cultivating Core Meta-Skills with Reinforcement Learning [51.17262419591891]
AlphaEvolveが示すように、環境フィードバックによる反復的自己進化によるテスト時間のスケーリングは、顕著なパフォーマンス向上を示している。
本稿では,データ合成パイプライン,進化対応強化学習,推論時進化探索によるメタスキル開発を目的としたMetaEvolveを提案する。
論文 参考訳(メタデータ) (2026-07-24T04:35:29Z) - Beyond Static Evaluation: Co-Evolutionary Mechanisms for LLM-Driven Strategy Evolution in Adversarial Games [46.73592377177437]
評価器の共進化によって,ノイズの多い数ゲームスコアを統計的に信頼性のある評価に置き換える方法について述べる。
また,階層的な深層評価が,ノイズの多い数ゲームスコアを統計的に信頼性のある評価に置き換えることを示す。
FAMOU は OpenEvolve や ShinkaEvolve と同じ基盤モデル・コード進化パラダイム上に構築されたフレームワークである。
論文 参考訳(メタデータ) (2026-06-09T03:55:31Z) - Learning to Self-Evolve [37.39989112050656]
本稿では,LSE(Learning to Self-Evolve)について紹介する。LSE(Learning to Self-Evolve)は,大規模言語モデル(LLM)を学習して,テスト時に自身の状況を改善するための強化学習フレームワークである。
LSEは、マルチステップ進化問題を1ステップのRL目標に還元し、各コンテキストの編集は、下流のパフォーマンスの改善によって報われる。
本結果は,自己進化を学習可能なスキルとして扱うことの有効性を強調した。
論文 参考訳(メタデータ) (2026-03-19T08:41:24Z) - Outcome Accuracy is Not Enough: Aligning the Reasoning Process of Reward Models [108.26461635308796]
Rationale Consistencyは、モデルの推論プロセスと人間の判断のアライメントを定量化する、きめ細かい計量である。
我々のフロンティアモデルの評価では,最先端モデル間で合理的な一貫性が効果的に識別できることが示されている。
我々は、GenRMトレーニングの合理性一貫性と結果精度を組み合わせたハイブリッド信号を導入する。
論文 参考訳(メタデータ) (2026-02-04T15:24:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。