想象一下，你有一个超级聪明、爱聊天的机器人助手（一个大语言模型），它热爱讲述世界的故事。但问题在于？有时这个机器人会对自己的记忆过于自信，以至于编造事实，或者忽略眼前摆在面前的实际证据。这就像一个学生，当被要求对照教科书检查一道数学题时，他直接写下了自己“认为”正确的答案，因为那是他在梦里记得的，即便教科书上写的却是别的内容。
长期以来，人们一直试图通过给机器人一个“工具箱”（比如计算器或数据库）来修复这个问题。但本文认为，仅仅把工具箱交给机器人是不够的。机器人可能仍然会忽略工具箱，或者在使用工具箱中的数字时，扭曲逻辑以符合它自己的故事。这就像给一位厨师提供新鲜且经过验证的食材，却任由他随心所欲地烹饪；最终的成品可能依然是一场灾难。
核心理念：“经核实声明”工厂
作者们（由 Junyu Ren 领导）构建了一个名为 EG-VAR（证据驱动的经核实代理推理）的新系统。你可以把它想象的不只是一个回答问题的机器人，而是一个拥有严格、不眨眼的检查员的高安全性工厂。
这个工厂是如何运作的，请看以下步骤：
- 工具层（可靠的快递员）： 首先，一个可靠、枯燥、具有确定性的机器（而不是那个爱聊天的机器人）前往源头——比如电子表格或数据库——获取原始数字。它会在这些数字上盖上“已核实”的印章。这是将真实数据引入工厂的唯一途径。
- 形式化器（翻译官）： 随后，这个爱聊天的机器人（LLM）被要求将人类的问题转化为一种严格的数学语言，称为 Lean 4。这就像是要求机器人写一份法律合同或数学证明，而不是写一段文字。
- 内核（不眨眼的检查员）： 这是最关键的部分。一个微小、极其严格的计算机程序（Lean 内核）充当检查员。它会逐行检查机器人的“合同”。
- 黄金法则： 检查员有一条规则：“除非你能指向一个带有来自可靠快递员印章和封条的数字，否则你不能声称某个事实是**已核实（VERIFIED）**的。”
- 如果机器人试图捏造一个数字，或者试图使用一个数字但连接逻辑错误，检查员就会拒绝整个过程。
- 结果：
- 如果证明通过，工厂会打印出一个**已核实（VERIFIED）**的答案。这个答案附带一个“可重演的审计追踪”，这意味着任何人以后都可以重新运行数学运算，并看到答案是如何从原始数据构建而成的。
- 如果证明失败，工厂不会瞎猜。它会说 ABSTAIN（意思是“我不知道”或“我无法证明这一点”）。这是一个诚实的“我放弃”，而不是一个自信的谎言。
论文的实际发现
作者们在针对表格（电子表格）的 120 个特定问题集上测试了这个系统。
- “完美”得分： 当问题清晰且机器人获得了正确的工具时，EG-VAR 正确回答了 120 出 120 个问题。准确率达到了 100%。
- 竞争对手： 其他使用了相同工具但没有严格检查员的系统，仅答对了 114 出 120 个问题（95%）。它们仍然在犯错。
- “反事实”测试： 这是真正的压力测试。作者修改了表格中的数字，使其与机器人从其训练中“已知”的内容相矛盾（例如，将一个国家的人口改为一个极小的数字）。
- 在没有严格检查员的情况下，机器人有 80% 到 90% 的时间会忽略新数字而坚持其旧记忆。
- 有了 EG-VAR，系统对这些新改变的数字保持了 100% 的忠实度。无论机器人的旧记忆有多强大，检查员都强制它使用新数据。
论文明确排除的内容（“禁区”）
论文非常明确地说明了该系统不是什么以及它不能做什么：
- 它不是解决所有幻觉的万灵药。 论文明确指出，机器人在将人类问题翻译成数学语言时仍可能出错。如果机器人误解了问题并写错了数学题，检查员会完美地检查那个数学题，但对于原始问题来说，答案仍然是错误的。
- 在他们的测试中，这种“翻译错误”在一个模型中发生了约 3.3%，在更强的模型中发生了 1.7%。
- 它不能修复错误的数据。 如果原始电子表格中有谎言，该系统会忠实地核实那个谎言。该系统保证的是答案来自于源头，而不是源头本身是真实的。
- 它不是一个“也许”系统。 论文反对那些给出“置信度分数”（如“我有 80% 的把握”）的系统。相反，EG-VAR 使用严格的“是/否”闸门。你要么拥有一个经核实的证明，要么拥有一个诚实的“我弃权”。
他们有多确定？
作者对他们系统的结构安全性非常有信心。他们通过数学方法证明了（定理 3.1 和 3.2）：
- 没有任何**已核实（VERIFIED）**的答案可以在没有带有印章的工具调用支持的情况下出现。
- 每一个已核实答案中的逻辑步骤都经过了内核的检查，并且在数学上是有效的。
然而，关于机器人翻译人类语言的准确性，他们则更为谨慎。他们测量了特定测试中的错误率（3.3% 和 1.7%），并建议如果对机器人进行更多关于如何正确翻译问题的训练，这些数字可能会变得更好。但“安全底线”——即系统不会默默撒谎的保证——是构建在架构之中的，而不仅仅是靠机器人的大脑。
总结
EG-VAR 就像一个工厂，除非能为使用的每一个零件都出示收据，否则拒绝发货。如果机器人试图混入一个假零件，工厂就会停产并说：“不行，我们不能发货。”它将“撒谎的机器人”问题转化为了“缺失收据”的问题，而后者更容易被发现和修复。虽然它并没有解决所有问题（机器人仍然可能误解订单），但它确保了当工厂说“已核实”时，它指的就是“已核实”。
技术摘要：证据驱动的验证式智能体推理 (EG-VAR)
问题陈述
大型语言模型（LLM）在推理过程中经常会产生经验性事实的幻觉，要么是捏造数据，要么是依赖与检索到的证据相冲突的过时参数先验。虽然工具增强型推理（RAG）允许模型咨询外部来源，但它无法保证可验证的经验性主张。现有方法存在两个结构性失效：
- 未经证实的输出： 被接受的输出并不一定源自经过证实的证据；模型可能会忽略与自身内部先验相冲突的检索数据（确认偏差）。
- 未经验证的演绎： 被接受的演绎在形式化审查下并不一定成立；模型可能会进行无效的逻辑步骤或误解工具输出。
现有的解决方案（如符号事实验证器或 LLM 驱动的定理证明器）要么缺乏外部接地（仅限数学证明器），要么依赖于无法在结构上保证不存在未经支持的主张的学习组件。
方法论：EG-VAR 架构
本文提出了 EG-VAR（证据驱动的验证式智能体推理），这是一个通过集成证明助手（Lean 4）与工具证言（tool-attestation）来使经验推理可控的四层架构。该系统将 LLM 视为受严格定义的信任账本约束下的不可信组件。
四层堆栈
- L1：工具层（可信、确定性）： 一个确定性运行时执行针对外部来源（例如表格单元格查找、聚合查询）的查询。它生成一个
Attested T 有效负载——一个记录了查询、来源身份和结果的运行时见证（witness）。只有运行时能够生成这些见证。
- L2：逐源形式化（离线审计）： “策展人”（Curator）为每个数据源定义一个提升目录（lift catalog）。该目录将 L1 存储事实（例如“第 r 行第 c 列的单元格值为 v”）映射到 L2 世界本体事实（例如
HasProperty, ArgmaxWhere）。这些提升过程经过一次性审计并作为公理导入。
- L3：Lean 4 内核（可信、形式化）： 内核是铸造
Evidence Verified 主张的唯一权威。它强制执行单一的铸造规则 mkVerified，该规则要求必须具备来自运行时的 Attested T 假设。内核对每一个证明步骤进行类型检查；如果步骤失败，则该主张被拒绝。
- L4：求解器 LLM（不可信、随机性）： LLM 接收一个类型化的目标并提出证明策略（tactics）。它可以消费由运行时引入的
Attested T 项，但不能合成这些项。如果内核拒绝了该策略，系统将进行迭代或选择弃权（abstain）。
核心机制
mkVerified 规则： Evidence Verified 的唯一构造函数要求提供 Attested T 见证。这确保了任何验证输出的存在都必须对应一个工具调用（定理 3.1）。- 依赖和见证（Dependent Sum Witnesses）： 主张被构造成依赖和（Σ）。对于问题“哪个实体具有属性 P？”，目标是 Σ(e:String)(v:Value),Evidence Verified(…)。表面答案是从内核检查的证明中提取出的见证。
- 诚实弃权： 如果内核拒绝了证明（由于缺少提升、无效策略或缺乏证言），系统会输出 ABSTAIN 并附带可重放的审计追踪，而不是进行猜测。
- 等级规范（Grade Discipline）： 证据带有显式的等级（
VERIFIED, SUPPORTED, PLAUSIBLE, SPECULATIVE）。系统强制执行“禁止向上转型”规则：结论的等级不能高于其最弱的前提。
核心贡献
- 接地性的结构化保证： EG-VAR 是首个将证明助手内核与工具证言结合为类型化公理的架构。它提供了一个结构化保证（定理 3.1），即每一个
VERIFIED 输出都源自一个经证实的工具调用，从而消除了无论 LLM 能力如何强弱都会导致的未经支持的幻觉。
- 形式安全 vs. 语义忠实性： 本文区分了形式安全（证明被内核接受）与语义忠实性（形式化目标与自然语言主张匹配）。EG-VAR 在结构上保证了前者；后者被视为一个通过形式化微调来解决的准确性目标。
- 可重放的审计追踪： 每个验证的主张都附带一个自包含的 Lean 证明文件。第三方可以在不重新运行 LLM 的情况下，使用内核、逐源提升目录和工具适配器，在离线状态下重新进行类型检查。
- 逐源形式化协议： 本文引入了一种将数据源视为同等信任人工制品的方法，要求进行形式化处理（提升目录），从而将来源侧的策展与主张侧的推理分离。
实验结果
评估侧重于 TableBench（表格数值推理），涵盖三个层级：
第一层级（金标准目标基准，n=120）：
- EG-VAR 在无歧义主张上达到了 120/120 (100%)，其结果与金标准答案一致且拥有经内核检查的证明。
- 基线模型（使用相同工具但没有内核）停滞在 95.0% (114/120)。
- EG-VAR 消除了这一差距，证明了内核规范强制执行了工具输出的正确组合。
第一层级 1.5（反事实压力测试，5 个领域 × 2 个模型）：
- 创建了合成表格，其中单元格数值与模型的世界知识先验相矛盾（例如，将某个国家的总人口修改为极低值）。
- EG-VAR 在所有领域和翻转幅度下均保持 100% 的来源忠实度。
- 基线模型（同类工具）下降至 80–90% (Sonnet) 和 50–80% (无工具)，显示出 EG-VAR 在结构上防止了“先验覆盖”失效模式（即模型忽略检索到的证据）。
第二层级（端到端结合 LLM 形式化器，n=120）：
- 在 LLM 提出形式化目标（移除金标准固定绕过）的全自动化设置下，纯形式化器错误率分别为 3.3% (Sonnet) 和 1.7% (Opus)。
- 剩余的分歧被归类为已记录的歧义 (4.2%) 或显现出的基准测试伪迹问题 (1.7%)，所有这些都是显性的、可审计的，而非沉默的幻觉。
意义与主张
本文将 EG-VAR 定位为处理高风险经验性主张的技术治理接口。其意义在于将安全性负担从统计学习转向架构强制执行：
- 消除未经支持的输出： 结构化保证确保了在系统的威胁模型下，“验证式幻觉”（即标记为
VERIFIED 但没有证据的输出）是不可能存在的。
- 可衡量的确定性： 通过将弃权作为内核拒绝的结构化结果而非学习行为，系统提供了可衡量的“拒绝率”和类型化不确定性。
- 形式化飞轮： 作者认为，随着数据源向类型化接口（SQL、API、知识图谱）演进，形式化负担将转化为可重用的基础设施，从而降低单次查询的验证成本。
- 治理属性： 系统实现了三种可强制执行的属性：(i) 通过可重放证明对每个验证输出进行独立审计；(ii) 通过等级规范实现类型化不确定性；(iii) 将诚实弃权作为一种可衡量的系统属性。
文章总结道，尽管语义形式化错误仍然存在（可通过在发布的策展语料库上进行微调来解决），但 结构化安全底线 已经建立，为消除 LLM 在经验推理中的幻觉提供了一条路径。
每周获取最佳 machine learning 论文。
受到斯坦福、剑桥和法国科学院研究人员的信赖。
请查收邮箱确认订阅。
出了点问题，再试一次？
无垃圾邮件，随时退订。