Adnan KhanAdnanProduct & AI
San Francisco Bay Area
Get in touch

Source note2 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

The paper introduces EG-VAR, a tool-calling architecture that aims to make the reasoning of a large language model (LLM) more trustworthy by verifying all outputs through tool-attestation axioms and kernel checks. The system achieves high accuracy on numerical reasoning tasks and maintains source faithfulness during counterfactual stress tests. It also reduces residual semantic-formalization errors on Sonnet and Opus datasets.

What the Document Says

  • EG-VAR is a Lean 4-based tool-calling architecture.
  • The Lean kernel verifies claims via tool-attestation axioms and declared source lifts.
  • Every verified output structurally descends from an attested tool call and a kernel-checked chain of valid inference (Thm. 3.1, Thm. 3.2).
  • Residual outputs are honest Abstain with a replayable audit trail.
  • EG-VAR achieves 100% accuracy on a subcollection of TableBench numerical reasoning tasks compared to a 95% same-tool baseline.
  • In counterfactual stress tests, EG-VAR maintains 100% source faithfulness while same-tool drops to 80-90%, and no-tool drops 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 aims to be a technical-governance interface for high-stakes empirical claims.
  • The formal sidecar makes the target proposition, source scope, evidence boundary, proof obligation, and abstention condition auditable.
  • Over time, typed sidecars in datasets, APIs, public records, and AI-generated documents can amortize this formalization burden into reusable infrastructure.

Key Concepts Mentioned

  • Large Language Model (LLM)
  • EG-VAR
  • Tool-attestation axioms
  • Lean 4
  • Verified claims
  • TableBench
  • Counterfactual stress tests
  • Sonnet
  • Opus
  • Formal sidecar

Claims Made by the Document

  • EG-VAR achieves high accuracy on numerical reasoning tasks.
  • EG-VAR maintains source faithfulness during counterfactual stress tests.
  • Residual semantic-formalization error is reduced with EG-VAR on Sonnet and Opus datasets.

Evidence Used

  • Results from TableBench numerical reasoning tasks
  • Counterfactual stress tests results
  • Results from Sonnet and Opus datasets

Methods / Approach

UNKNOWN

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.