論文の概要: Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
- arxiv url: http://arxiv.org/abs/2609.39544v2
- Date: Thu, 01 Oct 2026 08:57:55 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-03 01:19:23.557611
- Title: Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
- Title（参考訳）: エージェント/プロバーインターフェースの成長:Rocqとリーンで証明されたコスト効率のよい理論のための進化的ツール設計
- Abstract要約: 最近のAI支援数学の成果は、機械チェックされた証明証明書を生成するために、エージェントと証明アシスタントとの集中的な相互作用を必要とする。
エージェントは、エージェントが証明者から受け取ったものとそれらの相互作用のコストを制御するインターフェースを通じて、RocqやLeanのような証明アシスタントと対話する。
本稿では,フロンティアモデルが新たな特徴を漸進的に提案する進化的手法を提案する。
- 参考スコア（独自算出の注目度）: 6.652641137999889
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Recent achievements in AI-assisted mathematics require intensive interaction of agents with proof assistants to generate machine-checked proof certificates. Agents interact with proof assistants such as Rocq or Lean through an interface that controls what the agent receives from the prover and the cost of these interactions. Today, these interfaces are adapted from tools designed for humans and not optimized for agents. We propose an evolutionary method where a frontier model incrementally proposes new features and only keeps the ones that improve the overall performance of smaller models. We demonstrate the effectiveness of our method by growing, on a curated set of mathematical problems, \rme, a new MCP server for the Rocq prover. On the held-out \texttt{test} split of miniF2F-Rocq, an agent equipped with \rme outperforms both the baseline that only exposes the Rocq compiler and an established MCP server, across four models from two families, in success rate, cost per solve, and time per solve. Although evolved for Rocq, the resulting server transfers to Lean, improving cost and time per solve on a subset of PutnamBench. We release \rme and its port to Lean.
- Abstract（参考訳）: 最近のAI支援数学の成果は、機械チェックされた証明証明書を生成するために、エージェントと証明アシスタントとの集中的な相互作用を必要とする。
エージェントは、エージェントが証明者から受け取ったものとそれらの相互作用のコストを制御するインターフェースを通じて、RocqやLeanのような証明アシスタントと対話する。
現在、これらのインターフェースは人間用に設計されたツールに適応しており、エージェントに最適化されていない。
本稿では,フロンティアモデルが新たな特徴を漸進的に提案する進化的手法を提案する。
そこで我々は,Rocq 証明器用の新しい MCP サーバである \rme を,数理問題群に展開することにより,本手法の有効性を実証する。
miniF2F-Rocq の保持された \texttt{test} 分割において、rme を備えたエージェントは、Rocq コンパイラと確立された MCP サーバのみを公開するベースラインと、成功率、解決毎のコスト、解決毎の時間という4つのモデルの両方より優れる。
Rocqは進化したが、結果としてサーバがLeanに移行し、PutnamBenchのサブセットで解決するコストと時間が改善された。
私たちは、SharmeとそのLeanへのポートをリリースします。
関連論文リスト
- MADE: Belief-Driven Dual-Agent Coordination for Autonomous Model Deployment [19.126846876843356]
LLMベースのエージェントはドメイン固有のタスクに苦労し、外部ツールの統合を動機付けている。
オープンソースコミュニティは、典型的に異質な研究成果物としてリリースされる多数のAIモデルを提供している。
これらをプリ・ツー・コールのAPIに変換するのは費用がかかり、労力がかかる。
本稿では,デュアルエージェント協調システムであるModel Automated Deployment Engine (MADE)を紹介する。
論文 参考訳（メタデータ） (2026-08-02T12:14:43Z) - Agent Q-Mix: Selecting the Right Action for LLM Multi-Agent Systems through Reinforcement Learning [68.85408801740228]
協調型マルチエージェント強化学習問題としてトポロジ選択を再構成する強化学習フレームワークである textbfAgent Q-Mix を提案する。
提案手法は,Qmix値分解を用いて分散化された通信決定を学習し,各エージェントがラウンドワイド通信グラフを共同生成する一連の通信行動から選択する。
エージェントQ-Mixは,エージェント故障に対して優れたトークン効率とロバスト性を示しながら,既存手法と比較して高い平均精度を達成する。
論文 参考訳（メタデータ） (2026-04-01T00:38:24Z) - AgentArk: Distilling Multi-Agent Intelligence into a Single LLM Agent [57.10083973844841]
AgentArkは、マルチエージェントダイナミクスを単一のモデルの重みに蒸留する新しいフレームワークである。
各種モデル,タスク,スケーリング,シナリオの3つの階層的蒸留戦略について検討する。
シミュレーションからトレーニングへ計算の負担をシフトさせることで、蒸留されたモデルは、複数のエージェントの強い推論と自己補正性能を示しながら、一つのエージェントの効率を保ちます。
論文 参考訳（メタデータ） (2026-02-03T19:18:28Z) - GenAgent: Scaling Text-to-Image Generation via Agentic Multimodal Reasoning [54.42973725693]
我々は,エージェント型マルチモーダルモデルを用いて,視覚的理解と生成を統一したGenAgentを導入する。
GenAgentはGenEval++とWISEのベースジェネレータ(FLUX.1-dev)のパフォーマンスを大幅に向上させる。
本フレームワークは,1) 様々な機能を持つジェネレータへのクロスツール一般化,2) インタラクションラウンド間で一貫した改善を伴うテスト時間スケーリング,3) タスクに自動的に適応するタスク適応推論の3つの重要な特性を示す。
論文 参考訳（メタデータ） (2026-01-26T14:49:04Z) - ArchPilot: A Proxy-Guided Multi-Agent Approach for Machine Learning Engineering [18.83090180326138]
ArchPilotは、アーキテクチャ生成、プロキシベースの評価、適応検索を統一されたフレームワークに統合するマルチエージェントシステムである。
コストのかかるフルトレーニングの実行に最小限依存した、強力な候補を優先し、限られた予算下で効率的なMLエンジニアリングを促進する。
論文 参考訳（メタデータ） (2025-11-06T02:14:59Z) - $Agent^2$: An Agent-Generates-Agent Framework for Reinforcement Learning Automation [5.325886106098561]
強化学習(RL)エージェント開発は伝統的にかなりの専門知識と反復的な努力を必要とする。
本稿では,完全自動RLエージェント設計のための LLM 駆動型エージェント生成エージェントフレームワークである Agent$2$ を紹介する。
Agent$2$は、自然言語のタスク記述と環境コードを人間の介入なしに実行可能なRLソリューションに変換する。
論文 参考訳（メタデータ） (2025-09-16T02:14:39Z) - Chain-of-Agents: End-to-End Agent Foundation Models via Multi-Agent Distillation and Agentic RL [41.847359443133776]
CoA(Chain-of-Agents)は、大規模言語モデル(LLM)推論の新しいパラダイムであり、ネイティブなエンドツーエンドの複雑な問題解決を可能にする。
我々は, エージェント制御微調整のための多エージェント蒸留フレームワークを導入し, 最先端のマルチエージェントシステムをチェーン・オブ・エージェント・トラジェクトリに蒸留する。
次に、検証可能なエージェントタスクに対するエージェント強化学習を用いて、チェーン・オブ・エージェントの問題解決におけるモデルの能力をさらに向上する。
論文 参考訳（メタデータ） (2025-08-06T17:01:02Z) - R&D-Agent: An LLM-Agent Framework Towards Autonomous Data Science [70.1638335489284]
高レベルの機械学習エンジニアリングタスクは、労働集約的で反復的である。
機械学習プロセスを形式化する包括的で分離されたフレームワークであるR&D-Agentを紹介します。
R&D-AgentはMLEを2つのフェーズと6つのコンポーネントに定義し、MLEのエージェント設計を原則としてテスト可能なプロセスに変える。
論文 参考訳（メタデータ） (2025-05-20T06:07:00Z) - A Dynamic LLM-Powered Agent Network for Task-Oriented Agent Collaboration [55.35849138235116]
本稿では,様々なタスクやドメインに対する動的コミュニケーション構造において,候補からエージェントのチームを自動的に選択する手法を提案する。
具体的には, LLMを利用したエージェント協調のための動的LLMパワーエージェントネットワーク(textDyLAN$)というフレームワークを構築した。
我々は、コード生成、意思決定、一般的な推論、算術的推論タスクにおいて、適度な計算コストで、DyLANが強力なベースラインを上回ることを実証する。
論文 参考訳（メタデータ） (2023-10-03T16:05:48Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。