← 返回 PaperDaily 大模型与智能体

反事实压力下仍100%忠实，LLM事实核验新范式

这篇论文最狠的地方，不是“答对了”，而是把“为什么答对”也一起钉死了。工具调用、逐源提升、Lean 4 内核三件套一上，LLM 的经验性胡说就不再是“看起来像对”，而是必须拿出可回放的证明。

龙哥读论文 阅读 3 查看原文
#人工智能 #Agent #大语言模型 #模型架构
反事实压力下仍100%忠实，LLM事实核验新范式
🐉 龙哥读论文知识星球来了！
公众号每日8篇拆解不够看？星球无上限更AI领域论文、资讯、招聘、招博、开源代码，一站式干货，每日2分钟刷完即赚！
👇扫码加入「龙哥读论文」知识星球，前沿干货、实用资源一站式拿捏～ xingqiu_header

龙哥推荐理由：
这篇论文最狠的地方，不是“答对了”，而是把“为什么答对”也一起钉死了。工具调用、逐源提升、Lean 4 内核三件套一上，LLM 的经验性胡说就不再是“看起来像对”，而是必须拿出可回放的证明。


原论文信息如下：
论文标题:
Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs 发表日期:
2026年07月 发表单位:
没有 原文链接:
https://arxiv.org/pdf/2607.11884v1.pdf 开源代码链接:
https://github.com/7pocheR/eg-var 项目链接:
https://github.com/7pocheR/eg-var

当大模型信口开河时，我们如何让他闭嘴？

大模型最烦人的地方，不是偶尔答错，而是它经常答得特别像那么回事。尤其是在表格、统计、事实推断这类“看起来很简单，翻车却很快”的场景里，模型一旦把记忆里的旧知识和眼前证据搅在一起，输出就会从“回答问题”变成“编故事”。
这篇论文的思路很直接：既然模型嘴上不太老实，那就别只盯着答案对不对，而要让它拿出证据，还得拿出能被内核检查的证明。于是作者提出了 EG-VAR（Evidence-Grounded Verified Agentic Reasoning，基于证据的可验证智能体推理），用 Lean 4 证明内核做最后裁判：能证明的才叫 VERIFIED，证明不了的就老老实实 ABSTAIN（放弃回答）。
Figure 1. EG-VAR four-layer architecture. Solid arrows: control flow. Dashed arrow: Attested T payloads, the sole load-bearing hypothesis of mkVerified (Section 3.4).
图1：EG-VAR 的四层架构。控制流由上到下走，真正“扛事”的只有带有工具见证的 Attested T 证据。
先说人话版结论：这套方法不是让大模型“更会猜”，而是让它只能在证据链完整时说“对”。一旦证据链断了，模型就不能装懂，必须停下来。这种设计对高风险事实推断特别重要，比如金融报表、医疗统计、政策数据、审计材料，错一条都不是“模型小失误”，而是真会出事。

从“信”到“证”：EG-VAR的四层信任架构

EG-VAR 的关键不是单点技巧，而是一套分层信任账本。论文把整个流程拆成四层：工具层、逐源形式化层、Lean 4 内核层、以及最外面的 LLM 解决器层。前两层负责“给证据”，第三层负责“盖章”，第四层负责“提案”。
第一层是工具层（L1）。它是确定性的，干的活也很朴素：查表、筛选、聚合、取值。每次工具调用都会带回一个Attested T，可以理解为“这条结果是工具在运行时亲手盖过章的”。这里的 T 是 ToolId，表示工具类型；Attested T 就是“某工具的可验证见证”。
第二层是逐源形式化层（L2）。这层最容易被忽略，但其实最关键。因为工具拿到的是“表格里的值”，而用户问的是“世界里的事实”。比如表格里某行某列是 Alabama，用户问的却可能是“Alabama 的 HIV 发病率是否最高”。从“单元格值”到“世界事实”之间，必须有一个经过审计的映射，也就是论文说的 per-source lift（逐源提升）。
第三层是 Lean 4 内核。这里没有“差不多”“大概对”“模型觉得可以”这种词，只有类型检查通过或者不通过。Lean 内核只认形式证明，不认嘴硬。第四层才是 LLM 解决器，它负责提出工具调用、组织证据、生成证明草稿，但它本身并不可信，最多算个会干活的实习生。
Figure 2. Worked trace for one claim. Untrusted LLM output (white) commits to a goal type; trusted runtime (gray) produces the attested payload, composes it through the audited per-source lift, and the Lean kernel mints VERIFIED iff the derivation type-checks. The Sigma-witness of the accepted proof is the published answer.
图2：单条推理链路的工作流。LLM 先提出目标类型，运行时给出可审计证据，再通过逐源提升映射到世界事实，最后由 Lean 内核决定是否发放 VERIFIED。
这套分层设计的妙处在于，证据和推理被拆开管理。证据归证据，推理归推理，谁都别混。这样一来，系统既能保留大模型的灵活性，又不会让它把“看见了什么”和“因此能推出什么”胡乱糊成一锅粥。

