論文の概要: Viva La Vida: Verification and Accumulation Failures in Multi-Agent Proof Search
- arxiv url: http://arxiv.org/abs/2610.04829v1
- Date: Sun, 04 Oct 2026 00:24:02 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-11 08:34:37.526266
- Title: Viva La Vida: Verification and Accumulation Failures in Multi-Agent Proof Search
- Title（参考訳）: Viva La Vida: マルチエージェントの証明検索における検証と累積失敗
- Abstract要約: モデル出力を判断する言語モデルである検証器と補題ライブラリを用いてエージェント証明を解析する。
接続障害モードは3つあります。
これらの結果は、外部の検証がなければ、監督はそれ自体が重要な信頼境界であることを示している。
- 参考スコア（独自算出の注目度）: 1.6586086690525175
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: When an agentic prover works on an open problem, there is no proof assistant to fall back on: its verifier and lemma library are ultimately language models judging model outputs. We instrumented such a system end to end and analyzed $51{,}754$ traced observations across three full runs ($186$ hours, \$$5{,}694$). We find three connected failure modes. First, the three-model verifier requires unanimity and treats parse or API failure as non-approval; in $10$ of $12$ verification events, one member returned no parseable output or an API error, making acceptance arithmetically impossible without surfacing an error. Second, when the ensemble did function, one verifier approved $3$ attempts that GPT rejected, each claiming to resolve the open problem; a single-verifier design would therefore have announced a solution three times. Third, because nothing could be approved, every review was a refutation, yet the lemma extractor mines reviews as well as proofs: $24$ of $93$ lemmas ($26\%$) were extracted from rejected arguments with their refutational context removed. Taken together, these findings show that without external verification, supervision is itself a critical trust boundary: systems must distinguish abstention from rejection, preserve useful disagreement, and preserve the provenance and polarity of information before it becomes future context.
- Abstract（参考訳）: エージェント証明器がオープンな問題に取り組むとき、その検証器と補題ライブラリは最終的にモデル出力を判断する言語モデルである。
このようなシステムをエンドツーエンドに計測し、3回のフルラン(186$ hours, \$5{,}694$)にわたる511{,}754$のトレース観測を分析しました。
接続障害モードは3つあります。
まず、3モデル検証器は、一様性を必要とし、パースまたはAPI失敗を非承認として扱う。10ドルの検証イベントでは、1人のメンバーがパース可能な出力やAPIエラーを返し、エラーを発生させずに受理を算術的に不可能にする。
第二に、アンサンブルが機能すると、ある検証者はGPTが拒否した3ドルの試みを承認し、それぞれがオープンな問題を解決すると主張した。
第3に、何も承認できないため、すべてのレビューは難解なものだったが、レムマ抽出機はレビューと証明を採り入れている:$24$$933$ lemmas (26\%$) は、その難解な文脈を取り除いた議論から抽出された。
これらの知見は、外部の検証がなければ、監督はそれ自体が重要な信頼境界であることを示している:システムは拒否から棄却を区別し、有用な意見の不一致を保ち、将来的な文脈になる前に情報の存在と極性を維持する必要がある。
関連論文リスト
- VeriHarness: Scaling Agentic Verification for Long-Horizon Tasks [56.74345405508208]
LLMエージェントはますます複雑で長期のタスクをこなし、そのアウトプットを検証することがますます困難になっている。
本研究では, 基準応答へのアクセスや試験時の潤滑油の分解を行わずに, 固定ベースモデルで検証能力を強化する方法について検討する。
コンセンサスによってエラーを隠蔽できる一方で、不一致はしばしば正しい代替手段を公開することに気付きました。
これらの観察はVeriHarnessを動機付け、ジェネレータが使用する基礎となるLLMを、ワークスペース、エビデンスツール、再利用可能な検証スキルを与えることによって、エージェント検証器に変える。
論文 参考訳（メタデータ） (2026-10-01T03:02:17Z) - The Detectability Gap: Hidden Heterogeneity in Hallucination Detection Across Language Models [4.0571268682981865]
回答合意による幻覚の分割は、高い合意(ゴースト)と低い合意(フリッカリング)の体制を明らかにする。
個々の拡散軌道を用いたより厳密なテストとクロスシード情報は、3つのLLaDAデータセットのすべてに非対称性を保持する。
ハードレジームは、モデル間での頻度が大きく異なり(16%$から77%$)、マッチしたプロンプトはモデル間のレジームを頻繁に変更する。
論文 参考訳（メタデータ） (2026-09-25T17:12:24Z) - Audit Before You Commit: Locating Belief Failures in Active Identification for One-Shot Manipulation [2.255961793913651]
我々は、ペグを挿入する前に表面をタップするなど、ある不可逆的なアクションの前に数回プローブするロボットは、その証拠がコミットするのに十分なタイミングを決定する必要がある、と論じる。
この決定は、既存のメソッドが分離しない2つの条件に依存している、と我々は主張する。信念は、アクションを決定する座標の真理をまだカバーしなくてはならないし、アクションをスコアする失敗モデルは、実現した失敗を追跡する必要がある。
我々は、デプロイされたプローブ-then-commitパイプライン上で、オフラインと地上の真理の両方の条件を別々に監査する。
論文 参考訳（メタデータ） (2026-09-24T22:47:32Z) - TeleAntiFraud 2.0: A Refreshable, Profile-Grounded, and Audio-Based Benchmark for Telecom Fraud Detection [55.35119005976305]
テレコム詐欺スクリプトは急速に進化し、日常的なサービス会話に似たように設計されている。
ベンチマークは、以前に確立されたテストセットを上書きすることなく、新しく観察された詐欺パターンを組み込まなければならない。
本稿では,Mixed-Tree Anti-Fraud Generation Pipelineで構築したTeleAntiFraud 2.0について述べる。
論文 参考訳（メタデータ） (2026-09-16T14:41:11Z) - Can Code Specify a System Precisely Enough to Formally Verify It? [0.0]
本報告では,業務用レストラン・ポイント・オブ・セールシステムの支払ワークフローを実運用ソフトウェアで評価する。
コアプロトコルは、正確に定義された障害モデルの下で手作りのラインアクティベートされたモデルに対して正しい。
生産用サンドボックスの1つのプローブは、全リカバリはしごを到達不能にする応答形状のばらつきを露呈した。
論文 参考訳（メタデータ） (2026-07-06T13:39:00Z) - PA-User: Simulating Trust and Verification under AI-Generated Content [1.1105673928718571]
3つの新しいコンポーネントを持つユーザシミュレータPA-Userを提案する。
信頼コンポーネントは、それぞれのソースクラスの事実に関する別々のベータ信念を持っています。
決定ルールは、各結果に対する受け入れ、証明、破棄を選択する。
論文 参考訳（メタデータ） (2026-06-22T00:45:06Z) - Correction and Corruption: A Two-Rate View of Error Flow in LLM Protocols [51.56484100374058]
そこで本研究では,単一プロトコルステップを正確なマッチングタスクで監査するためのペアアウトカム計測インタフェースを提案する。
各インスタンスについて、インターフェースはベースラインの正当性ビットと後ステップの正当性ビットを記録する。
これらのレートは精度の変化を予測し、種、混合物、パイプライン間でテスト可能な再利用可能な経験的インターフェースを定義する。
論文 参考訳（メタデータ） (2026-04-20T13:25:40Z) - Consistency-Guided Decoding with Proof-Driven Disambiguation for Three-Way Logical Question Answering [4.878198984786631]
3方向の論理的質問応答(QA)は、$True/False/Unknown$を前提セット$S$の仮説に割り当てる。
CGD-PDは1つの3ウェイ分類器を$H$と$H$の機械式の両方でクエリする軽量なテスト時間層である。
論文 参考訳（メタデータ） (2026-03-12T18:26:16Z) - interwhen: A Generalizable Framework for Verifiable Reasoning with Test-time Monitors [47.363850513075356]
実験時間検証フレームワークであるInterwhenを提案し, 与えられた検証結果に対して, 推論モデルの出力が有効であることを保証する。
検証された推論は、物理的な世界にエージェントを配置するといった高度なシナリオにおいて重要な目標である。
論文 参考訳（メタデータ） (2026-02-05T08:35:01Z) - Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [71.7892165868749]
LLM(Commercial Large Language Model) APIは基本的な信頼の問題を生み出します。
ユーザーは特定のモデルに課金するが、プロバイダが忠実に提供できることを保証することはない。
我々は,このモデル置換問題を定式化し,現実的な逆条件下での検出方法を評価する。
我々は,信頼された実行環境(TEE)を実用的で堅牢なソリューションとして使用し,評価する。
論文 参考訳（メタデータ） (2025-04-07T03:57:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。