論文の概要: Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution

• arxiv url: http://arxiv.org/abs/2607.17352v1
• Date: Sun, 19 Jul 2026 17:26:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-21 18:48:37.435436
• Title: Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
• Title（参考訳）: 検証付きベンチマークによる自己修正型リーン証明エージェント
• Abstract要約: 私たちは、小さな固定ワークスペースが完全に変更可能な証明ワークフロー、プロンプト、ツールをラップする自己進化型のリーン実証エージェントを提示します。 固定された外部ベンチマークに対して最適化を行うほとんどの自己進化システムとは異なり、我々のシステムはエージェントとそのベンチマークを共進化させる。 最良の共進化剤は45.1%、種子は12.7%、固定ベンチマーク剤は32.0%に達する。
• 参考スコア（独自算出の注目度）: 20.44043749792232
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Designing effective Lean proof agents is a central challenge in formal mathematical reasoning. Beyond building stronger provers, recent work emphasizes the workflow around Lean: how an agent decomposes proof obligations, uses tools and compiler feedback, diagnoses failures, repairs proofs, and maintains structured proof context. Motivated by code-level self-evolving agents, we study whether such workflows can be evolved rather than hand-designed. We present a self-evolving Lean proof agent in which a small fixed, trusted runtime wraps a fully mutable workspace: the proof workflow, prompts, and tools. Unlike most self-evolving systems, which optimize against a fixed external benchmark, our system coevolves the agent and its benchmark. Between generations, the highest-scoring agent (the champion) revises the active task distribution through a mastery-throttled curriculum update that introduces harder proof obligations only after the current level is mastered, and a single-anchor recalibration re-runs the champion on the updated benchmark to keep scores comparable as difficulty rises. All evolution stays inside a Lean-grounded verification loop: however the agent rewrites itself, a success counts only when its behavior yields Lean-verified proofs under a trusted snapshot, and each attempt must emit a machine-readable, Lean-grounded proof context whose representation may evolve but whose groundedness is enforced. We run the coevolving trajectory and a fixed-benchmark baseline for 15 active generations and compare them on a held-out miniF2F test split. The best coevolving agent reaches a 45.1% held-out solve rate, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent, showing that verifier-grounded self-evolution can improve Lean proof workflows under a coevolving benchmark.
• Abstract（参考訳）: 効果的なリーン証明エージェントを設計することは、形式的な数学的推論における中心的な課題である。 エージェントが証明義務を分解し、ツールとコンパイラフィードバックを使用し、失敗を診断し、証明を修復し、構造化された証明コンテキストを維持する方法。 コードレベルの自己進化エージェントによって動機付けられ、そのようなワークフローが手作業で設計するよりも進化できるかどうかを研究する。 私たちは、小さな固定された信頼できるランタイムが完全に変更可能なワークスペース、すなわち証明ワークフロー、プロンプト、ツールをラップする自己進化型のリーン実証エージェントを提示します。 固定された外部ベンチマークに対して最適化を行うほとんどの自己進化システムとは異なり、我々のシステムはエージェントとそのベンチマークを共進化させる。 世代間、最高評価エージェント(チャンピオン)は、現在のレベルがマスタされた後にのみ、より厳しい証明義務を課すマスタースロットのカリキュラム更新を通じて、アクティブタスクの配布を更新し、シングルアンカーの校正により、更新されたベンチマーク上でチャンピオンを再実行し、難易度が上昇するにつれてスコアを同等に維持する。 エージェントは自分自身を書き換えるが、その振る舞いが信頼できるスナップショットの下でリーン検証された証明をもたらす場合に限り、成功はカウントされる。 共進化軌道と固定ベンチマークベースラインを15世代にわたって実行し, 保持したミニF2Fテストスプリットで比較した。 最高の共進化エージェントは45.1%の保留解決率に達し、種子は12.7%、固定ベンチマークエージェントは32.0%に達し、検証者による自己進化は共進化ベンチマークの下でリーンの証明ワークフローを改善できることを示した。

関連論文リスト

• HarnessEvolve: Learning from Reference Trajectories for Reliable Agent Self-Evolution [11.431479238875712]
  我々は、信頼できるエージェントの自己進化を実現するために、参照軌道から学習する自己進化フレームワークであるHarnessEvolveを紹介する。 私たちは、さまざまなモデルとエージェントフレームワークを使用して、オープンドメインとエンタープライズシナリオにまたがるいくつかのベンチマークで広範な実験を行います。 結果は、HarnessEvolveがすべてのベンチマークと設定で、最先端のベースラインを一貫して上回っていることを示している。
  論文  参考訳（メタデータ） (2026-09-01T07:31:18Z)
• TTHE: Test-Time Harness Evolution [50.26245555541721]
  既存のアプローチでは、デプロイ前、トレーニング前、あるいはテスト時に凍結される固定されたエージェントワークフローの開発データを最適化する。 我々は、エージェントがテスト入力で生成するラベルのない実行トレースのみを使用して、評価自体にハーネスを最適化できるかどうかを問う。 評価中、TTHEは候補ハーネスの人口を維持し、それらの実行トレースの理由をエージェントプロジェクタを通じてそれらを洗練する。 その後、審査員は実行元プロキシ信号から改善されたハーネスをコミットし、選択したプログラムは継続してその後の入力を統治する。
  論文  参考訳（メタデータ） (2026-07-09T05:53:39Z)
