超越求解器判定：用于自动形式化的生成式奖励模型

# 超越求解器判定：自动形式化的生成式奖励模型
来源：https://arxiv.org/html/2609.11085
Vikash Singh††thanks:本文工作在亚马逊云科技实习期间完成
Debargha Ganguly†
单位：凯斯西储大学
邮箱：[[email protected]](mailto:)
Aman Goel
单位：亚马逊云科技
邮箱：[[email protected]](mailto:)
Ali Torkamani
单位：亚马逊云科技
邮箱：[[email protected]](mailto:)
Xiaoxue Han
单位：亚马逊云科技
邮箱：[[email protected]](mailto:)
Joseph Lilien
单位：亚马逊云科技
邮箱：[[email protected]](mailto:)
Ferhat Erata
单位：亚马逊云科技
邮箱：[[email protected]](mailto:)
Vipin Chaudhary
单位：凯斯西储大学
邮箱：[[email protected]](mailto:)

###### 摘要
神经符号系统依赖于数学求解器来保证推理的正确性，然而求解器根本无法判断形式化翻译是否与指定形式化目标保持严格的参考等价性。我们将这一漏洞形式化为“判定保持不忠实性”：即一种错误编码成功执行且匹配预期判定的失效模式。我们从理论上证明，仅基于结构的判定验证启发式方法在数学上受限于对这类欺骗性有效跟踪只能达到随机检测水平。为了解决这一问题，我们引入了生成式验证方法，该方法通过重新利用语言模型的原生词汇空间，将离线的Z3等价性预言机蒸馏为一个无需参考的、连续的参考等价性评分。通过决策投影对数几率透镜和稀疏自编码器进行的机制分析表明，这种生成式读出无需显式定位训练即可原生提取精确的空间错误坐标。实证表明，我们的预言机挖掘验证器在参考等价性验证中实现了0.961的AUROC，可零样本泛化至未见过的翻译器和不同的形式化风格，并在智能体测试时计算分配中带来11.3个百分点的下游准确率提升。

## 1 引言
参见图注图1：相同的求解器判定并不意味着等价的形式化。将\(>>\)反转为\(<<\)会产生一个有效、可满足的候选方案，但与参考形式化在逻辑上不等价。虽然共享的sat判定无法区分这对编码，但GenV+HN仅使用源问题和候选编码就成功分离了它们。
神经符号系统承诺了一种清晰的分工：语言模型将自然语言问题翻译成形式逻辑，而可靠的求解器（如Z3）执行推导。这种架构支撑了可满足性辅助的语言模型、逻辑问答、自动形式化和部署策略检查。由此产生的保证强大但有条件。可靠的求解器证明了所提供的编码能推出什么，但并未证明该编码是否准确地表示了源问题。因此，翻译步骤是一个独立的失效点。一个编码可能在语法解析、执行并获得有效的求解器证明的同时，改变了比较运算符、遗漏了需求、颠倒了蕴含关系或绑定了错误的变量。图1展示了一个最小示例：两个编码返回相同的可满足性判定，但它们在逻辑上并不等价。求解器在这两种情况下都是正确的。失败之处在于源问题与形式化程序之间的对应关系。
我们研究这种失效是相对于指定的参考形式化\(s^{\star}\)而言的。当一个候选方案在语法上有效、返回与\(s^{\star}\)相同的求解器判定，并且与\(s^{\star}\)在逻辑上不等价时，我们称之为判定保持不忠实性。这是一个操作性的、相对于参考的定义。它为训练和评估提供了一个确定性的目标，但并未假设每个自然语言问题都有唯一的形式化表达，或者参考形式化完全捕获了主观的源意图。
标准的保障措施处理的是相关但不同的故障。解析和类型检查拒绝格式错误的程序，求解器执行拒绝不一致或不支持的结果，自我一致性奖励重复的答案。这些信号仍然有价值，但二元判定本身无法区分两个旨在共享该判定的候选方案。学习型的奖励模型可能检查更丰富的表示，因此它们检测VPU的能力是一个经验性问题，而非我们定理的直接推论。
第3节形式化了仅基于二元判定的评分信息限制：对于具有相同求解器判定的匹配对，任何仅依赖该判定的函数都会给成对方案分配相同分数，且AUROC为0.5。此结果不适用于检查源问题、候选程序、执行跟踪或内部模型状态的系统。
我们的核心设计选择将严格的离线预言机监督与测试时部署分离开来。双向Z3检查生成决定性的参考等价性标签。在部署阶段，指定的参考不存在，GenV将这种离线信号蒸馏为一个功能性的、无需参考的评分。GenV利用模型标准的标记预测能力来产生整体的是/否判断，使用归一化的标记概率作为连续等价性评分，而不是附加专门的分类层或聚合局部步骤评分。通过针对预言机认证的VPU进行定向挖掘，将这种监督集中在硬负例上，从而产生了部署版的GenV+HN验证器。
我们的贡献包括：
- •参考相对的故障形式化：我们将VPU形式化为相对于指定参考的判定保持不等价性，并描述了仅二元判定评分在匹配对上的信息限制。
- •无需参考的生成式验证：我们将离线双向等价性标签蒸馏为一个连续的下一标记评分，推理时仅需源问题和候选编码。
- •受控的实证评估：我们评估了真实的翻译器错误、留出的翻译器架构、偏移的形式化风格、匹配的奖励模型基线、输入依赖性控制、校准，以及静态和自适应部署设置。
- •诊断性表示分析：我们表明，可以通过前缀分数、基于梯度的归因和稀疏特征探针，从验证器的隐藏状态中恢复错误位置和VPU信息，同时将这些分析视为诊断性而非因果性的。

