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

求解器能证明“给定编码推出什么”，却不能证明编码与指定参考形式化严格等价；判定保持的不忠实编码（VPU）因此会通过现有检查。

• 场景与重要性：神经符号系统让语言模型把自然语言译成形式逻辑，再由 Z3 等可靠求解器做演绎。作者认为该保证是有条件的：翻译是独立失效点，编码可以解析、执行并拿到有效证书，同时改掉比较算子、漏掉约束、反转蕴含或绑错变量。
• 现有方法的不足：解析与类型检查拒绝畸形程序，求解器拒绝不一致或不受支持的结果，自一致性奖励重复答案。作者认为这些信号仍有用，但二元求解器判定无法区分被构造成共享该判定的两个候选。第 3 节称：在判定匹配的配对上，任何只依赖该判定的分数都会打成平局，AUROC 为 0.5。
• 核心观察：相对指定参考 s⋆，忠实性是模型论双向蕴含，而不是“能跑且判定相同”。作者把监督与部署分开：双向 Z3 检查只在离线生成标签；部署时指定参考不存在。
• 威胁模型：
  • 受害系统：把自然语言问题译成 SMT-LIBv2，再交给求解器的神经符号流水线；评价只覆盖可判定、语法合法、不返回 unknown 的候选。
  • 失效定义：相对指定参考 s⋆，候选语法合法、求解器判定与 s⋆ 相同、且不满足 Eq(s, s⋆) 时为 VPU（Definition 1）。这是操作上的、相对参考的定义，不假设每个自然语言问题只有唯一形式化。
  • 攻击者知识与能力：论文未使用 white-box / black-box 等说法。训练时可用 s⋆ 与 Z3；部署时验证器只接收源问题 x 与候选 s。硬负例来自对金参考的程序化变异 μ，且仅保留满足 VPU 条件者。
  • 成功判定：检测按参考等价的 AUROC；下游按 Proof of Thought 自适应分配与静态 Best-of-N 的答案准确率。
• 论文提出什么：作者提出 Generative Verification（GenV），把离线 Z3 等价预言机蒸馏成无参考、连续的下一 token 等价分数；部署模型为再经硬负例挖掘的 GenV+HN。贡献还包括 VPU 形式化、跨翻译器与形式风格的评测，以及用 decision-projected logit lens 与稀疏自编码器做的诊断分析。

• 条件保证与自动形式化：Wu et al. (2022)、Ye et al. (2023)、Pan et al. (2023)、Ganguly et al. (2024) 与 Amazon Web Services (2025) 用求解器辅助推理；Azerbayev et al. (2023) 与 Jiang et al. (2023) 被作者用来说明形式演绎假定初始翻译精确。Li et al. (2024) 与 Ganguly et al. (2025) 被作者放在“严格参考等价而非仅结构执行”这一上游问题上。
• 结构检查：Wang et al. (2023) 与 Singh et al. (2026) 的自一致性、Lu et al. (2025) 与 Amrollahi et al. (2026) 的回译，被作者称为能可靠拒绝无效编码。Beer et al. (2001) 与 Ammons et al. (2002) 被引用以说明通过结构检查并不保证参考等价。作者认为，若参考等价编码与 VPU 变异给出相同求解器判定，这些检查无法把二者分开。
• 学习验证与测试时计算：Zhang et al. (2025a) 的生成式验证器与 Lightman et al. (2024) 的奖励模型改进测试时计算分配（Kang et al., 2025）。Bengio et al. (2009) 的课程式难例与 Chen et al. (2024) 的选择性分配被作者用作训练与部署背景。作者称 GenV+HN 与标准验证器不同：它从预言机标签学习诊断性、无参考的生成式读出，并用程序化硬负例优化。
• 基线方法与基准：第 5 节的对照包括 K=5 自一致性、直接求解器判定、与 GenV 同为 27B 基座的 Process RM（Zhang et al., 2025b）和 Outcome RM（Lyu et al., 2025），以及 GTED（Liu et al., 2025）、FormalAlign 式双向对齐（Lu et al., 2025）和往返回译（Amrollahi et al., 2026）。主基准是 950 条真实翻译器输出；OOD 形式风格来自 FOLIO、ProofWriter、MALLS、ProverQA、ProntoQA、LogicNLI。

