論文の概要: Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
- arxiv url: http://arxiv.org/abs/2603.06737v1
- Date: Fri, 06 Mar 2026 07:34:07 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-10 15:13:13.007443
- Title: Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents
- Title（参考訳）: エージェントハント:LLMエージェントによるバウンティベースのコラボレーションオートモーフィゼーション
- Abstract要約: この設定は、協調的で分散化された証明探索と理論構築を探索する。
エージェントは、インタラクティブな証明システムと直接対話する。
承認されたすべての証明は、基礎となる証明アシスタントによってチェックされ、検証される。
- 参考スコア（独自算出の注目度）: 2.8292841621378844
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We describe an experiment in large-scale autoformalization of algebraic topology in an Interactive Theorem Proving (ITP) environment, where the workload is distributed among multiple LLM-based coding agents. Rather than relying on static central planning, we implement a simulated bounty-based marketplace in which agents dynamically propose new lemmas (formal statements), attach bounties to them, and compete to discharge these proof obligations and claim the bounties. The agents interact directly with the interactive proof system: they can invoke tactics, inspect proof states and goals, analyze tactic successes and failures, and iteratively refine their proof scripts. In addition to constructing proofs, agents may introduce new formal definitions and intermediate lemmas to structure the development. All accepted proofs are ultimately checked and verified by the underlying proof assistant. This setting explores collaborative, decentralized proof search and theory building, and the use of market-inspired mechanisms to scale autoformalization in ITP.
- Abstract（参考訳）: 対話的定理証明(ITP)環境における代数トポロジの大規模自己形式化実験について述べる。
静的中央計画に頼るのではなく、エージェントが動的に新しいレムマ(形式的ステートメント)を提案し、それらに報奨金をアタッチし、これらの証明義務を解除し、報奨を請求する、シミュレートされた報奨ベースのマーケットプレースを実装している。
エージェントは、インタラクティブな証明システムと直接対話し、戦術を実行し、証明状態と目標を検査し、戦術的な成功と失敗を分析し、その証明スクリプトを反復的に洗練することができる。
証明の構築に加えて、エージェントは開発を構築するために新しい形式定義と中間補題を導入することができる。
受け入れられたすべての証明は最終的に、基礎となる証明アシスタントによってチェックされ、検証される。
この設定は、協調的で分散化された証明探索と理論構築、およびIPPにおける自己形式化をスケールするための市場インスパイアされたメカニズムの利用を探索する。
関連論文リスト
- (Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs [0.20305676256390937]
本稿では,LLMエージェントを決定論的に制約されたワークフローで活用して,リーンの自己形式化タスクの漸進的な進歩を実現する自動形式化システムを提案する。
我々のアプローチは、まず第一に厳密な証明を持つことの意味についての一般数学者の考えに動機づけられている。
プロセスによって生み出された最近のRamsey理論のブレークスルーを、エンドツーエンドのリーン形式化にリンクします。
論文 参考訳（メタデータ） (2026-06-08T15:57:14Z) - A Sober Look at Agentic Misalignment in Automated Workflows [39.62671225833463]
マルチエージェントシステム(MAS)における創発的ミスアライメントのクラスについて検討する。
エージェントエビデンス属性(AEA)は、文脈特異的な証拠を用いてエージェント後部を改善する新しいアライメントパラダイムである。
論文 参考訳（メタデータ） (2026-05-22T20:40:20Z) - VerifyMAS: Hypothesis Verification for Failure Attribution in LLM Multi-Agent Systems [79.51005192758262]
大規模言語モデル駆動型マルチエージェントシステムは複雑なタスクで優れている。
しかし、信頼性の低いエージェントは、システムレベルの信頼性にとって重要なボトルネックである。
本稿では,エージェント故障の帰属に関する仮説検証フレームワークを提案する。
論文 参考訳（メタデータ） (2026-05-17T14:09:35Z) - Beyond Individual Intelligence: Surveying Collaboration, Failure Attribution, and Self-Evolution in LLM-based Multi-Agent Systems [65.90791804095561]
マルチエージェントシステムは、特殊エージェント間の構造化された協調を通じてこの問題に対処するが、より厳密な調整は、あまり検討されていないリスクを増幅する。
既存の調査では、個々のエージェント能力、マルチエージェントのコラボレーション、エージェントの自己進化を別々にカバーしている。
この調査は4つの因果関係のあるステージを中心にまとめられた統一されたレビューを提供する。これはLIFEの進展(Lay the capabilities foundation)、協力によるエージェントの統合、帰属による障害の発見、自律的な自己改善によるEvolveである。
論文 参考訳（メタデータ） (2026-05-14T14:36:13Z) - AgentV-RL: Scaling Reward Modeling with Agentic Verifier [63.55502685076245]
試験時間スケーリング(TTS)によるLCM推論を強化する検証器が実証されている。
本稿では,報酬モデリングを多ターンツール拡張型検討プロセスに変換するフレームワークであるエージェント検証を提案する。
Agentic Verifier は並列およびシーケンシャルTS の両方で一貫した性能向上が得られることを示す。
論文 参考訳（メタデータ） (2026-04-17T12:27:36Z) - Agentic Program Verification [14.684859166069012]
本稿では,プログラム検証を行うための最初の大規模言語モデルエージェントであるAutoRocqを提案する。
LLMの広範な訓練を実証例に頼っている過去の研究とは異なり、我々のエージェントはオンザフライで学習し、反復的な改善ループを通じて証明を改善する。
このようにして、我々の証明構成は証明エージェントと定理証明器との間の自律的な協調を含む。
論文 参考訳（メタデータ） (2025-11-21T15:51:48Z) - Alita-G: Self-Evolving Generative Agent for Agent Generation [54.49365835457433]
汎用エージェントをドメインエキスパートに変換するフレームワークであるALITA-Gを提案する。
このフレームワークでは、ジェネラリストエージェントが対象ドメインタスクのキュレートされたスイートを実行する。
計算コストを削減しながら、大きな利益を得ることができます。
論文 参考訳（メタデータ） (2025-10-27T17:59:14Z) - 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) - Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs [11.87831709160905]
本稿では,自動定理証明のためのAIエージェントであるProver Agentを紹介する。
大規模な言語モデル(LLM)と公式な証明アシスタントであるLeanを統合している。
MiniF2Fベンチマークで88.1%の成功率を達成した。
論文 参考訳（メタデータ） (2025-06-24T18:01:52Z) - When Disagreements Elicit Robustness: Investigating Self-Repair Capabilities under LLM Multi-Agent Disagreements [56.29265568399648]
我々は、不一致が早期のコンセンサスを防ぎ、探索されたソリューション空間を拡張することを主張する。
タスククリティカルなステップの相違は、ソリューションパスのトポロジによってコラボレーションを損なう可能性がある。
論文 参考訳（メタデータ） (2025-02-21T02:24:43Z) - Textualized Agent-Style Reasoning for Complex Tasks by Multiple Round LLM Generation [49.27250832754313]
我々は、llmベースの自律エージェントフレームワークであるAgentCOTを紹介する。
それぞれのステップで、AgentCOTはアクションを選択し、それを実行して、証拠を裏付ける中間結果を得る。
エージェントCOTの性能を高めるための2つの新しい戦略を導入する。
論文 参考訳（メタデータ） (2024-09-19T02:20:06Z) - Smart Proofs via Smart Contracts: Succinct and Informative Mathematical
Derivations via Decentralized Markets [4.567122178196833]
SPRIGは、エージェントが分散的な方法で簡潔で情報的な証明を提案し、検証することを可能にする。
様々な種類の情報を持つエージェントがどのように相互作用し、適切なレベルの詳細を持つ証明木につながるかを示す。
次に、単純化されたモデルを分析し、その均衡を特徴づけ、エージェントの信頼度を計算する。
論文 参考訳（メタデータ） (2021-02-05T08:00:19Z) - Empirically Verifying Hypotheses Using Reinforcement Learning [58.09414653169534]
本稿では,仮説検証をRL問題として定式化する。
我々は、世界の力学に関する仮説を前提として、仮説が真か偽かを予測するのに役立つ観測結果を生成することができるエージェントを構築することを目指している。
論文 参考訳（メタデータ） (2020-06-29T01:01:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。