摘要
单靠工具访问并不能使大语言模型的经验推理可控：接受的输出未必源于经过验证的证据，接受的推导也未必经得起正式审查。我们提出了EG-VAR（证据基础的验证代理推理），这是一种基于Lean 4的工具调用架构，其中Lean内核是通过工具验证公理和声明的源提升唯一的验证声明生成者。每个经过验证的输出结构上源于经过验证的工具调用（定理3.1）和内核检查的有效推理链（定理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定位为高风险经验声明的技术治理接口：一个正式的副车使得目标命题、来源范围、证据边界、证明义务和放弃条件可审计，从而消除今天不支持的验证输出，同时将形式化错误、提升和源权威争议、模糊性以及放弃转化为明确的审计目标。随着时间的推移，数据集、API、公共记录和AI生成文档中的类型副车可以将这种形式化负担转化为可重用的基础设施。
博主点评： EG-VAR的提出标志着LLM推理领域的重要进展，通过引入形式化的验证机制，显著提升了经验推理的可信度和透明度。这一方法的核心在于将工具调用与验证过程紧密结合，为高风险决策提供了强有力的支持，未来有望推动更广泛的应用场景。