作者把本文与上述工作的区别放在：用离线双向 Z3 等价标签训练一个部署时只需 (x, s) 的连续分数，并把评测目标定为判定保持的非等价，而不是结构上能否执行。

整体思路是把特权信息留在训练：用 Z3 制造精确标签，再把该信号蒸馏进 GenV 的原生词表读出；部署的 GenV+HN 不再需要指定参考。

问题设定与形式化

• 对象：x 为自然语言问题，s 为候选 SMT-LIBv2 编码，s⋆ 为指定参考。A(s) 是 s 中断言的逻辑合取，v(s) ∈ {sat, unsat}。
• 参考等价：对与参考签名兼容的候选，Eq(s, s⋆) 为双向蕴含指示：A(s) ∧ ¬A(s⋆) 不可满足，且 A(s⋆) ∧ ¬A(s) 不可满足。作者称该检验在所选签名下是模型论等价，对操作目标是精确的，但仍相对 s⋆；签名不兼容的保义重构，或对欠指定 s⋆ 的合法增补，可能需要进一步规范化才得到预期标签。
• VPU 与信息界：VPU(s; s⋆) 要求判定相同且 Eq 为假。Proposition 1 称，配对集中正例参考等价、负例为 VPU 且两者判定相同；任何 g(s)=h(v(s)) 都会给配对打出相同分数，平局按半信用计时经验 AUROC 为 0.5。作者称该命题不适用于检查 x、s、执行轨迹或内部状态的系统。

离线标签与硬负例

• 标签：对每个问题持有 s⋆。候选来自真实翻译器输出和对 s⋆ 的小幅编辑 μ(s⋆)，例如翻转比较。Z3 双向检查，单向一致不够；通过者为参考等价，仍能运行、判定相同但语义不同者为 VPU。作者称标签在指定签名与资源限制下确定，无需逐条人工标注。训练标签 y_ref = Eq(s, s⋆)。
• 硬负例：变异包括翻转关系算子、扰动常数或反转蕴含。s′=μ(s⋆) 仅在语法正确且满足 Definition 1 时保留；Z3 丢弃意外保持语义的变异。作者称初始分析中残余错误集中在高度结构化理论（如位向量与未解释函数），挖掘用来隔离该边界。
• 数据划分：GenV 只用语言模型生成的 2,591 条（1,894 等价、697 VPU）。GenV+HN 在此之上继续训练 732 条挖掘硬负例，等价:VPU 为 57:43。训练与挖掘用的自然语言问题与全部评测划分严格不相交。

生成式读出与训练

• 读出：固定系统提示把模型约束为裁判，输出单个判断 token（附录 D 给出完整提示词）。c(x, s) 为上下文，π 为下一 token 分布。Y、N 分别是正、负答案的词表 token ID。一次前向后把两类概率质量归一化：f_θ(x, s) = (Σ_{u∈Y} π_u) / (Σ_{u∈Y} π_u + Σ_{u∈N} π_u + ε)，ε=10^{-9}。作者称靠近 1 表示等价，靠近 0 表示 VPU。
• 优化：27B 指令微调骨干冻结，只训练 LoRA。上下文 token 的损失被屏蔽，只对答案 token 做因果交叉熵；作者称因此不新增随机初始化分类器。s⋆ 只用于构造标签，推理输入是 (x, s)。
• 分数用途：Figure 2 称该分数用于 VPU 标记、Best-of-N 选择和智能体门控。作者在局限中称它被设计用于检测与计算分配，而不是生成式导向。

诊断定位（不作为因果机制）

