让模型调用数据库或计算器，只能证明它“接触过工具”，不能保证最终结论确实来自该证据，也不能保证中间推导有效。EG-VAR 把 Lean 4 内核放在结论出口：只有通过工具认证和内核检查的命题才能标记为 Verified，其余输出必须弃答并留下可重放轨迹。
证据来源与推理有效性同时检查
系统用工具认证公理记录数据如何进入证明，再通过显式的 source lift 声明来源能支持什么命题。最终证明必须结构化地追溯到工具调用和合法推理链。形式化侧车同时暴露目标命题、来源范围、证据边界、证明义务与弃答条件。
论文在 TableBench 的 120 个数值推理子集上报告 120/120，而使用相同工具但没有形式核验的基线为 95%。在五个领域、两个模型的反事实压力测试中，EG-VAR 保持 100% 来源忠实；不过部署时由 LLM 负责形式化，仍有 1.7% 到 3.3% 的语义形式化错误。
对高风险应用的影响
金融报表、实验数据和公共记录问答可以把“可验证结论”作为一种单独输出类型，而不是把所有自然语言答案都包装成同等可信。无法证明时返回 Abstain，也比带着流畅解释猜测更容易治理。
但内核只能验证已经形式化的命题；来源是否权威、自然语言是否被准确翻译、认证工具是否可信，仍在证明边界之外。团队需要审计这些 lift 和适配器，避免把错误前提形式化得无懈可击。
我的判断
EG-VAR 的亮点是把“引用证据”和“结论受证据约束”区分开。短期最现实的用法不是验证所有开放问答，而是选择数值、规则和表格推理等边界清晰的任务，为少量高风险结论提供可审计等级。