内核是唯一的法官：mkVerified规则如何杜绝幻觉

论文里最硬核的一点，是一个叫 mkVerified 的规则。它的意思很简单：只有当运行时已经给出了带证据的工具输出，内核才允许生成 VERIFIED。没有工具见证，就没有 VERIFIED；没有 VERIFIED，就别想把答案包装成“已验证真理”。
这其实是在给大模型做“制度性闭嘴”。以前很多工具调用方案的问题是：模型虽然调用了工具，但最后输出的答案未必真从工具证据里长出来，可能只是顺手借了个壳。EG-VAR 不给这个机会。它要求每个 VERIFIED 结论都必须能追溯到一个工具调用叶子，再经过 Lean 内核逐步检查。链条断了，就只能 ABSTAIN。
更妙的是，论文还引入了证据等级：VERIFIED、SUPPORTED、PLAUSIBLE、SPECULATIVE。等级只能向下折损，不能向上硬抬。这看起来像是形式系统里的小规矩，实际很有治理味道：不确定就降级，别让一句“我觉得”偷偷变成“我已经证明”。
论文的证明对象也不是抽象概念，而是运行时真正吐出来的 proof object：Lean 文件、证据列表、步骤历史。换句话说，别人不需要重新跑一遍大模型，只要拿 Lean 文件重放审计，就能知道这条 VERIFIED 到底是不是“真有证据”。这对企业和监管场景非常友好，因为审计成本会比“重跑整个智能体流程”低得多。
这张演示图展示了重放审计的思路：只要证明文件符合白名单，且公理来源都在允许范围内，就能通过核验。说白了，模型可以犯错，但不能把错包装成“已证明”。

100%精准的代价：形式化提升与人工策展

先别急着鼓掌，100% 不是白来的。EG-VAR 的高准确率，背后有一个现实得不能再现实的代价：逐源形式化需要策展。也就是说，某个数据源怎么从表格语义映射到世界语义，不是模型自己“悟”出来的，而是需要人工或半自动地审定。
这也是论文很诚实的一点：它不是说“以后所有事实推断都能零成本自动化”，而是说把一次性的形式化成本前置，之后同一数据源上的很多问题都能复用。换句话说，贵的是第一下，后面就开始摊薄成本。这个逻辑和工程里做 schema、做 API 契约、做数据字典其实很像，前期磨人，后期省命。
图3：Tier 1 梯子结果。可以看到，单纯表格推理已经不差，但一旦把内核检查加进去，就能把最后那几个“差不多对”的洞补上。
论文在 TableBench 的 120 条无歧义声明上做了 Tier 1 测试。结果很漂亮：EG-VAR 做到 120/120，而同工具同模型基线是 114/120，纯表格单轮是 107/120。这个差距看着不算离谱，但别小看这几个点，在高风险场景里，95% 和 100% 不是同一张船票。
更重要的是，EG-VAR 的提升不是靠“模型更大”或者“提示词更长”，而是靠把证据、语义提升、证明检查这三件事拆开并锁死。这个方向的价值不在于炫技，而在于把可控性真正做出来。

反事实压力测试：当工具和数据都“说谎”，模型还能信谁？

真正能看出系统底色的，不是正常数据，而是反事实压力测试。论文专门构造了被篡改的表格：把真实值改成和模型先验冲突的值，再看模型到底听数据还是听脑子里的旧知识。这个测试非常狠，因为很多模型一遇到这种场景就开始“宁愿相信自己”。
图4：Tier 1.5 反事实压力测试。表格被故意翻转后，EG-VAR 仍然 100% 源忠实；同工具方案则开始出现不同程度的先验覆盖。
结果很有意思。无论是极端翻转还是细微翻转，EG-VAR 都保持 100% 的 source-faithful；而同工具基线会掉到 80% 到 90% 左右，纯无工具基线甚至更低。说明它不是“碰巧在干净数据上表现好”，而是在数据和先验打架时，仍然站在证据一边。
这点对现实系统非常关键。因为真实世界里，最常见的不是“表格里没答案”，而是“表格答案和模型记忆冲突”。如果系统没有强约束，就很容易把旧知识当真理，把新证据当噪声。EG-VAR 的价值就在于把这个倾向硬生生掰回来。
图5：Tier 2 误差分解。把“模型没答对”拆成不同类别之后，能看出真正的语义形式化错误并不高，更多问题来自歧义、基准瑕疵或系统主动放弃。
Tier 2 则更接近真实部署：不再把金标准目标类型提前喂给系统，而是让 LLM 自己去形式化。这里 Sonnet 的语义形式化错误率是 3.3%，Opus 是 1.7%。这个结果说明，形式化本身仍然是难点，但难点已经从“答案是否有证据”变成“自然语言能否准确翻译成形式目标”。后者是可以继续通过数据和训练改进的。
图6：Tier 2 在反事实压力下的表现。即便让 LLM 参与形式化，只要后端证据链和内核约束还在，系统仍能把输出拉回证据侧。

