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

arXiv: https://arxiv.org/abs/2607.12650 · HTML: https://mlsanity.com/paper/2607.12650/

## 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.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)
- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 21 of 21)

- [A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questions](https://mlsanity.com/paper/2311.05232/) (2023)
- [When Not to Trust Language Models: Investigating Effectiveness of Parametric and Non-Parametric Memories](https://mlsanity.com/paper/2212.10511/) (2022)
- [Adaptive Chameleon or Stubborn Sloth: Revealing the Behavior of Large Language Models in Knowledge Conflicts](https://mlsanity.com/paper/2305.13300/) (2023)
- [Chain-of-Verification Reduces Hallucination in Large Language Models](https://mlsanity.com/paper/2309.11495/) (2023)
- [RARR: Researching and Revising What Language Models Say, Using Language Models](https://mlsanity.com/paper/2210.08726/) (2022)
- [FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarios](https://mlsanity.com/paper/2307.13528/) (2023)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Long-form factuality in large language models](https://mlsanity.com/paper/2403.18802/) (2024)
- [TableBench: A Comprehensive and Complex Benchmark for Table Question Answering](https://mlsanity.com/paper/2408.09174/) (2024)
- [ClashEval: Quantifying the tug-of-war between an LLM's internal prior and external evidence](https://mlsanity.com/paper/2404.10198/) (2024)
- [FaithEval: Can Your Language Model Stay Faithful to Context, Even If "The Moon is Made of Marshmallows"](https://mlsanity.com/paper/2410.03727/) (2024)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [ProoFVer: Natural Logic Theorem Proving for Fact Verification](https://mlsanity.com/paper/2108.11357/) (2021)
- [DYNAMICQA: Tracing Internal Knowledge Conflicts in Language Models](https://mlsanity.com/paper/2407.17023/) (2024)
- [Counterfactual reasoning: Testing language models' understanding of hypothetical scenarios](https://mlsanity.com/paper/2305.16572/) (2023)
- [Homotopy Type Theory: Univalent Foundations of Mathematics](https://mlsanity.com/paper/1308.0729/) (2013)
- [Attestable Audits: Verifiable AI Safety Benchmarks Using Trusted Execution Environments](https://mlsanity.com/paper/2506.23706/) (2025)
- [VET Your Agent: Towards Host-Independent Autonomy via Verifiable Execution Traces](https://mlsanity.com/paper/2512.15892/) (2025)
- [TabVer: Tabular Fact Verification with Natural Logic](https://mlsanity.com/paper/2411.01093/) (2024)
- [Automating change of representation for proofs in discrete mathematics](https://mlsanity.com/paper/1505.02449/) (2015)

## Built on by (most cited first, 2 of 2)

- [Beyond Natural Language: An Agent-Native Language for Autonomous Science](https://mlsanity.com/paper/2609.25421/) (2026)
- [RSure-Agent: Reliable Use of Tool Observations for Remote Sensing Agents](https://mlsanity.com/paper/2610.04836/) (2026)

## 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.