GenV 精读：把 Z3 等价性判定蒸馏成语言模型的"第六感"
题目：Beyond Solver Verdicts: Generative Reward Models for Autoformalization 链接：https://arxiv.org/abs/26085.11085 → https://arxiv.org/abs/2609.11085 团队：Case Western Reserve University × Amazon Web Services（Vikash Singh 等，实习期完成） 数据日：2026-09-11
一、题目与背景
Autoformalization——把数学陈述从自然语言转成形式化语言（Lean/Isabelle）——是形式化数学与验证智能体的地基。求解器（Z3 等）是这个领域最可靠的裁判，但论文开篇点破其根本局限：sound solver 只认证"给定编码下"的推导有效，不认证"编码忠实表达了原意"。一句话：求解器能证明你写的形式化命题，不能证明你翻译对了。
更麻烦的是欺骗性轨迹：翻译错误的形式化版本在句法上完全合法、证明也通畅——过程与结果都"看起来对"，只有语义层面对照原文才能识别错位。论文证明在此类轨迹上，任何仅看轨迹文本的方法（含 ORM/PRM）在数学上有界于随机水平。
二、研究定位
处于 reward model 研究与程序推理的交叉。与标准 GenRM 的差异：多数 GenRM 蒸馏人类偏好或结果标签；GenV 蒸馏的是一个可精确执行的等价性判定程序（Z3 脚本）——标签源头从"人类觉得"换成"机器证得"。这继承了"oracle 蒸馏"谱系（如 AlphaProof 系的验证器利用），但创新点在蒸馏目标是等价性这一关系判断而非对错判断，且配了完整的机制可解释性分析。
三、问题定义
训练一个奖励模型 $r(\text{原文}, \text{形式化}) \to [0,1]$，使其在无参考翻译（reference-free）条件下输出"该形式化与原文语义等价"的连续分数。约束：可用于 RL 训练循环（可微、低成本），且能区分"表面合法、语义错位"（VPU，valid-but-unfaithful）与真等价。
四、解法
GenV（Generative Verification）：
- 离线 Z3 oracle：对（原文，形式化）对构造 Z3 可判定的等价性检查脚本（可判定的片段上运行），产出精确二元标签+反例 witness。
- 生成式读出：不训练独立的打分头，而是复用 LM 的原生词表空间——让模型"生成"等价性判断（类似把分类伪装成生成），连续分数从生成分布读出。这个设计让等价性信号与模型的自然语言理解共享表示。
- 程序化 hard negatives（HN）：用程序变换制造"几乎等价但关键量错位"的难负例（交换量词、偏移常数、换谓词）——强迫模型学到精确的边界而不是粗粒度"像不像"。
- 机制验证：decision-projected logit lens + 稀疏自编码器（SAE）分析——确认等价性信息真实存在于残差流中且被读出，而非数据集伪迹。
五、实验结果
| 模型 | VPU Precision | VPU Recall | F1 | ECE |
|---|---|---|---|---|
| GenV+HN（本文） | 0.854 | 0.812 | 0.832 | 0.069 |
| GenV（无 HN） | 0.824 | 0.792 | 0.808 | 0.050 |
| Process reward model | 0.562 | 0.158 | 0.246 | 0.119 |
| Outcome reward model | 0.439 | 0.585 | 0.502 | 0.13 |
两个结构性发现：其一，PRM 在 VPU 上接近随机（F1 0.246）——过程奖励学到的是"推理流不流畅"，与"翻译忠实"正交；其二，机制分析显示 GenV 的读出天然提取空间/结构化的错误坐标（错在哪个量词、哪个谓词），具备定位能力而不只是打分——这是生成式读出相对打分头的隐藏优势。
六、知识反推
- “精确但贵"的判断可以被蒸馏成"近似但廉"的直觉。Z3 每次判定要写脚本跑求解，GenV 一次前向就出分——中间损失的精度（F1 0.83 vs 1.0）换来三个数量级的速度，RL 循环因此可行。oracle 蒸馏是把符号系统引入神经训练的通用桥：任何你有确定性判定器（测试、类型检查、linter）的场景都可复制。
- hard negative 的"程序化制造"优于人工挖掘。交换量词/偏移常数的变换生成器产出无限多边界样本且缺陷位置已知——监督信号自带定位。这比从真实数据挖负例便宜且分布可控。
- 机制可解释性是 reward model 的质检工序。logit lens/SAE 验证信号存在于残差流——排除了"模型在走捷径”（如记住了 Z3 判定的表面统计）的解释。给关键组件配机制验证正在成为顶会论文的标配环节。
七、通用灵感
- 给代码评审 Agent 蒸馏一个"语义等价"奖励：你的系统里同样存在"补丁合法但不解决问题"的 VPU 类样本——用测试套件/静态检查当 oracle 离线打标，训练评审模型的等价性直觉，替代昂贵的运行时全量验证。
- 用"生成式读出"统一打分与定位：需要"分数+哪里错"双输出的场景（评审意见、缺陷预测），让模型生成结构化判断再解析，比双头设计更一致。
- 变换式负例生成器值得做成团队工具：对代码（算子交换、边界偏移）、对文档（否定注入、限定词替换）各写一组保形变换，自动扩充训练负例——NSD 的负条件构造与这里是同一套思想。