論文の概要: 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エージェントによるバウンティベースのコラボレーションオートモーフィゼーション
• Authors: Chad E. Brown, Cezary Kaliszyk, Josef Urban,
• 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における自己形式化をスケールするための市場インスパイアされたメカニズムの利用を探索する。

関連論文リスト

• 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)

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

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