← 返回 PaperDaily
大模型与智能体
反事实测试100%忠实：EG-VAR把幻觉拦在内核外
LLM会调用工具，不代表它就会老老实实认账。EG-VAR最狠的地方，不是“又接了个工具”，而是把证据、形式化、内核检查绑死，能证才给VERIFIED，证不出来就ABSTAIN。TableBench、反事实压力测试、端到端形式化误差，这套结果够硬。
龙哥读论文
阅读 4
查看原文
🐉 龙哥读论文知识星球来了！公众号每日8篇拆解不够看？星球无上限更AI领域论文、资讯、招聘、招博、开源代码，一站式干货，每日2分钟刷完即赚！👇扫码加入「龙哥读论文」知识星球，前沿干货、实用资源一站式拿捏～
龙哥推荐理由：
LLM会调用工具，不代表它就会老老实实认账。EG-VAR最狠的地方，不是“又接了个工具”，而是把证据、形式化、内核检查绑死，能证才给VERIFIED，证不出来就ABSTAIN。TableBench、反事实压力测试、端到端形式化误差，这套结果够硬。
原论文信息如下：
LLM调用工具就不幻觉了吗？不，99%都不行！
现在很多系统都爱说一句话：“给大模型接上工具，幻觉就少了。”听起来很美，现实却很骨感。工具只能说明模型“查过资料”，不能说明它“查对了、理解对了、推理也对了”。更扎心的是，模型还可能一边查表，一边把自己的旧记忆当真理，最后给出一个看起来很像回事、其实经不起审计的答案。
这篇论文最狠的地方就在这里：它没有继续和大模型“讲道理”，而是直接上了Lean 4 定理证明器，把“正确答案”变成一个必须被内核亲自签字的东西。能证明，才给 VERIFIED；证不出来，就老老实实 ABSTAIN。这不是“更会猜”，而是“不会乱装懂”。
用定理证明器给LLM的推理上“安全锁”
先把背景说人话：表格问答、数值推理、事实核查这类任务，难点不是“模型会不会说话”，而是“模型说出来的话能不能被追溯到证据”。传统做法通常是检索、工具调用、再让模型总结。问题在于，检索到证据并不等于证据被正确使用，更不等于推理链条在形式上无懈可击。
EG-VAR 的思路很直接：把整个系统拆成四层，谁负责什么、谁可信、谁不可信，全部写清楚。最底层是工具层，负责从表格里查数；第二层是“源到世界”的形式化映射，把表格里的存储事实翻译成世界事实；第三层是 Lean 4 内核，负责最终验签；第四层才是大模型，负责提议、猜测、写 tactic，但它自己没有“盖章权”。
这套结构的核心约束只有一句话：VERIFIED 只能从“已被工具证实的证据”出发，再经过内核检查的推导产生。也就是说，大模型可以参与，但它不能凭空创造证据；它可以组织推理，但最后必须让 Lean 4 点头。
这里有个很关键的术语要解释清楚。论文里说的 Attested T，意思是“被工具运行时证明过的证据载体”，可以理解成工具返回结果时顺手附上的一张可核验小票。mkVerified 则是唯一的“发证入口”，只有拿着这张小票，Lean 才允许生成 VERIFIED。没有小票，门都没有。
论文还引入了一个很实用的概念：证据等级。它把结果分成 VERIFIED、SUPPORTED、PLAUSIBLE、SPECULATIVE 四档，只能从高等级往低等级降，不能反向“升级”。这个设计很像现实世界的审稿流程：证据不够，就别硬把猜测包装成定论。模型最怕的不是不会，而是把“也许”说成“肯定”。
拆解EG-VAR：四层结构如何杜绝胡说八道，100%零幻觉！
如果把它当成一条流水线看，流程其实很清楚。第一步，大模型先读问题，猜一个结构化目标；第二步，工具从表格或数据源里拿到原始值；第三步，源侧的形式化映射把这些值翻译成 Lean 能理解的世界事实；第四步，Lean 内核检查这条推理链是否成立。只要其中任何一环出问题，系统就不装懂，直接弃权。
这套设计的妙处在于，它不是把“正确性”押在模型嘴上，而是押在可回放、可重检、可审计的证明对象上。换句话说，答案不是“模型觉得对”，而是“内核证明它对”。在高风险事实推理里，这种态度比“自信满满地胡说”靠谱得多。
论文还专门强调了一个容易被忽略的问题：表格不是“数据摆在那里就完了”，表格本身也要形式化。因为同一张表可以有不同语义解释，比如“哪一列代表国家”“哪一行代表球队”“哪个字段是数值”。EG-VAR 把这部分做成了“源侧 lift”，也就是每个数据源都先定义好一套从存储事实到世界事实的映射，后续所有问题都复用这套映射。这样做的代价是前期要做一次审计，但好处是后面每次查询都不用重复猜语义。
从工程角度看，这个系统最像一个“带安全壳的智能代理”。大模型还是那个大模型，还是会犯错，还是会偏见上头；但它的输出必须穿过工具、形式化和内核三道门。门槛越多，越不容易出“看着像真的，实际上是编的”这种经典事故。说白了，这不是让模型更像神，而是让它更像一个会认账的工程系统。
反事实测试大展身手，当AI学会“认怂”：诚实弃权比瞎猜更高级
这篇论文最值得看的，不只是“答对了多少”，而是它怎么在反事实压力测试里保持忠实。所谓反事实，就是故意把表格中的某些值改掉，让它和模型“脑子里的常识”打架。很多模型一遇到这种情况就开始倔：明明表里写的是 A，它偏要说 B，因为 B 更符合它的参数记忆。
结果很有意思。EG-VAR 在反事实场景下保持了 100% source-faithful，也就是始终忠于来源数据；而同工具基线会掉到 80% 到 90%，不用工具的基线甚至低到 50% 到 80%。这说明工具调用本身并不是保险箱，真正把系统“拴住”的，是工具证据必须进入形式化证明，再由内核决定生死。
更值得注意的是，论文没有把“弃权”当失败，而是把它当成一种诚实输出。当形式化不通过、语义不清楚、证据不完整时，系统宁可 ABSTAIN，也不硬编一个 VERIFIED。这个态度很对。现实业务里，最怕的从来不是系统说“我不知道”，而是系统一本正经地说“我知道”，然后把人带沟里。
论文还做了一个很实在的端到端实验：让 LLM 自己来做形式化器。这个环节的语义形式化错误率，Sonnet 大约 3.3%，Opus 大约 1.7%。这组数字很说明问题：即便最强模型也不是“天然会把自然语言精确翻成可证明逻辑”的。模型会把大意翻对，但在边界条件、歧义、量词范围上翻车，这些地方恰恰是事实核查最容易出事故的地方。
再往下看，论文给出的结论其实很朴素：工具调用能降低幻觉，但不能自动消灭幻觉；把工具证据纳入定理证明，才真正把“正确”变成可审计的结构。这句话听着不花哨，但很硬。因为它指出了当前大模型系统里最容易被忽略的事实：真正难的不是“拿到信息”，而是“让信息进入可证明的推理链”。
龙迷三问
这篇论文到底解决了什么问题？它解决的不是“模型会不会查资料”，而是“模型查到资料后，能不能把答案变成可证明、可回放、可审计的结论”。EG-VAR 用工具证据 + Lean 4 内核，把 VERIFIED 和 ABSTAIN 分开，避免把猜测包装成事实。
文中的 Attested T、mkVerified、ABSTAIN 分别是什么意思？Attested T 是工具运行时生成的“证据小票”；mkVerified 是 Lean 内核唯一允许发出 VERIFIED 的入口；ABSTAIN 则表示证据不足或证明失败时的诚实弃权，不再硬猜。
为什么还要做反事实测试？因为很多模型在“常识”和“表格”冲突时会偷偷站队常识。反事实测试就是故意把表格改成和常识冲突，看系统到底信谁。EG-VAR 在这类测试里保持了 100% source-faithful，说明它确实把来源证据放在了第一位。
如果你还有哪些想要了解的，欢迎在评论区留言或者讨论~
龙哥点评
论文创新性分数：★★★★☆
把“工具调用”和“形式化证明”绑在一起不算空前，但把工具证据、源侧 lift、Lean 内核验签、诚实弃权做成一条完整管道，思路很完整，且有明显治理味道。
实验合理度：★★★★☆
有基线、有反事实、有端到端形式化误差分解，实验设计挺像样。唯一要留意的是，当前主要还是表格任务，跨源泛化还没真正展开。
学术研究价值：★★★★★
这篇工作真正有价值的地方，不只是提升准确率，而是给“可验证的经验推理”搭了一个技术治理框架。对事实核查、报表分析、审计辅助都很有启发。
稳定性：★★★★☆
只要工具、lift 和内核都稳定，系统就很稳；但一旦源侧语义定义错了，错误会被“形式化地正确”地放大，所以前置审计很关键。
适应性以及泛化能力：★★★☆☆
框架思想很强，但论文当前主要落在表格场景。迁移到 SQL、知识图谱、API 还需要更多源侧形式化工作。
硬件需求及成本：★★★☆☆
推理时不一定特别吃硬件，但 Lean 检查、工具调用、形式化器协作会增加系统复杂度。算力不是最大成本，工程编排和源侧审计才是。
复现难度：★★★☆☆
代码开源是加分项，但 Lean 4、Python、API、数据和 lift 都要配齐，环境门槛不低。不是不能复现，是“认真复现”得花点时间。
产品化成熟度：★★★☆☆
在高风险事实核查、审计、报表解释场景里有潜力，但离通用产品还差一层“源侧标准化”和“语义 lift 维护体系”。
可能的问题：框架很硬，但前提也很硬：源侧语义必须被认真定义，lift 必须足够可信，否则形式化只能保证“证明了某个解释”，不保证解释本身永远正确。
主要参考文献
Junyu Ren. Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs. arXiv:2607.12763v1, 2026.
项目开源代码：https://github.com/7pocheR/eg-var
项目说明：https://github.com/7pocheR/eg-var/blob/main/README.md
*本文仅代表个人理解及观点，不构成任何论文审核或者项目落地推荐意见，具体以相关组织评审结果为准。欢迎就论文内容交流探讨，理性发言哦～ 想了解更多原文细节的小伙伴，可以点击"阅读原文"，查看更多原论文细节哦！
欢迎加入龙哥读论文粉丝群，
扫描下方二维码或者添加龙哥助手微信号加群：kangjinlonghelper。
一定要备注：研究方向+地点+学校/公司+昵称。想看更多“让AI不敢胡说”的硬核拆解，进群继续聊🤘
