論文の概要: When Verification Is Not Agreement: Cross-Agent LLM-to-Dafny Formalization
- arxiv url: http://arxiv.org/abs/2611.07073v1
- Date: Wed, 04 Nov 2026 19:31:51 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-11-06 21:50:50.438991
- Title: When Verification Is Not Agreement: Cross-Agent LLM-to-Dafny Formalization
- Title（参考訳）: 検証が一致しないとき - クロスエージェントなLLM-to-Dafny形式化
- Abstract要約: ダフニーの事後条件は、式が成り立つことを証明しているが、真に独立した推論によって結果が到達したことを保証していない。
Specifier モデル臨床試験基準は Dafny 述語に翻訳され、Implementer モデルはそれに対してチェックされた操作方法を記述する。
同モデル制御は、機能ギャップがなくても、同じテキストから独立した再抽出が59.3%の時間しか一致しないことを示す。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: A verified Dafny postcondition certifies that a formula holds, but it does not guarantee that the result was reached through genuine independent reasoning. We introduce a cross-agent formalization protocol where a Specifier model translates clinical trial criteria into a Dafny predicate, and an Implementer model writes an operational method checked against it. A same-model control establishes that even with no capability gap, independent re-extraction from identical text agrees only 59.3% of the time. Evaluating four model configurations on 96 clinical trial documents, we find that agreement is highly sensitive to how model capability is allocated across the two roles: the GPT-4.1-nano/GPT-4.1-mini configuration achieves 53.0% agreement when the stronger model is the Implementer, but only 14.3% when the roles are reversed. The strongest tested configuration, GPT-5.6-luna/GPT-5.4-mini, improves agreement to 34.4% but remains below the same-model baseline and is dominated by direct contradiction (42.7%). We also detect a critical verification artifact in which a weaker Implementer satisfies the postcondition by invoking the Specifier's predicate directly; after structural auditing, corrected agreement falls from 14.3% to 13.2%. Our results show that verification success alone is insufficient evidence of independent cross-agent agreement, and that model capability does not guarantee agreement when formalizing the same source independently.
- Abstract（参考訳）: 検証されたダフニーの条件は、式が成り立つことを証明しているが、真に独立した推論によって結果が到達したことを保証していない。
本稿では,検定基準をダフニー述語に翻訳するクロスエージェント形式化プロトコルを提案する。
同モデル制御は、機能ギャップがなくても、同じテキストから独立した再抽出が59.3%の時間しか一致しないことを示す。
GPT-4.1-nano/GPT-4.1-mini構成は、強いモデルがImplementerである場合に53.0%の合意を得るが、ロールが逆転するとわずか14.3%となる。
最も強力な試験装置であるGPT-5.6-luna/GPT-5.4-miniは合意を34.4%に改善したが、同じモデルベースライン以下であり、直接矛盾(42.7%)に支配されている。
また,より弱いImlementerが特定者の述語を直接呼び出すことにより,条件を満足する重要な検証成果も検出する。構造監査後,修正された合意は14.3%から13.2%に低下する。
本結果から,検証成功だけでは独立したクロスエージェント契約の証拠が不十分であること,モデル能力が同一ソースを独立に定式化する際の合意を保証するものではないことが示唆された。
関連論文リスト
- Right Answers, Wrong States: Hidden Information Failures in Multi-Agent Collaboration [69.14904049421806]
共同作業は、即時決定が正しい場合でも、腐敗した情報状態に置き去りにすることができる。
GPT、Gemini、Qwenモデル全体では、標準的なコラボレーションは、状態の信頼性よりもはるかに強力なタスクパフォーマンスを示している。
我々は、矛盾する証拠を解決し、共有された事実を検証し、信頼された国家を再構築するReGroundを紹介します。
論文 参考訳（メタデータ） (2026-10-01T07:42:27Z) - Persuaded, Not Informed: Incentive-Misaligned Witnesses Defeat In-Context Grounding [0.0]
より強力なモデルで対処されていない障害モードを特定します。
文脈が楽観主義へのインセンティブを持つ当事者による主張を含む場合、モデルはこの主張を証拠として扱い、明確化は会社の記録を容認できないとみなす。
論文 参考訳（メタデータ） (2026-09-23T23:52:24Z) - Measuring What a Specification Determines: A Formal Semantic-Block Model and an Execution-Judged Benchmark [0.0]
本研究では,仕様の形式的セマンティックブロックモデルと,仕様品質を評価するための実行基準ベンチマークを導入する。
仕様は、セマンティックブロック、依存関係の関係、ブロック所有ルール、決定ポイント、明示的にオープンな質問からなる構造として表現される。
ベンチマークは実装者のパネルを固定し、必須の非仕様管理アームを含み、決定論的実行ジャッジとして16と実動のOracleインスタンスを使用する。
論文 参考訳（メタデータ） (2026-08-19T22:17:31Z) - ModelEquivBench: Certifying Multi-Relational Evaluation of LLM-Generated Optimization Models [6.820882579439242]
マルチリレーショナル評価システムであるModelEquivBenchを提案する。
それぞれのエントリは、E0--E1、正のE2--E6結論の正確な有理証明のための関係適切なトレースまたは明示的なマップを持っている。
結果として得られるプロファイルは、粗いベースラインが表現しない区別を明らかにする。
論文 参考訳（メタデータ） (2026-07-31T13:55:09Z) - Evaluating and Guarding Citation Faithfulness in Agentic Scientific Synthesis [2.7092559671391]
OpenScholarやPaperQA2のようなエージェントLLMシステムは科学論文を読み、引用された回答を返す。
どちらもそのチェックの信頼性を監査しません。
私たちはそれが信頼できないこと、そしてこれが重要であることを示します。
本報告では,ゴールドアンコール評価プロトコルとデプロイ可能なガードについて述べる。
論文 参考訳（メタデータ） (2026-07-10T02:05:17Z) - Knowledge Index of Noah's Ark [63.143852586221534]
KINAは,261分野にわたる899項目のベンチマークである。
ボーナス・オン・バートーナメントがFOSDを弱く支配していることを示す。
トップモデルであるGemini-3.1-Pro-Previewは53.17%、Claude-Opus-4.6は49.92%、GPT-5.4は48.55%に達した。
論文 参考訳（メタデータ） (2026-06-03T17:06:49Z) - How Independent are Large Language Models? A Statistical Framework for Auditing Behavioral Entanglement and Reweighting Verifier Ensembles [46.63622714488747]
共有事前学習データ、蒸留、アライメントパイプラインは、隠れた振る舞い依存、潜伏絡みを誘導することができる。
実際には、これは相関した推論パターンと同期された障害として現れます。
ブラックボックス言語モデル間の行動絡みを監査するための統計的枠組みを開発する。
論文 参考訳（メタデータ） (2026-04-08T23:32:06Z) - Claw-Eval: Toward Trustworthy Evaluation of Autonomous Agents [66.97968363332465]
エージェントベンチマークの3つのギャップに対処するエンドツーエンド評価スイートであるClaw-Evalを紹介した。
Claw-Evalは3つのグループにまたがる9つのカテゴリにまたがる300の人間検証タスクで構成されている。
すべてのエージェントアクションは、3つの独立したエビデンスチャネルを通じて記録される。
論文 参考訳（メタデータ） (2026-04-07T17:43:18Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z) - Reliable Evaluation and Benchmarks for Statement Autoformalization [18.218951526592914]
改良されたメトリクス、堅牢なベンチマーク、体系的な評価を組み合わせた総合的なアプローチを提案する。
まず、評価指標の質を評価するための新しいデータセットであるProofNetVerifとともに、人間の判断と強く相関する自動メトリクスBEq+を紹介する。
ProofNet#はProofNetの修正版であり、RLM25は6つの形式化プロジェクトから619の新しい研究レベルの数学のペアである。
論文 参考訳（メタデータ） (2024-06-11T13:01:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。