• EvoAgentBench: Benchmarking Agent Self-Evolution via Ability Transfer [25.657960361149833]
  EvoAgentBenchは、Ability-guided Transferによるエージェントの自己進化のベンチマークである。 すべてのテストタスクは、認証されたトレーニングサイドの能力サポートによってバックアップされる。
  論文  参考訳（メタデータ） (2026-07-06T15:17:09Z)
• The Red Queen Gödel Machine: Co-Evolving Agents and Their Evaluators [17.44053709945519]
  自己改善エージェントはエージェントコーディングベンチマークの最先端(SOTA)であり、最近一般的なドメインに拡張されている。 非定常ユーティリティ下での自己改善のための進化的フレームワークであるRed Queen Godel Machine(RQGM)を紹介する。 RQGMは、補完的なエージェント・アズ・ア・ジャッジ・コード・レビュー信号を追加することにより、以前のSOTAよりもテストパス率を向上させることを示す。 次に、科学論文の執筆とレビュー、オリンピアードレベルの証明の執筆と評価に目を向け、RQGMは以前の自己改善エージェントよりもパフォーマンスを向上させる。
  論文  参考訳（メタデータ） (2026-06-24T18:38:26Z)
• Self-evolving LLM agents with in-distribution Optimization [60.05867547965365]
  大規模言語モデル(LLM)は最近、複雑な環境で対話的なエージェントのための強力なコントローラとして登場した。 本稿では,自動プロセス・リワードラベリングとポリシー学習を統一するLDMエージェントの自己進化フレームワークであるQ-Evolveを提案する。 我々は,AlfWorld,WebShop,ScienceWorldの手法を評価し,Q-Evolveがサンプル効率,堅牢性,全体的なタスク性能において高いベースラインを達成していることを示す。
  論文  参考訳（メタデータ） (2026-06-05T15:09:52Z)
• AgentV-RL: Scaling Reward Modeling with Agentic Verifier [63.55502685076245]
  試験時間スケーリング(TTS)によるLCM推論を強化する検証器が実証されている。 本稿では,報酬モデリングを多ターンツール拡張型検討プロセスに変換するフレームワークであるエージェント検証を提案する。 Agentic Verifier は並列およびシーケンシャルTS の両方で一貫した性能向上が得られることを示す。
  論文  参考訳（メタデータ） (2026-04-17T12:27:36Z)
• FRESCO: Benchmarking and Optimizing Re-rankers for Evolving Semantic Conflict in Retrieval-Augmented Generation [73.22935457705057]
  時間的動的文脈における再ランカ評価のためのベンチマークであるFRESCOを紹介する。 レクエンシ検索クエリと過去のウィキペディアのリビジョンを組み合わせることで、FRESCOは、セマンティックな関連性を維持しながら、リランカが事実として最新の証拠を優先順位付けできるかどうかをテストする。 我々の評価では、既存の再ランカ間で一貫した障害モードが明らかになっている。
  論文  参考訳（メタデータ） (2026-04-14T17:04:25Z)
• CoVerRL: Breaking the Consensus Trap in Label-Free Reasoning via Generator-Verifier Co-Evolution [52.691495954442985]
  CoVerRLは1つのモデルがジェネレータと検証ロールを交換するフレームワークで、各機能が他方をブートストラップする。 Qwen と Llama のモデルファミリーでの実験では、CoVerRL は数理推論のベンチマークで4.7-5.9% でラベルなしのベースラインを上回っている。 自己検証の精度は55%から85%以上改善され、両方の能力が真に共存することを確認した。
  論文  参考訳（メタデータ） (2026-03-18T14:38:55Z)
• AgentDevel: Reframing Self-Evolving LLM Agents as Release Engineering [8.201374511929538]
  AgentDevelは、現行のエージェントを反復的に実行するリリースエンジニアリングパイプラインである。 実行トレースから実装盲の症状レベルの品質信号を生成する。 主要な症状パターンを集約し、監査可能なエンジニアリング仕様を生成する。
  論文  参考訳（メタデータ） (2026-01-08T05:49:01Z)
• Towards Self-Evolving Benchmarks: Synthesizing Agent Trajectories via Test-Time Exploration under Validate-by-Reproduce Paradigm [60.36837655498119]
  本稿では,トラジェクトリをベースとしたエージェント・ベンチマーク・複雑度進化フレームワークを提案する。 このフレームワークは、既存のベンチマークから元のタスクを受け取り、エージェントがそれをより難しい新しいタスクに進化させるよう促す。 GAIAベンチマークの実験では、TRACEフレームワークはタスクの複雑さを継続的に向上し、正確性の信頼性を向上させる。
  論文  参考訳（メタデータ） (2025-10-01T01:52:52Z)

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

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