## 2 相关工作
自动形式化中的条件保证。自动形式化使得辅助求解器推理成为可能，但形式推导假设初始翻译是精确的。判定保持不忠实性通过评估严格的参考等价性，而非仅仅是结构执行，来解决这个上游瓶颈。
结构性检查无法弥合等价性差距。标准检查如类型检查、自我一致性和回译能够可靠地拒绝无效编码。然而，如果两者产生相同的求解器判定，它们无法将参考等价的编码与VPU变体区分开来。通过结构检查并不保证参考等价性。
学习型验证与测试时计算。虽然生成式验证器和奖励模型改善了测试时计算分配，但GenV+HN独特地蒸馏了一个精确的离线SMT等价性预言机。与标准验证器不同，GenV直接从预言机标签学习一个诊断性的、无需参考的生成式读出，通过程序化的硬负例进行优化，以指导选择性分配。

## 3 问题表述
参考忠实性。令\(x\)为自然语言问题，\(s\)为候选的SMT-LIBv2编码，\(s^{\star}\)是\(x\)的指定参考编码。令\(A(s)\)表示\(s\)中断言的逻辑合取，令\(v(s) \in \{\texttt{sat}, \texttt{unsat}\}\)表示其求解器执行结果。对于与参考具有兼容逻辑签名的候选方案，我们通过相互蕴含来定义参考等价性：
\(\operatorname{Eq}(s,s^{\star})=\mathbf{I}\!\left[\begin{array}{l}A(s)\wedge\neg A(s^{\star})\ \text{is \{unsat\}},\\ A(s^{\star})\wedge\neg A(s)\ \text{is \{unsat\}}\end{array}\right]\) (1)
此测试在选定签名下确定模型论等价性。对于我们操作性目标而言，它是精确的，尽管这仍然相对于\(s^{\star}\)：具有不兼容签名的、保持含义的重构，或对欠规范的\(s^{\star}\)的有效补充，可能需要进一步的规范化才能获得预期标签。我们排除解析失败、超出求解器限制或返回unknown的候选方案。因此，我们的评估仅涉及求解器可判定的、语法有效的候选方案，其中操作训练标签为\(y_{\mathrm{ref}}=\operatorname{Eq}(s,s^{\star})\)。

