Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs
Junyu Ren
cs.LG
Jul 14, 2026 · v1
cs.AI cs.CY cs.SE
TL;DR
Uses the Lean 4 kernel as sole minter of Verified empirical claims, type-checking LLM-proposed proof tactics under tool-attestation axioms.
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.
Problem
LLMs hallucinate empirical facts and, even with tool access, may accept outputs not derived from attested evidence or that fail formal scrutiny. Ensuring verifiable, auditable empirical claims requires structural rather than statistical guarantees.
Approach
EG-VAR is a Lean 4-based tool-calling architecture with a four-layer stack: trusted deterministic tools attest storage facts, per-source lifts imported as Lean axioms map facts to world claims, the Lean kernel type-checks proofs and is the sole minter of Verified claims via a mkVerified rule requiring an attestation hypothesis, and an untrusted LLM proposes proof tactics. Every Verified output must structurally descend from an attested tool call and a kernel-checked inference chain; rejected outputs yield honest abstention with a replayable Lean proof artifact. The LLM also acts as a deployment-time formalizer proposing typed goals.
Results
On TableBench numerical reasoning (n=120) EG-VAR attained 120/120 versus a 95% same-tool baseline. On counterfactual stress tests EG-VAR stayed 100% source-faithful while same-tool dropped to 80-90% and no-tool to 50-80%. With LLM formalization, residual semantic-formalization error was 3.3% (Sonnet) and 1.7% (Opus).
| Rung | Match |
|---|
| Table-only | 107/120 (89.2%) |
| Tools-open | 113/120 (94.2%) |
| Tools-curated | 114/120 (95.0%) |
| EG-VAR | 120/120 (100.0%) |
TableBench Tier 1 match rate by rung
| Category | Sonnet | Opus |
|---|
| Correct | 84.2% | 87.5% |
| Ambiguous claim (logged) | 4.2% | 4.2% |
| Semantic formalizer error | 3.3% | 1.7% |
| Honest abstain | 2.5% | 5.0% |
| Solver gave up | 4.2% | 0.0% |
Tier 2 end-to-end outcome categories
