Adnan KhanAdnanProduct & AI
San Francisco Bay Area
Get in touch

Source note3 min read

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

Source

arXiv

arxiv.org/abs/2607.12650v1

Read the source

Source

Plain-Language Brief

Junyu Ren presents EG-VAR (Evidence-Grounded Verified Agentic Reasoning), a tool-calling architecture that aims to make empirical reasoning in large language models (LLMs) more trustworthy and auditable. The system ensures that every verified output is supported by attested evidence and valid inference, and it provides an audit trail for residual outputs. EG-VAR was tested on numerical reasoning problems and counterfactual stress tests, where it outperformed a baseline system in terms of source faithfulness.

What the Document Says

  • The paper presents EG-VAR, a tool-calling architecture built using Lean 4.
  • The Lean kernel is responsible for verifying claims through tool-attestation axioms and declared source lifts.
  • Every verified output in EG-VAR structurally descends from an attested tool call and a chain of valid inference checked by the kernel.
  • Residual outputs are honest Abstain with a replayable audit trail.
  • On a subcollection of TableBench numerical reasoning problems (n=120), EG-VAR achieved 120/120 versus a 95% same-tool baseline.
  • On counterfactual stress tests across 5 domains and 2 models, EG-VAR maintained 100% source-faithfulness while the same-tool dropped to 80-90% (no-tool dropped to 50-80%).
  • With the LLM as deployment-time formalizer, residual semantic-formalization error is 3.3% on Sonnet and 1.7% on Opus.
  • EG-VAR is positioned as a technical governance interface for high-stakes empirical claims, providing an auditable record of the target proposition, source scope, evidence boundary, proof obligation, and abstention condition.

Key Concepts Mentioned

  • Evidence-Grounded Verified Agentic Reasoning (EG-VAR)
  • large language models (LLMs)
  • tool-calling architecture
  • Lean 4
  • kernel-checked chain of valid inference
  • attested tool call
  • audit trail

Claims Made by the Document

  • EG-VAR attains 120/120 on a subcollection of TableBench numerical reasoning problems.
  • On counterfactual stress tests, EG-VAR stays 100% source-faithful while same-tool drops to 80-90% (no-tool drops to 50-80%).

Evidence Used

  • Results from a subcollection of TableBench numerical reasoning problems and counterfactual stress tests.

Methods / Approach

  • Use of Lean 4-based tool-calling architecture
  • Kernel checking of valid inference chains
  • Tool attestation axioms and declared source lifts

Limitations Stated by the Authors

UNKNOWN

Limitations Noted by the Agent

Agent interpretation — not from the source.

UNKNOWN

Open Questions

UNKNOWN

Notes for Future Q&A

May include interpretation. Labeled where it does.

UNKNOWN

Raw Abstract / Excerpt

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.