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

AI summary

Overview

• Research area: Verifiable AI and AI governance, at the intersection of LLM agents, formal verification, and empirical data reasoning. The paper is published under arXiv:2607.12650v1 [cs.LG] (14 Jul 2026), category Machine Learning, by Junyu Ren (Committee on Computational and Applied Mathematics, University of Chicago).
• Technical level: Advanced. It assumes familiarity with Lean 4, dependent type theory (Martin-Löf dependent sums, Curry–Howard correspondence), proof-assistant kernels, and axiom whitelisting, though the paper's argument is stated in plain language about trust and audit.
• One-sentence scope: It presents and empirically evaluates EG-VAR, a Lean 4-based agentic architecture in which a proof-assistant kernel is the only entity allowed to label an empirical claim "Verified," with tables as the first end-to-end substrate.

What This Paper Is About

Large language models hallucinate when they reason about empirical facts, and simply giving them tool access does not fix this: the paper argues that with tools alone, accepted outputs still need not descend from attested evidence, and accepted deductions still need not survive formal scrutiny. EG-VAR attacks both failures structurally by forcing every "Verified" output to descend from a recorded, runtime-attested tool call and every accepted derivation to type-check in the Lean 4 kernel; anything else surfaces as an honest "Abstain" with a replayable audit trail.

Key Contributions

1. The EG-VAR architecture. A four-layer stack — L1 deterministic tool layer, L2 audited per-source formalization, L3 Lean 4 kernel, L4 untrusted solver LLM — in which a single mint rule, mkVerified, requires an Attested_T hypothesis that only the runtime can introduce, so the solver LLM cannot synthesize evidence. The paper states this is, to its knowledge, the first proof-assistant-verified architecture in Lean 4 for this setting.
2. Two structural safety theorems, plus a companion whitelist discipline. Theorem 3.1 states that any runtime return with verdict Verified, where the generated Lean file is whitelist-compliant for the source, has every runtime-emitted observation-leaf axiom backed by a prior tool execution and every other axiom dependency in the fixed EG-VAR prelude, standard Lean 4 core axioms, or the per-source lifts Λ(s). Theorem 3.2 states that every inference step accepted as part of a Verified output type-checks in Lean 4's kernel under the declared axiom set. A whitelist-compliant module is defined by four axiom buckets (B1–B4) with no sorry variant in the closure and at least one trust-artifact witness.
3. A three-tier empirical evaluation on TableBench, separating formal safety (kernel acceptance against committed trust artifacts) from semantic faithfulness (the formalized goal matches the natural-language claim, measured by answer_match against frozen gold answers), and releasing a curator-grade (claim, gold goal) corpus intended as fine-tuning data.
4. A governance translation. Three structural properties — auditable evidence trails via replayable per-claim Lean proofs (G1), typed uncertainty under no-upcast grade discipline over {Verified, Supported, Plausible, Speculative} (G2), and externally specifiable refusal thresholds via honest abstention (G3).

Main Findings

