論文解説: Beyond Solver Verdicts — ソルバーが「正しい」と言っても翻訳は間違っているかもしれない
LLMが自然文を論理式に翻訳し、Z3が解く。ソルバーの答えが合っていても翻訳が誤っている「VPU」という失敗を定式化し、Z3の等価判定をYes/Noの次トークン確率に蒸留する検証器GenVを提案した論文を、前提知識ゼロから解説します。
要点
- Verdict-Preserving-Unfaithfulness（VPU）とは、判定は正解と同じだが論理的には等価でない形式化の失敗である。
- ソルバーが保証するのは渡された式から言えることまでで、式が問題文を正しく表すかは保証しない。
- ソルバーの判定だけを入力にするスコアは、正しい候補とVPU候補に同点を付け、AUROCは0.5になる。
- 著者らはZ3の等価判定を正解不要の連続スコアに蒸留するGenerative Verification（GenV）を提案している。
- ハードネガティブで鍛えたGenV+HNは、正解との等価性判定でAUROC 0.961を出した。
Beyond Solver Verdicts: Generative Reward Models for Autoformalization
一次資料 — この記事の根拠
論文の発表 2026-09-10→この解説の公開 2026-09-24同月
Beyond Solver Verdicts: Generative Reward Models for AutoformalizationVikash Singh, Debargha Ganguly, Aman Goel ほか · 2026-09-10 · v2arXiv:2609.11085論文ページ·PDF原文の要旨（Abstract）を読む
Neurosymbolic systems rely on mathematical solvers to guarantee reasoning correctness, yet solvers are fundamentally blind to whether a formal translation maintains strict reference-equivalence to a designated formalization. We formalize this vulnerability as Verdict-Preserving-Unfaithfulness (VPU): a failure mode where an incorrect encoding executes successfully and matches the expected verdict. We theoretically prove that structural, verdict-only verification heuristics are mathematically bounded to chance-level detection on these deceptively valid traces. To resolve this, we introduce Generative Verification (GenV), which distills an offline Z3-equivalence oracle into a reference-free, continuous reference-equivalence score by repurposing the language model's native vocabulary space. Mechanistic analysis via decision-projected logit lenses and sparse autoencoders shows this generative readout natively extracts precise spatial error coordinates without explicit localization training. Empirically, our oracle-mined verifier (GenV+HN) achieves 0.961 AUROC in reference-equivalence verification, generalizes zero-shot across unseen translators and divergent formal styles, and yields an 11.3-point downstream accuracy gain in agentic test-time compute allocation.
この論文は何を言っているのか
今回読むのは "Beyond Solver Verdicts: Generative Reward Models for Autoformalization"（Singh ほか, arXiv:2609.11085, 2026年9月）です。Case Western Reserve University と Amazon Web Services の共同研究です。
アブストラクトの主張を日本語でまとめると、次のとおりです。LLMの推論を数学ソルバーで裏付ける「ニューロシンボリック」なシステムは、ソルバーのおかげで推論の正しさを保証できるとされてきました。ところがソルバーには、自然文から論理式への翻訳が、指定された正解の形式化と厳密に等価かどうかは見えません。論文はこの弱点を Verdict-Preserving-Unfaithfulness（VPU、判定を保ったままの不忠実） と名付けています。誤った論理式がエラーなく実行され、しかも期待どおりの判定を返してしまう失敗です。著者らは、ソルバーの判定だけを見る構造的な検査では、この種のケースを偶然レベル（当てずっぽう）でしか見分けられないことを証明しました。そのうえで、オフラインで動かす Z3 の等価判定を「正解不要の連続スコア」に蒸留する Generative Verification（GenV） を提案しています。GenV は言語モデルがもともと持つ語彙の出力をそのまま判定に使います。ハードネガティブで鍛えた版の GenV+HN は、正解との等価性判定で AUROC 0.961 を出し、未知の翻訳モデルや別の形式スタイルにも追加学習なしで一般化しました。さらに、エージェントがテスト時の計算をどこに使うかの判断に組み込むと、最終的な正答率が 11.3 ポイント上がったと報告されています。
比喩: 電卓は正しい、でも式を写し間違えている
算数の文章題を思い浮かべてください。「りんごは5個より多い」と書いてあるのに、式に写すときに「5個より少ない」と書いてしまったとします。電卓（ソルバー）はその式を完璧に計算します。そして運が悪いと、間違った式でも「答えがある／ない」という結論だけは正しい式と一致してしまいます。
採点者が「結論が合っているか」しか見ないなら、この写し間違いには絶対に気づけません。論文が扱うのはまさにこの状況です。ソルバーは健全で、嘘はつきません。ただしソルバーが保証するのは「渡された式から何が言えるか」までです。式が問題文を正しく表しているかどうかは保証してくれません（§1）。
VPU: 判定は同じなのに意味が違う
もう少し正確に見ていきます。自然文の問題を 、LLM が書いた SMT-LIBv2 形式の候補コードを 、人が用意した正解の形式化を とします。 は「 の中の制約（assert）をすべて AND でつないだもの」です。
言い換えると、「 は成り立つのに は成り立たない状況」も、その逆の状況も存在しないなら、2つは等価です。 は中身が真なら1、偽なら0を返す記号です。片方向だけ確かめても等価とは言えないので、両方向を Z3 に確かめさせます（§3）。
これを使うと、VPU は次のように定義されます。
はソルバーの判定（sat＝解がある／unsat＝解がない）です。つまり 「判定は正解と同じ」かつ「論理的には等価でない」 のが VPU です。論文の図1の例では、比較演算子 を逆向きにしただけの候補が、正解と同じ sat を返しています。
なぜ判定だけでは原理的に見抜けないのか
論文の命題1（§3）は、とても短い議論です。正しい候補 と VPU 候補 を、判定が同じになるようにペアにした評価セットを考えます。判定だけを入力にするスコア は、どんな関数 を選んでも、ペアの両方に同じ点を付けます。
入力が同じなら出力も同じなので、全ペアが同点になります。同点を半分の正解として数える通常の約束では、AUROC（「正しい方に高い点を付けられる確率」）は 0.5、つまりコイン投げと同じ値になります。
著者らはこの結果の範囲を慎重に限定しています。これは「判定の2値だけを見る方式」の限界です。問題文やコード、実行の痕跡、モデル内部の状態まで読む検証器が VPU を見抜けるかどうかは、実験で確かめるべき問いとして残しています（§1, §3）。
コメント
コメントにはログインが必要です