###### 定义 1（参考相对的判定保持不忠实性）。
相对于指定的参考\(s^{\star}\)，候选方案\(s\)是判定保持不忠实的，当它语法有效、具有与参考相同的求解器判定，并且与参考不等价时：
\(\operatorname{VPU}(s;s^{\star})=\mathbf{I}[v(s)=v(s^{\star})]\,[1-\operatorname{Eq}(s,s^{\star})]\) (2)
第一个条件隔离了那些仅通过单个求解器判定检查无法提供警告的候选方案。第二个条件识别了与指定参考的逻辑不匹配。因此，VPU是参考不匹配的一个操作类别。

###### 命题 1（仅二元判定不可区分性）。
考虑一个配对评估集\(\{(s_i^+,s_i^-)\}_{i=1}^{n}\)，其中\(s_i^+\)是参考等价的，\(s_i^-\)是VPU，并且对于每一对都有\(v(s_i^+)=v(s_i^-)\)。对于任何仅依赖于二元求解器判定的评分函数\(g(s)=h(v(s))\)，对于每个\(i\)都有\(g(s_i^+)=g(s_i^-)\)。因此，当平局获得一半分数时，函数\(g\)在配对集上的经验AUROC为0.5。

###### 证明。
因为每一对的两个成员具有相同的判定，所以\(g(s_i^+)=h(v(s_i^+))=h(v(s_i^-))=g(s_i^-)\)。因此，正例和负例的分数多重集是相同的。没有任何正例获得严格高于其配对负例的分数，每次比较都是平局。根据平局获得一半分数的标准惯例，AUROC为0.5。∎

命题1隔离了一个狭窄的信息限制：仅二元求解器判定在判定匹配对上是不充分的。它并没有为检查\(x\)、\(s\)、求解器模型、证明跟踪或学习的隐藏表示的验证器建立不可能性结果。
在部署时，指定的参考\(s^{\star}\)不可用。因此，系统必须学习一个连续的、无需参考的评分函数：
\(f_{\theta}(x,s)\approx\Pr_{\theta}(y_{\mathrm{ref}}=1\mid x,s),\quad f_{\theta}(x,s)\in[0,1]\) (3)
我们仅在训练期间使用\(s^{\star}\)来构建精确的Z3预言机标签。这强制在监督所需的特权信息与推理时可用的无需参考的输入之间实现严格分离。

## 4 生成式验证
图2：我们的流程概述。(1)*标签。*对于每个问题，我们持有一个指定的参考\(s^{\star}\)。候选方案\(s\)来自真实的翻译器输出和经过小范围故意编辑的\(\mu(s^{\star})\)，例如翻转一个比较运算符。Z3在两个方向上检查等价性，因此单向一致是不够的。通过的候选方案是参考等价的；一个仍然能运行并返回相同判定但不再意味着相同含义的编辑就是VPU。Z3在指定的签名和资源限制下，为操作性的参考等价性目标生成确定性标签。这些标签无需逐项人工标注。(2)*训练。*一个简短的提示\(c(x,s)\)询问\(s\)是否正确形式化了\(x\)，并期望一个单词的回复。一个27B模型使用冻结的基础模型和仅训练的LoRA适配器来读取它；损失仅覆盖答案标记，因此我们不添加随机初始化的分类器。Z3标签监督该答案。(3)*部署。*过了虚线之后，指定的参考消失了，这才是重要的情况。仅给定\((x, s)\)，一次前向传播比较"Yes"与"No"的概率，得到一个分数\(f_{\theta}(x,s)\in[0,1]\)：接近1表示等价，接近0表示VPU。该数字用于VPU标记、Best-of-N选择和智能体门控。

为了解决公式3中定义的部署挑战，我们将离线的Z3预言机蒸馏为一个可部署的、无需参考的生成式验证器。我们的框架不是改变底层模型架构，而是完全在语言模型的原生词汇空间内操作。我们的方法包括三个步骤：通过下一标记预测来形式化连续验证评分，执行定向监督微调，以及通过预言机引导的硬负例挖掘来隔离逻辑边界。

通过下一标记预测进行验证。标准奖励建模通常受...