未来展望：形式化提升的“基础设施化”与AI治理

这篇论文最值得记住的，不只是一个方法，而是一种思路：把形式化从“论文里的一次性工作”变成“数据和系统里的基础设施”。如果数据源、API、报表、文档都能带上可复用的正式语义侧车，那么以后大模型做事实推断时，就不必每次都从零开始猜。
这对 AI 治理也很有启发。很多治理方案喜欢盯着“模型说了什么”，但 EG-VAR 更像是在回答“这句话能不能被审计地证明出来”。一旦证明链条可回放，责任边界、证据边界、歧义边界都会清楚很多，至少不会再出现那种“模型一本正经地胡说八道，系统还给它打高分”的尴尬场面。
当然，这条路也不是没有坑。它依赖高质量的逐源提升、依赖清晰的源语义、依赖可维护的形式化资产。换句话说，它更像治理基础设施，而不是一键起飞的魔法盒。但恰恰因为它不装，反而更像能落地的东西。

龙迷三问

下面是龙哥对于大家可能的一些问题的解答：

这篇论文到底解决了什么问题？它解决的不是“模型会不会算”，而是“模型算出来的经验性结论能不能被证据和证明链条一起托住”。EG-VAR 让 VERIFIED 输出必须来自工具见证和 Lean 内核检查，答不出来就 ABSTAIN。

Attested T 和 mkVerified 是什么意思？Attested T 可以理解为“工具运行时给出的带章证据”；mkVerified 是内核里的唯一发证规则，只有拿到这个证据，系统才允许把某条世界事实标成 VERIFIED。没有这两个东西，系统就只能沉默，不能乱编。

这套方法能直接产品化吗？能做，但不是“直接装上就跑”。它更适合高价值、强审计、数据源稳定的场景，比如报表核验、合规审查、知识库问答、事实型文档生成。前提是源语义和逐源提升先整理好，不然内核再严，也救不了脏数据。

如果你还有哪些想要了解的，欢迎在评论区留言或者讨论~

龙哥点评

论文创新性分数：★★★★☆

把工具调用、逐源提升和 Lean 内核绑成一条证据链，这个结构很硬，且不是常见的“工具增强版 LLM”换皮。

实验合理度：★★★★☆

Tier 1、Tier 1.5、Tier 2 分层清楚，既测基线也测反事实，还把形式化误差单独拆出来，逻辑比较完整。

学术研究价值：★★★★★

它不只是做一个更准的系统，而是提出了一种可审计的事实推断范式，对可信 AI、形式化验证和数据治理都有启发。

稳定性：★★★☆☆

证明链本身稳定，但强依赖源语义、逐源提升和高质量工具接口，换个脏数据源未必还能这么稳。

适应性以及泛化能力：★★★☆☆

框架思路可推广到 SQL、API、知识图谱等，但每个源都要做形式化提升，泛化是架构级的，不是开箱即用的。

硬件需求及成本：★★★☆☆

推理本身不一定重，但 Lean 检查、工具调用和形式化策展都要成本；真正贵的是前期工程化和数据治理。

复现难度：★★★☆☆

代码开源是加分项，但 Lean 4、Anthropic API 和数据策展门槛都不低，复现不是“点一下就完事”。

产品化成熟度：★★★☆☆

适合强审计场景试点，不适合直接铺到所有问答任务；先把高价值事实核验做稳，再谈大规模扩展。

可能的问题：最强的短板不是模型，而是逐源提升的人工成本和语义边界；一旦源语义不清，形式化再强也只能严谨地错。


主要参考文献

Junyu Ren. Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs. arXiv:2607.11884v1, 2026.
EG-VAR 开源代码：https://github.com/7pocheR/eg-var
原文链接：https://arxiv.org/pdf/2607.11884v1.pdf

*大模型会答题不稀奇，能把“正确”答案也做成可回放、可审计、可追责，才是真本事。欢迎来龙哥读论文群，一起围观这种“让AI闭嘴”的硬核架构～  

end
欢迎加入龙哥读论文粉丝群，扫描下方二维码或者添加龙哥助手微信号加群：kangjinlonghelper。一定要备注：研究方向+地点+学校/公司+昵称（如 图像处理+上海+清华+龙哥），根据格式备注，可更快被通过且邀请进群。想聊大模型、Agent、AI安全，群里都能找到同好。
wechat_helper dianzan
转发文章 微博 X LinkedIn Facebook
龙哥读论文 · PaperDaily

本文基于龙哥读论文 PaperDaily 数据库整理，结合论文原文与工程视角进行解读。