给评分者打分：LLM 推理验证的自治等级 L0–L5

这篇论文直指一个被长期忽视的问题：大语言模型如今被大量搭配验证器使用，步骤检查器逐步核对、自一致性过滤靠多数投票、工具事实核查调用外部知识、形式化证明助手则追求严格推导，它们都声称能发现模型的错误。然而作者发现，验证文献对"等级"一词的使用高度混乱，至少同时承载了五种不同含义。论文的核心贡献正是提出验证自治等级（VAL），用一个统一的轴来厘清这些概念，其分类依据是验证规范究竟从何而来，以及验证结论能够保证什么。作者由此构建了一个从 L0 到 L5 的连续谱：L0 是 LLM 的自我声明，缺乏确定性锚点；L2 建立在客观真值之上，只能保证正确性；L3 与 L4 进入可判定系统，分别具备单属性或领域级完备性；而 L5 在不受限制的情形下被证明不可达。这一框架的意义在于，它为纷繁复杂的验证方案提供了一个可对话、可比较的元标准，使得不同工作之间的差异得以被精确描述，而非被笼统地混为一谈。VAL 最核心的洞察是完备性盲区：基于替换与采样的验证器只能确认所提出的候选确实成立，却无法证明没有遗漏任何候选。这一区分贯穿全文，成为理解各类验证器能力边界的关键钥匙。 在技术方法上，VAL 并非又提出一种新的验证器，而是提出一套分类法与认识论框架。作者将验证方案沿单一主轴排列，主轴的两个端点分别是"验证规范的来源"与"结论的保证强度"。规范来源决定了验证的自治程度：若规范来自模型自身的声明，则停留在 L0；若来自客观真值，则达到 L2；若来自可判定系统的形式化规约，则进入 L3 与 L4。保证强度则刻画了结论的强弱：正确性只是最弱的保证，完备性才是更强的承诺。作者进一步指出文献中长期未被明确表述的一种二分：完备性只能针对可被形式化规约的性质才可达，而经验性的开放世界验证——例如事实核查与医疗诊断——其上限被锚定在 L2 的锚定正确性上。这一二分解释了为什么许多声称"全面验证"的系统实际上只能做到局部正确。VAL 还明确将粒度、概念层次、风险等级与系统栈层级判定为与 VAL 相互正交的维度，从而把长期纠缠在一起的概念拆解开来。在训练与评估层面，作者并未引入新的训练目标，而是构建了一套评估体系，对四类领域与一个形式化验证基线进行系统检验，并由此揭示出 17 篇 surveyed 论文中普遍存在的系统性概念混淆。 在实验设置与关键结果方面，论文选取了四个差异显著的领域作为验证场景：符号数学、行为监控、医疗诊断与代码生成。选择这些领域并非随意，它们恰好覆盖了从强形式化到强经验性的光谱两端：符号数学与代码生成更接近可判定与可规约，而医疗诊断与行为监控则属于开放世界的经验验证。作者在这四个领域中对各类验证方案进行了评估，并特别在一个当前最强的形式化验证基线上检验了 VAL 的解释力。耐人寻味的是，该基线作者本人承认其验证器"只关注每一步的正确性"，这恰好印证了 VAL 的判断：即便在最强的形式化系统里，实际达到的也只是正确性保证，而非完备性。这一观察成为 VAL 理论的一个有力旁证。消融与对比层面的发现同样关键：作者证明粒度、概念层次、风险与系统栈这四个常被误当作"等级"的维度，实际上与 VAL 正交，彼此之间不构成包含或推导关系。由此，VAL 化解了 17 篇 surveyed 论文中普遍存在的系统性概念混淆，把原本混为一谈的五种"等级"含义重新区分开来。这些结果共同支持了一个核心结论：验证能力的真实边界由规范来源与保证强度决定，而非由人们习惯称呼的那些"等级"标签决定。 在行业意义与潜在影响方面，这篇论文的价值在于为整个社区提供了一套可共享的概念语言。对开源社区而言，作者将代码与完整评估作为补充材料开放，使得研究者可以用 VAL 重新审视各自提出的验证器，判断其真实能力边界，而非停留在模糊的"更可靠"这类表述上。对工业落地而言，这一框架帮助工程团队在部署验证器时做出更清醒的决策：一个只能保证正确性的验证器无法告诉你是否遗漏了错误，而完备性只在可形式化的范围内才成立，盲目信任其"全面"会带来风险。对后续研究而言，VAL 把"验证能做到什么"这一长期被模糊处理的问题，转化为一个可分析、可测量、可比较的问题，从而引导研究者把精力投入到真正可达的目标上，例如在可规约性质上追求完备性，或在开放世界场景中诚实标注其 L2 上限。更重要的是，它提醒人们警惕那些声称"完全验证"的系统，因为完备性盲区意味着：确认了已有候选成立，绝不等于确认没有遗漏任何候选。这一洞见对安全关键的场景——如医疗诊断与代码生成——具有直接的警示意义。综合来看，这篇论文以清晰的分类与扎实的跨领域证据，为 LLM 推理验证这一快速膨胀的领域奠定了概念基础，其影响很可能延续到验证器设计、评估与部署的各个环节。