循证验证代理推理：通过工具证明的内核证明消除经验推理中 LLM 幻觉的途径

单独使用工具并不能使 LLM 经验推理变得可管理：接受的输出不需要来自经过证实的证据，并且接受的推论不需要经过正式的审查。我们提出了 EG-VAR（基于证据的验证代理推理），这是一种基于 Lean 4 的工具调用架构，其中 Lean 内核是通过工具证明公理和声明的源提升进行验证的声明的唯一铸造者。每个经过验证的输出在结构上都源自经过验证的工具调用（Thm.3.1）和经过内核检查的有效推理链（Thm.3.2）；剩余输出是诚实的 弃权并具有可重播的审计跟踪。在 TableBench 数值推理的子集合 (n=120) 上，EG-VAR 达到 120/120，而相同工具基线为 95%；在反事实压力测试（5 个域 x 2 个模型）中，EG-VAR 保持 100% 的源忠实度，而同一工具则下降至 80-90%（无工具 50-80%）。使用 LLM 作为部署时形式化器，残余语义形式化错误在 Sonnet 上为 3.3%，在 Opus 上为 1.7%。我们将 EG-VAR 定位为高风险经验主张的技术治理接口：正式的 sidecar 使目标命题、来源范围、证据边界、证明义务和弃权条件可审计，消除当今不受支持的已验证输出，同时将形式化错误、提升和来源权威争议、模糊性和弃权变成明确的审计目标。随着时间的推移，数据集、API、公共记录和人工智能生成的文档中的类型化 sidecar 可以将这种形式化负担分摊到可重用的基础设施中。