論文の概要: RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
- arxiv url: http://arxiv.org/abs/2602.05762v1
- Date: Thu, 05 Feb 2026 15:28:26 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-02-06 18:49:09.00155
- Title: RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
- Title（参考訳）: RocqSmith: 自動最適化は証明エージェントを改善できるか?
- Authors: Andrei Kozyrev, Nikita Khramov, Denis Lochmelis, Valerio Morelli, Gleb Solovev, Anton Podkopaev,
- Abstract要約: 我々は,Rocqの証明生成エージェントを最適化するタスクに適用した場合に,異なる自動エージェントがどのように機能するかを評価する。
以上の結果から,いくつかのブートストラップが測定可能な改善をもたらす一方で,単純な数発ブートストラップが最も有効であることが示唆された。
- 参考スコア（独自算出の注目度）: 0.07696728525672149
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: This work studies the applicability of automatic AI agent optimization methods to real-world agents in formal verification settings, focusing on automated theorem proving in Rocq as a representative and challenging domain. We evaluate how different automatic agent optimizers perform when applied to the task of optimizing a Rocq proof-generation agent, and assess whether parts of the fine-grained tuning of agentic systems, such as prompt design, contextual knowledge, and control strategies, can be automated. Our results show that while several optimizers yield measurable improvements, simple few-shot bootstrapping is the most consistently effective; however, none of the studied methods matches the performance of a carefully engineered state-of-the-art proof agent.
- Abstract（参考訳）: 本研究は,Rocqを代表的かつ困難な領域として証明した自動定理に着目し,実世界のエージェントに対するAIエージェントの自動最適化手法の適用性について検討する。
我々は,Rocqの証明生成エージェントを最適化するタスクに適用した場合に,異なる自動エージェントオプティマイザがどのように機能するかを評価し,プロンプト設計や文脈知識,制御戦略などのエージェントシステムの微粒化チューニングの一部が自動化可能であるかを評価する。
以上の結果から,いくつかのオプティマイザが測定可能な改善を実現しているのに対し,単純な数発のブートストラップが最も有効であることが示唆された。
関連論文リスト
- AgentArk: Distilling Multi-Agent Intelligence into a Single LLM Agent [57.10083973844841]
AgentArkは、マルチエージェントダイナミクスを単一のモデルの重みに蒸留する新しいフレームワークである。
各種モデル,タスク,スケーリング,シナリオの3つの階層的蒸留戦略について検討する。
シミュレーションからトレーニングへ計算の負担をシフトさせることで、蒸留されたモデルは、複数のエージェントの強い推論と自己補正性能を示しながら、一つのエージェントの効率を保ちます。
論文 参考訳（メタデータ） (2026-02-03T19:18:28Z) - Are Agents Just Automata? On the Formal Equivalence Between Agentic AI and the Chomsky Hierarchy [4.245979127318219]
本稿では,現代エージェントAIシステムのアーキテクチャクラスと階層の抽象機械との形式的等価性を確立する。
単純な反射エージェントは有限オートマタと等価であり、階層的なタスク分解エージェントはプッシュダウンオートマタと等価であり、リフレクションに読み取り/書き込み可能なメモリを使用するエージェントはTMと等価であることを示す。
論文 参考訳（メタデータ） (2025-10-27T16:22:02Z) - InfiAgent: Self-Evolving Pyramid Agent Framework for Infinite Scenarios [28.65914611521654]
InfiAgentはピラミッドのようなDAGベースのMulti-Agent Frameworkで、textbfinfiniteのシナリオに適用できる。
InfiAgentはADAS(類似の自動生成エージェントフレームワーク)と比較して9.9%高いパフォーマンスを実現している
論文 参考訳（メタデータ） (2025-09-26T15:44:09Z) - $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) - A Multi-AI Agent System for Autonomous Optimization of Agentic AI Solutions via Iterative Refinement and LLM-Driven Feedback Loops [3.729242965449096]
本稿では,産業間におけるエージェントAIソリューションを自律的に最適化するフレームワークを提案する。
このフレームワークは、仮説を自律的に生成し、テストすることで、人間の入力なしに最適な性能を達成する。
ケーススタディでは、アウトプットの品質、妥当性、動作性が大幅に改善された。
論文 参考訳（メタデータ） (2024-12-22T20:08:04Z) - Agent-as-a-Judge: Evaluate Agents with Agents [61.33974108405561]
本稿ではエージェント・アズ・ア・ジャッジ(Agent-as-a-Judge)フレームワークを紹介し,エージェント・システムを用いてエージェント・システムの評価を行う。
これはLLM-as-a-Judgeフレームワークの有機的拡張であり、タスク解決プロセス全体の中間フィードバックを可能にするエージェント的特徴を取り入れている。
55のリアルな自動化AI開発タスクのベンチマークであるDevAIを紹介します。
論文 参考訳（メタデータ） (2024-10-14T17:57:02Z) - Gödel Agent: A Self-Referential Agent Framework for Recursive Self-Improvement [112.04307762405669]
G"odel AgentはG"odelマシンにインスパイアされた自己進化型フレームワークである。
G"odel Agentは、パフォーマンス、効率、一般化性において手作業によるエージェントを上回る、継続的な自己改善を実現することができる。
論文 参考訳（メタデータ） (2024-10-06T10:49:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。