• 前缀分数：F_t = f_θ(x, s_{≤t})，F_0 为仅声明的前缀；预测错误步是下降最大的断言。作者称显式训练来给前缀打分的验证器，在全部 150 个留出变异上定位正确；更强检验使用冻结的、只做检测的 GenV+HN。
• 决策投影：决策间隔 g 为 Yes 与 No 两类 logits 的 logsumexp 之差；q_{ℓ,t} 是 g 对中间激活 h_{ℓ,t} 的梯度与该激活的内积。作者称这是一阶归因，用作诊断，不声称因果机制或局部工作空间。SAE 作用于第 48 层：z = TopK(W_E(h−b), K)，重构为偏置加解码。作者把这些分析称为诊断而非因果。

实验设置

• 验证器：冻结 27B 指令微调骨干，LoRA 训练。GenV 为无挖掘负例的变体；GenV+HN 为部署模型。对照为同基座、同训练流形与优化预算的 Process RM、Outcome RM（token head）、K=5 自一致性、求解器判定匹配。扩展划分另比 GTED、FormalAlign（fwd+bwd）、无参考往返回译。
• 主检测集：950 条真实翻译器编码，来自 197 个源问题，排除变异生成的测试负例，含 260 个 VPU；评测标识与训练标识不相交。文本规范化审计发现 298 行的源陈述在不同标识下训练时见过，故另报 652 行保守子集。扩展划分为 488 行、184 个 VPU。
• OOD 与下游：FOLIO、ProofWriter、MALLS、ProverQA、ProntoQA、LogicNLI 的指定参考被译成 SMT-LIBv2 并挖掘判定保持变异。下游为自适应 Proof of Thought 与静态 Best-of-N。智能体表覆盖 12 个后端、9 个推理基准；Table 6 的显著性为 8,420 条合并轨迹上的精确配对 McNemar，p<0.05。Table 7 为 8 个后端 × 9 个数据集 = 7,200 个 K=5 池。
• 指标：检测为 AUROC；下游为答案准确率及点数差。论文未报告主检测 AUROC 的重复次数。争议切片另有独立 LLM 评审面板，比较 Z3 参考等价与面板多数意图；评审模型名称论文未在正文写明。
• 训练预算：作者称 LoRA 约 12 GPU 小时、单张 NVIDIA H100-80GB；评测与智能体循环用 bf16。

主结果

据 Table 1。Panel (a) 为 950 行、260 个 VPU；panel (b) 为 488 行、184 个 VPU，“rf”表示推理时无参考。

系统	划分	AUROC
GenV+HN	(a) 950 行	0.961
GenV（无挖掘负例）	(a)	0.956
Self-consistency vote (K=5)	(a)	0.863
Outcome RM (token head)	(a)	0.762
Process RM (token head)	(a)	0.756
Solver-only (verdict match)	(a)	0.500
Generative readout, ours rf	(b) 488 行	0.950
GTED / FormalAlign / Round-trip	(b)	0.835 / 0.752 / 0.578

• 作者解读：作者称求解器判定匹配为随机水平 0.500；Process RM 与 Outcome RM 分别为 0.756 与 0.762；K=5 自一致性为 0.863，低于一次生成式等价前向。文本不相交的 652 行子集上，GenV+HN 为 0.955。
• 读出消融（Table 2，original split）：整段编码监督下，生成式 P(Yes) 为 0.983；二分类头暖启动 0.921、冷启动 0.920。逐步 token head 加 min 聚合：PRM 标签 0.633，ORM 标签 0.827。作者称在所评监督与初始化下，词表空间读出相对二分类头还有额外提升，并把 Yes/No 换成 A/B 或 X/Y 仍稳健；论文未在表中给出后一替换的数字。
• 例外：Table 2 的 0.983 高于 Table 1 的 0.961，二者划分不同（original split 对 combined benchmark），论文未把二者写成同一设置。

零样本形式风格

