Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs

• URL: http://arxiv.org/abs/2607.12650v1
• Date: Tue, 14 Jul 2026 11:33:44 GMT
• Title: Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs
• Abstract summary: We show how a Lean 4-based tool-calling architecture can be used to govern empirical claims.<n>Every verified output structurally descends from an attested tool call and a kernel-checked chain of valid inference.<n>A formal sidecar makes the target proposition, source scope, evidence boundary, proof obligation, and abstention condition auditable.<n>Over time, typed sidecars in datasets, APIs, public records, and AI-generated documents can amortize this formalization burden into reusable infrastructure.
• Score: 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.

Related papers

• Fidelity Is Not Enough: Dispatch-Level Instrumentation for Agentic Datasheet Extraction [6.419341495897254]
  We log every tool call in an agentic benchmark of 25 hand-curated claims over three components, with 12 more on a fourth, 37 in all.<n>We build two instruments: a rule-based failure-attribution classifier, and a silent-failure detector whose two rules check only which tools were called, never the extracted value.
  arXiv  Detail & Related papers  (2026-08-28T15:25:12Z)
• From Runnable to Verifiable: An Independent Reproducibility Study of LLM/Agent-Driven Vulnerability Validation Artifacts [4.093009863847175]
  Security research artifacts are increasingly produced by agent-driven vulnerabilities.<n>The gap between emphpublicly available, emphrunnable, emphsignal-producing, and emphsemantically confirmed artifacts is poorly measured.<n>We conduct a pre-registered consensus audit of this literature.
  arXiv  Detail & Related papers  (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]
  We present an agent instrument built so that verification is structural rather than post-hoc.<n>Every run invalidates itself when per-organ write-error, render-size, or salted-canary-echo floors are breached.<n>We report a clean, single-variable result on a failure every long-horizon agent suffers.
  arXiv  Detail & Related papers  (2026-08-04T15:10:37Z)
• Deterministic Integrity Gates for LLM-Assisted Clinical Manuscript Preparation: An Auditable Biomedical Informatics Architecture [0.3823356975862005]
  We describe an architecture pairing generation with verification, resting on three principles.<n>This determinism-where-possible split, organized as an integrity-gate taxonomy, is the core contribution.<n> MedSci Skills is an open-source toolkit of 43 skills with a 21-detector deterministic tier, evaluated on three public-dataset pipelines.
  arXiv  Detail & Related papers  (2026-06-08T13:51:04Z)
• Pramana: A Protocol-Layer Treatment of Claim Verification in Autonomous Agent Networks [0.0]
  Production verification today splits into two halves: Probabilistic verdict patterns (self-consistency voting, reviewer LLM ensembles) produce judgments, not artifacts.<n>Pramana defines the missing wire format. Every consequential agent output is wrapped in a typed ClaimAttestation with one of four variants.<n>Pramana exhaustively verified under TLC across three symmetry-reduced models: 38,563 distinct reachable states, zero invariant violations.
  arXiv  Detail & Related papers  (2026-05-19T17:00:33Z)
• Hallucination as Exploit: Evidence-Carrying Multimodal Agents [10.441697487723568]
  Multimodal agents increasingly choose tool calls from screenshots, documents, and webpages, where a false perceptual claim can turn from an answer-quality error into an authorization failure.<n>We propose evidence-carrying multimodal agents (ECA), which treat free-form model text as inadmissible evidence.<n>ECA converts opaque model belief into auditable residuals at the verifier, schema, and implementation levels.
  arXiv  Detail & Related papers  (2026-05-18T23:40:43Z)
• FactReview: Evidence-Grounded Reviews with Literature Positioning and Execution-Based Claim Verification [57.196748998757954]
  We present FactReview, an evidence-grounded reviewing system that combines claim extraction, literature positioning, and execution-based claim verification.<n>Given a submission, FactReview identifies major claims and reported results, retrieves nearby work to clarify the paper's technical position, and, when code is available, executes the released repository.<n>It then produces a concise review and an evidence report that assigns each major claim one of five labels: Supported, Supported by the paper, Partially supported, In conflict, or Inconclusive.
  arXiv  Detail & Related papers  (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]
  Large language models (LLMs) introduce a new risk: fabricated references that appear plausible but correspond to no real publications.<n>We present the first comprehensive benchmark and detection framework for hallucinated citations in scientific writing.<n>Our framework significantly outperforms prior methods in both accuracy and interpretability.
  arXiv  Detail & Related papers  (2026-02-26T19:17:39Z)
• Preventing the Collapse of Peer Review Requires Verification-First AI [49.995126139461085]
  We propose truth-coupling, i.e. how tightly venue scores track latent scientific truth.<n>We formalize two forces that drive a phase transition toward proxy-sovereign evaluation.
  arXiv  Detail & Related papers  (2026-01-23T17:17:32Z)
• Towards Comprehensive Stage-wise Benchmarking of Large Language Models in Fact-Checking [64.97768177044355]
  Large Language Models (LLMs) are increasingly deployed in real-world fact-checking systems.<n>We present FactArena, a fully automated arena-style evaluation framework.<n>Our analyses reveal significant discrepancies between static claim-verification accuracy and end-to-end fact-checking competence.
  arXiv  Detail & Related papers  (2026-01-06T02:51:56Z)
• Inferring multiple helper Dafny assertions with LLMs [47.33158055894705]
  We investigate the use of Large Language Models to automatically infer missing helper assertions in Dafny programs.<n>We introduce a taxonomy of assertion types to analyze inference difficulty.<n>Results show that automated assertion inference can substantially reduce proof engineering effort.
  arXiv  Detail & Related papers  (2025-10-31T09:45:39Z)
• Lyra: Orchestrating Dual Correction in Automated Theorem Proving [63.115422781158934]
  Lyra is a new framework that employs two distinct correction mechanisms: Tool Correction and Conjecture Correction. Tool Correction contributes to mitigating hallucinations, thereby improving the overall accuracy of the proof. Conjecture Correction refines generation with instruction but does not collect paired (generation, error & refinement) prompts.
  arXiv  Detail & Related papers  (2023-09-27T17:29:41Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.