技術的サマリー：自然言語数学推論のためのリスク制御型 Lean-as-Judge

1. 問題定義

本論文は、大規模言語モデル（LLM）によって生成された自然言語の数学的推論に対し、形式証明アシスタント（特に Lean）をジャッジとして用いる際の課題に取り組む。成功した Lean 証明は形式化された命題に対する強力な肯定的証拠を提供するが、証明の欠如は曖昧なシグナルである。証明の失敗は数学的に誤った回答を示唆する可能性もあるが、同様に、不適切な型付けの形式化、欠落したライブラリ事実、または証明探索のタイムアウトに起因する可能性もある。

現在の手法は、証明の失敗を否定的な正しさのシグナルとして扱うことが多く、数学的な誤りと形式化カバレッジの欠如を混同するリスクを孕んでいる。著者は「カバレッジの崖（coverage cliff）」を特定している：形式選択の信頼性は、成功して形式化され証明された候補回答の割合に鋭く依存する。カバレッジが高い場合、形式選択は極めて正確であるが、カバレッジが低い場合、そのシグナルは信頼できなくなる。

核心的な問題は、下流システムがいつ形式 Lean シグナルを信頼すべきか、またいつそのシグナルを「カバレッジ外（すなわち未解決）」として扱い、「誤り」として扱わないべきかを決定し、かつ受け入れられた回答に対して有限サンプルのリスク保証を提供することである。

2. 手法：COVCAL

著者は、カバレッジ診断に基づいて形式回答の受諾または棄権を決定する、リスク制御型の選択的ラッパーであるCOVCAL（Coverage-Calibrated Lean）を提案する。

2.1 部分観測フレームワーク

本システムは、形式パイプラインを部分観測メカニズムとして扱う。すべての候補回答の真偽を観測するのではなく、以下の事項のみを観測する：

1. どの正規化された回答クラスが Well-formed な Lean 文に到達したか（型付きカバレッジ）。
2. その中のどのクラスが成功して証明されたか（証明済みカバレッジ）。
3. 最高重みの証明済みクラスと、最高重みの未解決の競合クラスとの間の重みの差（形式マージン）。

回答クラスとは、同じ最終回答を表す候補文字列のグループとして定義される（例：$1/2$、$0.5$、$2/4$）。形式化されなかったり証明されなかったりしたクラスは、自動的に誤りと見なされるのではなく、未解決とみなされる。

2.2 カバレッジ診断

COVCAL は、与えられた問題 $x$ に対して 4 つの主要な指標を計算する：

• 型付きカバレッジ（$C_{typ}$）：Well-formed な Lean 文に到達した（ステータス：proved、typechecked、またはtimeout）候補クラスの総重み。
• 証明済みカバレッジ（$C_{prf}$）：カーネルチェック済みの証明を得た候補クラスの総重み。
• 未解決競合質量（$R_{unres}$）：証明されなかった最高重みの回答クラスの重み。
• 形式マージン（$M$）：最高重みの証明済みクラスの重みと未解決競合質量との差。

2.3 選択と認証

COVCAL は、閾値 $(\tau_{typ}, \tau_{prf}, \tau_M)$ に基づく事前宣言されたルールが満たされた場合にのみ、最高重みの証明済みクラスを受諾する。ルールが満たされない場合、システムは棄権する（または自己整合性などの非形式的手法にフォールバックする）。

信頼性を確保するため、COVCAL は有限サンプル選択的リスク認証を採用する。確率 $1-\delta$ で、受諾された回答の選択的リスク（誤り率）が最大 $\epsilon$ であることを保証する。2 つの認証レジームが提案されている：

1. ボンフェローニ・レジーム：キャリブレーション分割上の閾値のグリッドを探索し、多重比較を考慮するためにユニオンバウンド補正（$\delta/|T|$）を適用する。これは保守的であり、実行可能となるには高いシグナル密度を必要とする。
2. Dev-then-Cal レジーム：独立した開発分割上で閾値を選択し、単一の Clopper-Pearson 境界（$\delta$）を使用してキャリブレーション分割上で一度認証する。これはよりサンプル効率的であるが、開発データとキャリブレーションデータの厳密な分離を必要とする。

2.4 理論的限界