• 测了什么：Table 3 在公开 VPU 集上比较 G-20 readout、GenV、Process RM、Outcome RM 与 GenV+HN。这些集合是各数据集指定参考的合成、预言机认证变异。
• 结果：GenV+HN 为 ProverQA 0.964、MALLS 0.925、ProntoQA 0.915、ProofWriter 0.842、FOLIO 0.830、LogicNLI 0.642；域内行 GenV+HN 0.961、GenV 0.956。作者称 Process RM 与 Outcome RM 在 ProverQA、LogicNLI 上未超过 0.600：表中 Process RM 为 0.588 与 0.559，Outcome RM 为 0.528 与 0.577。
• 作者的解读与例外：作者称生成式读出能超出训练中的特定理论。FOLIO 上 Process RM 为 0.774，高于 GenV 的 0.595，低于 GenV+HN 的 0.830；G-20 在域内为 0.959，略低于 GenV+HN。

意图对齐与测试时分配

• 争议切片（Table 4）：以 Z3 对指定参考的等价为目标时，GenV+HN 为 0.907，Judge 为 0.654；以面板多数意图为目标时，GenV+HN 为 0.679，Judge 为 0.778。作者称严格参考等价是可复现的形式评测目标，并认为消解非正式歧义仍是开放问题。Table 1(b) 的生成式读出为 0.950，高于 GTED 0.835、FormalAlign 0.752、回译 0.578。
• 同一记录池回放（Table 5）：单次 PoT 0.655；Best-of-N（vote@5 对单次）到 0.748（+9.3）；GenV+HN 门控升级到 0.760（+1.2）；验证器选择到 0.768（+0.9）。完整自适应系统相对单次 PoT 为 +11.3 点。求解器门控对照为 0.768→0.758（−1.0）；等预算下建议反馈相对无反馈，71/72 次翻转，作者记为约 0。
• 分后端：Table 6 的合并 Δpts 从 Qwen3-32B 的 +2.3（文中未标星）到 gpt-oss-20b 的 +42.6∗；Claude Opus 4.7 为 +2.6∗。作者称个别数据集有小的正负波动。Table 7 的静态重排：gpt-oss-20b 相对 1-shot +14.2∗，Qwen3-32B +11.8∗；合并为 +7.0∗ / 相对 Vote@3 +0.6∗。作者称等 K=5 预算下相对 vote@5 有轻微回退，因此把优势归于动态门控而不是静态重排器。正文示例“+14.2、+11.8”与 Table 7 一致。

其他消融与分析

• Figure 3A：作者称检测专用的 GenV lens 在无定位训练时定位留出变异；图中标注 GenV lens 0.82、GenV prefix 0.75、ORM head 0.36、PRM head 0.22，chance 标在 0.2。显式前缀模型对 150 个留出变异全部定位正确。
• Figure 3B 与 SAE：图中 GenV+HN 标注 output、SAE、1 feature 为 0.96、0.90、0.88。正文称稀疏特征线性探针恢复 0.960 AUROC；PRM 与 ORM 的隐藏状态比其部署输出暴露更多 VPU 信息。作者称分析未干预激活，因此不建立因果机制。
• 附录逐步示例：四对上 GenV+HN 的 min 聚合平均 Δ 为 +0.9431，独立逐合取定位 4/4；PRM 为 1/4，作者称因果注意力把缺陷泄漏到后续步；ORM 无步轴。该示例分母为 4。
• 负面结果：LogicNLI 上 GenV+HN 为 0.642；求解器门控比已交付门控低 1.0 点；建议反馈在不扩大采样预算时，作者称未带来可测的准确率改进。不可满足公式在标准 Z3 模型检查下空泛等价，作者称遗漏无法靠等价识别；基准中金参考在评测前均被验证为可满足。

作者指出的局限与后续方向

