GenV: 为自动形式化引入生成式验证, 超越求解器判定

摘要

研究指出，符号系统依赖数学求解器保证推理正确性，却无法判断形式化翻译是否与指定的形式化保持严格等价。作者将此漏洞形式化为“判定保持性不忠实”（Verdict-Preserving-Unfaithfulness, VPU）：错误编码仍能成功执行并得到预期判定；并从理论上证明，仅依赖判定的结构性验证启发式在这类“看似有效”的轨迹上，检测能力在数学上被限制在随机水平。为此提出生成式验证 GenV，将离线 Z3 等价预言蒸馏为与参考无关的连续参考等价分数，复用语言模型原生词表空间。经决策投影 logit lens 与稀疏自编码器的机制分析显示，该生成式读出无需显式定位训练即可提取精确的误差坐标。其预言挖掘的验证器 GenV+HN 在参考等价验证上达到 0.961 AUROC，能对未见过的翻译器和不同的形式风格零样本泛化，并在 agentic 测试时算力分配中带来 11.3 个百分点的下游准确率提升。