本論文は、カバレッジ診断なし（すなわち、証明の存在のみに依存）では、未解決で不等価な競合クラスが存在する場合、非空虚な点ごとの正しさの証明を導出できないことを証明している。欠落した形式証拠は数学的偽りの証拠ではなく、未解決の状態の証拠である。

3. 主要な貢献

1. カバレッジの崖の特性評価：MATH-500 データセットにおいて、著者は「証明が勝つ」回答が、証明済みカバレッジが高い場合は 96% の確率で正しく、カバレッジが低い場合は 20% しか正しくないことを実証した。これにより、Lean 証明はカバレッジとマージンが高い場合にのみ信頼性があることが確立された。
2. シグナルの疎性と忠実性：形式シグナルは疎で不完全である。7B オートフォーマライザーは問題の 28% に対してのみクラスを証明する。さらに、手動監査により、これらの証明の約 43% だけが元の問題に忠実であることが判明した（残りは自明な同一性または真だが無関係な命題である）。
3. COVCAL 手法：部分観測下でリスクを認証する選択的予測フレームワーク。証明失敗の非対称性を明示的に処理し、受諾された予測に対して有限サンプル保証を提供する。
4. フォーマライザー依存の実現可能性：本論文は、証明書の実現可能性がオートフォーマライゼーションのカバレッジによって支配されることを実証している。7B フォーマライザーは、シグナルがボンフェローニ・レジームの厳格なユニオンバウンドを満たすにはあまりに疎であるため（20 のブートストラップ分割すべてを棄却）、結果として生じるが、証明に特化したフォーマライザー（Goedel-Prover-V2-8B、79% のカバレッジ達成）を使用すると、20 分割のうち 17 分割で手法が実現可能となる。

4. 実験結果

実験は、Qwen2.5-Math-7B による生成と各種フォーマライザーによるオートフォーマライゼーションを用いて、MATH-500 のフィルタリングされた部分集合（378 例）で行われた。

• ベースライン性能：棄権なしの自己整合性のみで 91% の精度を達成。
• COVCAL 性能：
  • 7B フォーマライザーを用いたボンフェローニ・レジーム下では、シグナルが厳格なユニオンバウンドを満たすにはあまりに疎いため、すべての入力が棄却された（20 分割中 0）。
  • 7B フォーマライザーを用いたdev-then-cal レジーム下では、20 分割中 12 が認証された。受諾割合は約 21% で、受諾精度は 0.93 だった。
  • Goedel-Prover-V2-8B（特化型フォーマライザー）を使用すると、証明済みカバレッジは 79% に上昇する。ボンフェローニ・レジームは 20 分割中 17 で実現可能となり、約 48% の問題を受諾し、受諾精度は 0.98 となった。
• 忠実性監査：45 例の層化されたサンプルの手動監査により、証明された命題の 73.6% が非自明で正しいものであったが、問題文に忠実だったのは 43% だけであることが示された。多くの「証明済み」命題は、問題の制約を捉えていない真の副次的事実や自明な同一性であった。

5. 意義と主張

本論文の主要な貢献は、単に生精度を向上させることではなく、リスク制御の下で、いつ、どのフォーマライザーを用いれば部分的な形式シグナルを信頼できるかの精密な説明にある。

• 生精度に対するリスク制御：自己整合性ですでに 91% の精度を達成しているため、COVCAL の価値は、受諾する回答のサブセットに対して証明を提供し、「検証済み」と「未解決」を「正解」と「不正解」から区別する能力にある。
• 部分観測の処理：本作業は、形式検証を、欠落した証明を未解決候補として扱う選択的予測問題として再定義し、形式化の失敗により正しい推論が誤りと誤ってラベル付けされるのを防ぐ。
• 特化への依存：結果は、生モデルの規模が特化の代わりにはなり得ないことを浮き彫りにしている。証明カバレッジという、認証可能なリスク制御の拘束条件において、証明に特化したフォーマライザーは、より大規模な一般モデルを大幅に上回る。

著者は、COVCAL は Lean をジャッジとして使用する際の保守的なインターフェースとして機能すると結論づけている。それは、リスク証明を支援するのに十分な回答質量をオートフォーマライザーがカバーしている場合にのみ実現可能かつ有益であるが、すべての回答が検証されることを保証するものではない。