論文の概要: Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs
- arxiv url: http://arxiv.org/abs/2607.12650v1
- Date: Tue, 14 Jul 2026 11:33:44 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-15 17:08:30.131766
- Title: Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs
- Title（参考訳）: Evidence-Grounded Verified Agentic Reasoning:A Path to Elimination LLM Hallucination in Empirical Inference through Tool-Attested Kernel Proofs
- Abstract要約: リーン4ベースのツールコールアーキテクチャが経験的クレームを管理するのにどのように使用できるかを示します。
検証されたすべての出力は、検査済みのツールコールと、有効な推論のカーネルチェックされたチェーンから構造的に下降する。
正式なサイドカーは、目標命題、ソーススコープ、エビデンス境界、証明義務、棄権条件を監査可能にする。
時間とともに、データセット、API、公開レコード、AI生成ドキュメントの型付きサイドカーは、この形式化の負担を再利用可能なインフラストラクチャに戻すことができる。
- 参考スコア（独自算出の注目度）: 0.564046562677526
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Tool access alone does not make LLM empirical reasoning governable: accepted outputs need not descend from attested evidence, and accepted deductions need not hold up under formal scrutiny. We present EG-VAR (Evidence-Grounded Verified Agentic Reasoning), a Lean 4-based tool-calling architecture in which the Lean kernel is the sole minter of Verified claims via tool-attestation axioms and declared source lifts. Every verified output structurally descends from an attested tool call (Thm. 3.1) and a kernel-checked chain of valid inference (Thm. 3.2); residual outputs are honest Abstain with a replayable audit trail. On a subcollection of TableBench numerical reasoning (n=120), EG-VAR attains 120/120 versus a 95% same-tool baseline; on counterfactual stress tests (5 domains x 2 models), EG-VAR stays 100% source-faithful while same-tool drops to 80-90% (no-tool 50-80%). With the LLM as deployment-time formalizer, residual semantic-formalization error is 3.3% on Sonnet and 1.7% on Opus. We position EG-VAR as a technical-governance interface for high-stakes empirical claims: a formal sidecar makes the target proposition, source scope, evidence boundary, proof obligation, and abstention condition auditable, eliminating unsupported Verified outputs today while turning formalization errors, lift and source-authority disputes, ambiguities, and abstentions into explicit audit targets. Over time, typed sidecars in datasets, APIs, public records, and AI-generated documents can amortize this formalization burden into reusable infrastructure.
- Abstract（参考訳）: 承認された出力は証明された証拠から降りる必要はなく、承認された控除は正式な精査の下では保たない。
EG-VAR(Evidence-Grounded Verified Agentic Reasoning)はリーン4ベースのツールコールアーキテクチャである。
検証されたすべての出力は、検査対象のツールコール(Thm.31)と有効な推論のカーネルチェックされたチェーン(Thm.32)から構造的に下降する。
TableBenchの数値推論(n=120)のサブコレクションでは、EG-VARは120/120と95%の同じツールベースラインに到達し、反ファクト的ストレステスト(5ドメイン x 2モデル)では、EG-VARは100%ソースフルで、同じツールは80-90%(ノーツール50-80%)に低下する。
LLMをデプロイメント時フォーマライザとして、残留セマンティックフォーマル化エラーはSonnetで3.3%、Opusで1.7%である。
フォーマルなサイドカーは、目標命題、ソーススコープ、エビデンス境界、証明義務、および禁忌条件を監査可能とし、今日、形式化されたエラー、リフトとソースオーソリティの論争、曖昧さ、および禁忌を明示的な監査対象にしつつ、現在、未確認の出力を排除します。
時間とともに、データセット、API、公開レコード、AI生成ドキュメントの型付きサイドカーは、この形式化の負担を再利用可能なインフラストラクチャに戻すことができる。
関連論文リスト
- Fidelity Is Not Enough: Dispatch-Level Instrumentation for Agentic Datasheet Extraction [6.419341495897254]
3つのコンポーネントに対して25のハンドキュレートされたクレームのエージェントベンチマークで、すべてのツールコールをログします。
ルールベースの障害帰属分類器と、2つのルールがどのツールが呼び出されたかのみをチェックするサイレント障害検出器の2つを構築しました。
論文 参考訳（メタデータ） (2026-08-28T15:25:12Z) - From Runnable to Verifiable: An Independent Reproducibility Study of LLM/Agent-Driven Vulnerability Validation Artifacts [4.093009863847175]
セキュリティ研究成果物は、エージェント駆動の脆弱性によってますます生成される。
公衆に入手可能で、飛行可能で、飛行可能で、飛行可能で、飛行確認済みの人工物とのギャップは、十分に測定されていない。
我々はこの文献について事前登録されたコンセンサス監査を行う。
論文 参考訳（メタデータ） (2026-08-10T13:05:02Z) - The LLM Proposes, the Executive Disposes: A Self-Verifying Agent Instrument that Dissociates Commitment Drift from Binding Drift in Long-Horizon Agents [0.0]
本稿では,ポストホックではなく構造的検証を行うためのエージェント機器を提案する。
組織ごとの書き込みエラー、レンダリングサイズ、あるいは塩漬けのカナリアエチョフロアが破られた場合、実行はすべて無効になる。
長期のエージェントが苦しむたびに、クリーンでシングル変数の結果が報告される。
論文 参考訳（メタデータ） (2026-08-04T15:10:37Z) - Deterministic Integrity Gates for LLM-Assisted Clinical Manuscript Preparation: An Auditable Biomedical Informatics Architecture [0.3823356975862005]
検証を伴うアーキテクチャペア生成を3つの原則に基づいて記述する。
この決定論的な分割は、整合性のある分類として組織化され、中核的な貢献である。
MedSci Skillsは、43のスキルのオープンソースツールキットで、21の決定論的階層を持ち、3つのパブリックデータセットパイプラインで評価されている。
論文 参考訳（メタデータ） (2026-06-08T13:51:04Z) - Pramana: A Protocol-Layer Treatment of Claim Verification in Autonomous Agent Networks [0.0]
確率的検証パターン(自己整合性投票、レビュアー LLM アンサンブル)は、人工物ではなく、判断を生成する。
Pramana は、ワイヤフォーマットの欠如を定義している。すべての連続エージェント出力は、タイプ付き ClaimAttestation でラップされ、4つの変種のうちの1つでラップされる。
プラマナは3つの対称性を再現したモデル(38,563個の到達可能な状態、0個の不変な違反)でTLCの下で徹底的に検証された。
論文 参考訳（メタデータ） (2026-05-19T17:00:33Z) - Hallucination as Exploit: Evidence-Carrying Multimodal Agents [10.441697487723568]
マルチモーダルエージェントはますます、スクリーンショットやドキュメント、Webページからツールコールを選択している。
本稿では,自由形式モデルテキストを不許容な証拠として扱うエビデンス搬送型マルチモーダルエージェント(ECA)を提案する。
ECAは不透明なモデルの信念を検証者、スキーマ、実装レベルで監査可能な残留物に変換する。
論文 参考訳（メタデータ） (2026-05-18T23:40:43Z) - FactReview: Evidence-Grounded Reviews with Literature Positioning and Execution-Based Claim Verification [57.196748998757954]
本稿では,クレーム抽出,文献位置決定,実行に基づくクレーム検証を組み合わせたエビデンスベースレビューシステムであるFactReviewを紹介する。
FactReviewは論文を提出すると、主要なクレームを特定し、その結果を報告し、論文の技術的な位置を明らかにするために近くの作業を取り出し、コードが利用可能であれば、リリースされたリポジトリを実行する。
その後、簡潔なレビューと、主要な請求を5つのラベルのうち1つに割り当てるエビデンスレポートを生成する。
論文 参考訳（メタデータ） (2026-04-05T11:45:22Z) - CiteAudit: You Cited It, But Did You Read It? A Benchmark for Verifying Scientific References in the LLM Era [51.63024682584688]
大規模言語モデル (LLM) は新たなリスクを導入している。
本稿では,科学文献における幻覚的引用のための総合的なベンチマークおよび検出フレームワークについて紹介する。
我々のフレームワークは、精度と解釈可能性の両方において、先行手法を著しく上回っている。
論文 参考訳（メタデータ） (2026-02-26T19:17:39Z) - Preventing the Collapse of Peer Review Requires Verification-First AI [49.995126139461085]
我々は、真理結合、すなわち、過度に科学的真理をトラックする場所のスコアの厳密さを提案する。
プロキシ・ソブリン評価に向けた相転移を駆動する2つの力の形式化を行う。
論文 参考訳（メタデータ） (2026-01-23T17:17:32Z) - Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
大規模言語モデル(LLM)は、現実のファクトチェックシステムにますます多くデプロイされている。
FactArenaは、完全に自動化されたアリーナスタイルの評価フレームワークである。
本研究では,静的クレーム検証精度とエンドツーエンドのファクトチェック能力の相違点を明らかにした。
論文 参考訳（メタデータ） (2026-01-06T02:51:56Z) - Inferring multiple helper Dafny assertions with LLMs [47.33158055894705]
本研究では,Dafnyプログラムにおけるヘルパーアサーションの欠落を自動的に推測するために,Large Language Modelsの使用について検討する。
推論の難易度を分析するために,アサーション型の分類を導入した。
その結果、自動アサーション推論は証明工学の労力を大幅に削減できることが示された。
論文 参考訳（メタデータ） (2025-10-31T09:45:39Z) - Lyra: Orchestrating Dual Correction in Automated Theorem Proving [63.115422781158934]
Lyraは新しいフレームワークで、ツール補正とConjecture Correctionという2つの異なる補正メカニズムを採用している。
ツール補正は幻覚の緩和に寄与し、それによって証明の全体的な精度が向上する。
Conjecture Correctionは命令で生成を洗練させるが、ペア化された(生成、エラー、改善)プロンプトは収集しない。
論文 参考訳（メタデータ） (2023-09-27T17:29:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。