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

形式化求解器能确认推理结果，却无法识别代码翻译是否偏离了题意本身。论文将这种“结论正确但形式失真”（VPU）的形式化盲区形式化证明，并提出 GenV，将 Z3 等价性预言机蒸馏至语言模型的原生词表空间。该模型在无参考验证中取得 0.961 AUROC，并让测试期算力分配的下游精度提升了 11.3 个百分点。