• Tier 1 closes the same-tool gap to zero. On n = 120 unambiguous TableBench claims with claude-sonnet-4-6 at temperature 0, the ladder is Table-only 107/120 (89.2%), Tools-open 113/120 (94.2%), Tools-curated 114/120 (95.0%), and EG-VAR 120/120 (100.0%). EG-VAR's score is joint formal safety and semantic faithfulness; the same-tool baseline plateaus at 114/120 on semantic faithfulness alone and has no formal-safety surface, since baselines cannot abstain.
• Tier 1.5 shows 100% source-faithfulness under counterfactual pressure. On the extreme-flip panel (n = 20 binary-compare and direction claims), EG-VAR is 20/20 on both Sonnet and Haiku; Table-only is 16/20 (Sonnet) and 15/20 (Haiku); Tools-open and Tools-curated are 16/20 on Sonnet and 20/20 on Haiku. On the subtle-flip panel, EG-VAR is again 20/20 on both models, while Table-only drops to 10/20 (Sonnet) and 8/20 (Haiku), and Tools-open and Tools-curated reach 18/20 (Sonnet) and 20/20 (Haiku). Residual errors are all prior-override, with no wrong-other cases.
• Panel construction and injection regimes. Each Tier 1.5 panel is 5 domains × 2 entity-pair injections × 3 claim shapes = 30 claims (20 binary-compare plus direction, and 10 cell-lookup; the cell-lookup set does not trigger prior-override and is excluded from the reported n = 20). The extreme-flip panel uses magnitude-10-plus reversals (Italy GDP → $50, Patriots → 0–16, Sinopec → $50); the subtle-flip panel uses 10–25% reversals (Mont Blanc → 4500 m vs Monte Rosa 4634 m, Madrid GDP 90 vs Berlin 95) over stable-scalar priors.
• Tier 2 bounds formalizer error with the LLM as formalizer. On n = 120 with the runtime invoking the LLM formalizer (claude-sonnet-4-6 at temperature 0, and Opus), the six-category decomposition is: Correct 84.2% (Sonnet) and 87.5% (Opus); Ambiguous claim (logged) 4.2% and 4.2%; Benchmark gold error (surfaced) 1.7% and 1.7%; Semantic formalizer error 3.3% and 1.7%; Honest abstain 2.5% and 5.0%; Solver gave up 4.2% and 0.0%.
• Formal safety is model-independent; semantic faithfulness is not. The paper states that formal safety holds regardless of which LLM proposed the goal type (Theorem 3.1), whereas semantic faithfulness is operational and model-dependent, so the 3.3% Sonnet and 1.7% Opus figures are the pure formalizer-error rates.
• Tier 2 still holds under counterfactual pressure. Re-running the Tier 2 Sonnet pipeline on the Tier 1.5 extreme-flip panel (n = 20) yields 20/20 source-faithful Verified outputs, matching the gold-formalization rung, while the Tier 1.5 same-tool baseline drops to 16/20 on the same tables.
• The same-tool architectures fail on prior conflict, not on tool absence. The paper reports frontier-model confirmation bias — dismissing retrieved evidence that conflicts with parametric memory — and notes its own counterfactual stress tests reproduce the pattern at roughly 12–15%, robust to an explicit "according to the table" source-anchoring cue.
• Comparisons against prior systems. Table 1 places EG-VAR as the only row combining a proof-assistant kernel with tool-attested grounding and honest abstention on rejection, alongside TabVer, ProoFVer, FoVer, AWS Bedrock, AlphaProof, DeepSeek-Prover, Attestable Audits, and Proofs of Autonomy. Against ClashEval, the paper reports prior-override above 60% on incorrect retrieved content, with Context-Bias 0.157 for Opus, 0.201 for Sonnet, 0.245 for Gemini 1.5, and 0.304 for GPT-4o.
• Not reported. The paper content does not report wall-clock latency, token cost, energy use, or human-subject evaluation; its stated evaluations use temperature 0, 1-rep canonical runs for EG-VAR with corroborating multi-rep partial runs, and a frozen curator fixture for Tiers 1 and 1.5.

Methodology in Plain English

The system splits reasoning into layers with different trust levels. A deterministic tool layer answers fixed queries against a source (for tables: cell lookups, filtered aggregates, selection operators) and packages each answer with a runtime witness recording the query, the source identity, and the result — only the runtime can create these witnesses.

A per-source formalization layer, written and audited offline by a curator, is a list of typed "lifts" that say which low-level storage facts support which high-level world claims (for example, that a cell at row r, column "state" with value "alabama" supports "Alabama has the highest HIV incidence rate"). These lifts are imported into Lean as axioms, so the language describes the world rather than the storage vehicle — a separation the paper attributes to Codd's split between a relational schema and the predicates it serves.

