基于证据的可验证智能推理：通过工具验证内核证明消除经验推理中语言模型幻觉的途径
Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs
AI总结：
研究旨在消除语言模型经验推理中的幻觉，提出基于Lean 4的EG-VAR工具调用架构，通过工具验证公理等生成可验证声明，经实验在数值推理等测试中表现良好，定位为高风险经验声明的技术治理接口，可审计相关条件并转化错误为审计目标。
AI中文摘要：
仅靠工具访问并不能使语言模型的经验推理可控：被接受的输出不一定来自经证实的证据，被接受的推导在形式审查下也不一定成立。我们提出了EG-VAR（基于证据的可验证智能推理），这是一种基于Lean 4的工具调用架构，其中Lean内核是通过工具验证公理和声明的源提升来唯一生成可验证声明的。每个经过验证的输出在结构上都来自经过验证的工具调用和内核检查的有效推理链；剩余输出是带有可重放审计跟踪的诚实弃权。在TableBench数值推理的一个子集中，EG-VAR达到了120/120，而相同工具的基线为95%；在反事实压力测试中，EG-VAR保持100%的源忠实度，而相同工具的下降到80-90%（无工具为50-80%）。以语言模型作为部署时的形式化工具，在Sonnet上剩余语义形式化错误为3.3%，在Opus上为1.7%。我们将EG-VAR定位为高风险经验声明的技术治理接口：一个形式化的辅助工具使目标命题、源范围、证据边界、证明义务和弃权条件可审计，消除了目前无根据的已验证输出，同时将形式化错误、提升和源权威争议、歧义以及弃权转化为明确的审计目标。随着时间的推移，数据集中、API、公共记录和人工智能生成文档中的类型化辅助工具可以将这种形式化负担分摊到可重复使用的基础设施中。
英文摘要：
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.
