mlsanityData to 14 Oct 2026

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

arXiv 2607.12650 ↗First posted 14 Jul 2026cs.LG cs.AI cs.CYcited by 2

On the map: LLM reasoning → Reasoning benchmarks and evaluation

also in 1 more
Abstract (arXiv)

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.

Key facts. Cited by 2 papers in the map (data through 14 Oct 2026). Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning. Builds on 21 of its 57 references that are in the map. First posted on arXiv 14 Jul 2026.

Builds on

21 of 57 references.

References · 21

  1. 2023A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questionscited by 1,601
  2. 2022When Not to Trust Language Models: Investigating Effectiveness of Parametric and Non-Parametric Memoriescited by 1,128
  3. 2023Adaptive Chameleon or Stubborn Sloth: Revealing the Behavior of Large Language Models in Knowledge Conflictscited by 341
  4. 2023Chain-of-Verification Reduces Hallucination in Large Language Modelscited by 324
  5. 2022RARR: Researching and Revising What Language Models Say, Using Language Modelscited by 287
  6. 2023FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarioscited by 251
  7. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
  8. 2024Long-form factuality in large language modelscited by 155
  9. 2024TableBench: A Comprehensive and Complex Benchmark for Table Question Answeringcited by 128
  10. 2024ClashEval: Quantifying the tug-of-war between an LLM's internal prior and external evidencecited by 113
  11. 2024FaithEval: Can Your Language Model Stay Faithful to Context, Even If "The Moon is Made of Marshmallows"cited by 86
  12. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 60
9 more
  1. 2024Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalizationcited by 55
  2. 2021ProoFVer: Natural Logic Theorem Proving for Fact Verificationcited by 53
  3. 2024DYNAMICQA: Tracing Internal Knowledge Conflicts in Language Modelscited by 34
  4. 2023Counterfactual reasoning: Testing language models' understanding of hypothetical scenarioscited by 27
  5. 2013Homotopy Type Theory: Univalent Foundations of Mathematicscited by 8
  6. 2025Attestable Audits: Verifiable AI Safety Benchmarks Using Trusted Execution Environmentscited by 8
  7. 2025VET Your Agent: Towards Host-Independent Autonomy via Verifiable Execution Tracescited by 4
  8. 2024TabVer: Tabular Fact Verification with Natural Logiccited by 3
  9. 2015Automating change of representation for proofs in discrete mathematicscited by 1

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 2.

2 papers.

  1. 2026Beyond Natural Language: An Agent-Native Language for Autonomous Sciencecited by 0
  2. 2026RSure-Agent: Reliable Use of Tool Observations for Remote Sensing Agentscited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2026VeriHarness: Scaling Agentic Verification for Long-Horizon Tasks
  2. 2026MAVEN: Multi-Agent Verification-Elaboration Network with In-Step Epistemic Auditing
  3. 2026Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
  4. 2026CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
  5. 2026Grading the Graders: Verification Autonomy Levels (L0-L5) for LLM Reasoning
  6. 2026MAVEN: Improving Generalization in Agentic Tool Calling
  7. 2026A2RBench: An Automatic Paradigm for Formally Verifiable Abstract Reasoning Benchmark Generation
  8. 2026Tool Receipts, Not Zero-Knowledge Proofs: Practical Hallucination Detection for AI Agents