The Lean 4 kernel is the only entity that can mint a Verified label. Its single mint rule, mkVerified, demands an attested payload hypothesis, and the solver LLM cannot produce such a term — it can only consume ones introduced by tool calls during the loop. The solver LLM receives a typed goal, proposes proof tactics, and receives kernel rejections that drive revision. The certified answer is extracted as the witness of a dependent sum: a question like "which entity has property P?" becomes a goal of type Σ (e : String) (v : Value), Evidence Verified (… e v), and the surface answer is the first projection of the kernel-checked witness.

In the end-to-end loop, an analyst LLM drafts a guide, a formalizer LLM proposes the goal type, and the solver iterates tool calls and proof attempts until the kernel accepts (returning a proof object of a Lean file, an evidence list, and a step history) or the loop exhausts its step budget and the system abstains. Evaluation is run on a four-rung ladder to isolate each ingredient: Table-only, Tools-open, Tools-curated (the same tool surface as EG-VAR), and EG-VAR.

Why This Matters

Impact on research. The paper reframes hallucination in empirical inference as a structural problem rather than a statistical one: Theorem 3.1 is claimed to rule out unsupported Verified outputs model-independently, so an arbitrarily wrong solver can never produce a verified-but-unsupported output. This offers an alternative to both symbolic factual verifiers (which carry mapping-error risk) and hardware or execution-attestation systems (which attest provenance rather than claim truth, and are described as complementary). It also proposes that verification cost is amortized: each per-source lift is audited once at curation time and reused across all later claims grounded in that source, so formalization never enters the per-query inference loop.

Real-world applications (as the paper frames them):

• High-stakes empirical claims over structured sources, such as public-health or epidemiological statistics — the worked example in the paper is an argmax over state HIV incidence rates.
• Spreadsheet and table-based analytical reporting, including sports and economic comparisons like the "Brazil scored on average x more goals in the 2018 opener than Italy" motivating example.
• Datasets, APIs, public records, and AI-generated documents that could one day carry typed "formal sidecars" alongside prose, letting recipients re-check key claims offline.
• Downstream policy enforcement, where a pipeline can require Verified and reject Abstain, or admit Abstain as a flagged state, without re-implementing the trust boundary.

Industry relevance. The governance argument targets regulated or audited settings: a third party with the kernel, per-source lifts, and tool adapter can re-typecheck an accepted claim from the attested payload without re-running the model, and the trust artifact set (L1 vocabulary, lifts, tool adapter, kernel) is enumerable. The paper also argues that as sources move from CSV toward SQL views, OpenAPI schemas, knowledge graphs, and typed registries, the per-source lifting burden falls, positioning formalization as reusable infrastructure rather than per-query overhead.

Future Directions

1. Fine-tune the NL formalizer on the curator-provided (claim, gold type) corpus with kernel acceptance as the reward signal — an accuracy intervention that the paper says tightens the Tier 2 residual rate without weakening Theorem 3.1.
2. Multi-source attestation with conflict-downgrade rules, for example downgrading Verified to Supported when disagreement between sources is detected.
3. A cross-substrate panel (KG-grounded, SQL-grounded) to test the L1/L2 portability claim, since all reported evaluations are on single TableBench tables and multi-source, knowledge-graph, and streaming sources are explicitly out of scope.
4. Typed sidecars in the wild. The longer-run bet is that as upstream providers run EG-VAR-like pipelines, formalization becomes mechanized and data arrives already bearing kernel-checked Verified instructions, moving the formalization burden out of the inference loop.

Open items the paper flags as unresolved: semantic faithfulness of the formalization to the natural-language claim, the possibility of a semantically wrong but audited lift certifying a wrong formalized claim, and source-data corruption that passes the runtime identity-cell validator — all three are stated as outside the current safety theorems.

Target Audience

Researchers and practitioners working on verifiable AI, AI governance, and trustworthy LLM agents; formal-methods and proof-assistant researchers interested in extending Lean 4 verification from self-contained mathematics to externally grounded empirical claims; and policy, audit, or compliance engineers who need measurable, replayable evidence boundaries around automated claims about data. Readers without a background in dependent type theory will still follow the architecture and results, but the safety-theorem and whitelist details assume familiarity with proof-assistant internals.

Authors’ 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.