Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs
Junyu Ren
Why It Matters
What makes this one worth your time
This work is relevant for AI researchers and engineers focused on improving the reliability and trustworthiness of LLM outputs, particularly in high-stakes applications.
EG-VAR provides a framework for verified reasoning in LLMs to prevent hallucinations by grounding outputs in tool-attested evidence.
Summary
The paper introduces EG-VAR, a Lean 4-based architecture for verified reasoning in LLMs, aiming to eliminate hallucinations in empirical inference by ensuring outputs are grounded in tool-attested evidence and verified through a kernel-checked chain of inference.
Key contributions
- Development of the EG-VAR architecture for evidence-grounded reasoning.
- Demonstration of improved source-faithfulness and reduced formalization errors in empirical inference tasks.
Notable insights
- The use of a Lean 4-based architecture to ensure that every verified output is grounded in attested tool calls and valid inference chains.
- The introduction of a formal sidecar to make propositions, evidence boundaries, and proof obligations auditable.
Possible limitations
- Not stated in the abstract
Abstract
arXiv:2607.12650v1 Announce Type: cross 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.