用形式化证明杜绝大模型推理幻觉，确保每步结论都有证据可查。
Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs
- 通过工具调用与形式化内核结合，只允许经验证的输出生成
- 在120个数学题中实现100%正确率，远超基线95%
- 适合高风险决策场景，让推理过程可审计、可复现
仅依赖工具访问无法控制大模型的实证推理：被接受的输出未必源于可信证据，推导也未必经得起形式检验。我们提出EG-VAR（证据根基的验证代理推理），基于Lean 4的工具调用架构，以Lean内核为唯一验证声明的生成者，通过工具证实公理和源码提升机制。每个已验证输出都严格源自经证实的工具调用（定理3.1）和内核验证的推理链（定理3.2）；未验证输出则诚实放弃，并保留可重播的审计轨迹。在TableBench子集（n=120）上，EG-VAR达成120/120正确率，优于同工具基线95%；在5个领域的反事实压力测试中，EG-VAR保持100%源忠实，而同工具下降至80-90%（无工具为50-80%）。以LLM作为部署时的形式化器，语义-形式化误差为Sonnet 3.3%、Opus 1.7%。EG-VAR定位为高价值实证主张的技术治理接口：形式化侧车使目标命题、源范围、证据边界、证明义务和弃权条件均可审计，消除当前未经支持的验证输出，同时将形式化错误、提升与源权威争议、模糊性及弃权转化为明确审计目标。长期来看，数据集、API、公共记录与生成文档中的类型化侧车可摊薄此形式化负担，形成可复用基础设施。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。