• 意图差距：第 9 节称 GenV+HN 优化的是 Z3 预言机下的严格参考等价，而不是主观人类意图；弥合该语义差距需要未来的人工标注基准（Appendix B）。
• 监督边界：第 9 节称监督受 SMT 可判定性限制，并假设金参考被完全指定。
• 分布偏移：第 9 节称验证器能零样本跨架构迁移，但形式逻辑风格上的严重分布外偏移会改变分数分布并降低阈值校准（Appendix C）。
• 变异类型：第 9 节称 VPU 挖掘依赖合成的单次编辑，可能无法完全捕捉自然程序中相关的、多错误分布。
• 用途与机制：第 9 节称部署中它用于检测和计算分配，而不是生成式导向；把分数当作建议反馈，若不扩大采样预算，不会带来可测的准确率改进（Appendix C.3）。梯度透镜与 SAE 被作者称为诊断工具；把这些内部表示扩展到因果地引导多错误修复流水线，被写成神经符号架构的开放前沿。
• 不可满足情形：第 9 节称逻辑等价保证适用于可满足的形式规约；标准 Z3 模型检查下两个不可满足公式空泛等价，因此不一致参考公式中的遗漏无法通过等价识别。

实验覆盖范围

• 检测数据：主结果在 950 行真实翻译器输出（197 个源问题、260 个 VPU）和 652 行规范化文本不相交子集上报告；扩展对齐比较为 488 行、184 个 VPU（第 5–6 节，Table 1）。
• 训练构成：GenV 使用 2,591 条语言模型候选（1,894 等价、697 VPU）；GenV+HN 另加 732 条硬负例，类分布 57:43（第 5 节）。
• OOD 风格：零样本 AUROC 覆盖 FOLIO、ProofWriter、MALLS、ProverQA、ProntoQA、LogicNLI，负例为各数据集指定参考的合成变异（Table 3）。
• 下游协议：自适应结果在 12 个后端、9 个基准上比较 PoT 与 +GenV，显著性检验为 8,420 条合并轨迹（Table 6）；静态重排为 8 后端 × 9 数据集共 7,200 个 K=5 池（Table 7）。机制回放使用同一记录池（Table 5）。
• 分析范围：定位实验使用已知单次编辑的合成例；显式前缀打分模型覆盖 150 个留出变异。SAE 取第 48 层。论文写明主检测指标为 AUROC，未报告该 AUROC 的重复次数；争议切片的评审模型名称在正文未写出。附录 D 给出裁判提示词。

GenV+HN 针对神经符号翻译之后、求解器证书之前的对应失败：编码可以与指定参考共享求解器判定，同时并不等价。

• 问题：作者把语法合法、判定与 s⋆ 相同且双向蕴含失败的候选定义为 VPU。Proposition 1 称，只看二元判定的分数在这类配对上 AUROC 为 0.5。
• 方法：训练时用 Z3 做双向等价标注，候选来自翻译器输出和对金参考的程序化变异。冻结 27B 骨干，只训练 LoRA，损失只落在 Yes/No 答案 token；一次前向把两类概率归一化成 [0,1] 分数。部署不再使用 s⋆。GenV+HN 在 2,591 条真实候选之外继续使用 732 条硬负例。
• 检测：950 行、260 个 VPU 的真实输出基准上，GenV+HN 为 0.961，GenV 为 0.956，K=5 自一致性为 0.863，Outcome RM 与 Process RM 为 0.762 与 0.756，求解器判定匹配为 0.500（Table 1a）。652 行文本不相交子集为 0.955。Table 2 的整段编码、生成式 P(Yes) 设置为 0.983。
• 迁移与下游：Table 3 中 GenV+HN 在 ProverQA 为 0.964，在 LogicNLI 为 0.642。同一记录池上，完整自适应系统相对单次 PoT 从 0.655 到 0.768（+11.3 点，Table 5），其中 Best-of-N 本身占 +9.3。以面板多数意图为目标时，GenV+HN 为 0.679，低于 Judge 的 0.778（Table 4）。
• 作者的结论：作者认为判定有效性不能代替参考等价；生成式读出在未见翻译器与形式风格上维持约 0.96 的 AUROC，并把内部信号暴露为可诊断的定位信息。作者同时认为该保证限于可满足规约、受形式风格偏移与人类意图歧义约束，且当前内部分析不是因果修复机制。