arXivは2026年10月4日(現地時間)、Omar Farouk Zouak氏らによる研究論文「Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs」を発表した。本研究は、大規模言語モデル (LLM) が定理の真偽判定において反例生成に課題を抱える「偽証ギャップ」に焦点を当て、教師ありファインチューニング (SFT) がこれを悪化させる可能性を指摘している。検証器を報酬関数とする新たなコーパス「SymCE」を公開し、強化学習によって反例生成能力が改善されることを示した。
論文では、LLMが定理を順方向に解決できる一方で、密接に関連する誤った定理の反証には失敗する「偽証ギャップ」が存在すると説明している。このギャップはSFTでは解消されず、能動的に悪化させる場合がある。研究チームは、反例生成を、定理ごとにPythonで実装された決定論的な検証器に対する制約付き証拠放出として捉える枠組みを提案した。
公開されたSymCEは、大学レベルの代数学および実解析における4,707の誤った推測のコーパスであり、それぞれ実行可能な検証器と対になっている。この検証器は報酬関数としても機能し、SymCEは訓練環境としても活用できる。Qwen3-4Bモデルに対し、SFT後にGRPOを用いた訓練を行った結果、「模倣の罠」と呼ばれる現象が明らかになった。反例のみのSFTは、真の定理認識率を0.27から0.00にまで低下させた。
これに対し、希薄な結果のみの報酬を用いたRLVR（Reinforcement Learning with Verifier Rewards）は、この問題を0.66まで改善し、SFT後のベースライン性能を超えた。この認識率の低下は4つの異なるシードとGemma-3-4Bモデルでも再現された。希薄報酬と密な報酬は、ドメイン内での成功においては統計的に区別できないものの、ホールドアウトされたキャリブレーションプローブでは33ポイントの差が生じ、この乖離は部分クレジット項に起因すると分析されている。
本研究で開発された4Bモデルは、評価対象となったすべての7Bオープンウェイト数学専門モデルを上回り、6つの最先端商用APIとも競合する性能を示した。また、GSM8K、MATH-500、MMLU-college-mathといったベンチマークにもプロンプトを変更せずに転移可能であることが確認された。177件の検証器判定に対する人間による監査では、97.7%の精度が確認された。本研究はEMNLP 2026 Findingsに採択された。
参考: arXiv cs.CL — 2026年10月5日 13:00 (JST)
原文ハイライト"When Imitation Hurts and Reinforcement Repairs"