LeanPRM、形式証明で自然言語による数学推論を段階的に監督

数学証明の検証が難しい理由

大規模言語モデルは、長く複雑な数学証明を生成できるようになっている。しかし、文章が自然であることと、各推論ステップが正しいことは別問題だ。開放型の証明では、最終的な答えだけを確認しても途中の誤りを見つけられない。かといって、すべてのステップを人間が確認してラベル付けする方法は、コストも時間も大きい。

LeanPRMは、形式証明支援系Leanを使って、このプロセス監督用データを自動的に作る枠組みを提案する。自然言語の説明と、機械的に検査できる形式証明を対応させる点が中心となる。

LeanPRMの仕組み

• 二つの証明を同時に生成：モデルは自然言語証明と対応するLean証明を作る。生成時にはLeanからフィードバックを受けない。
• ステップ単位で検査：Leanが形式証明の各ステップをチェックし、正誤の信号を提供する。
• 形式化由来の失敗を除外：形式証明が通らない理由は、数学的な誤りだけとは限らない。文法や自然言語との対応付けが原因の場合もあるため、別のモデルでこうした失敗をフィルタリングする。
• 人手なしでデータ化：10,634件の証明と約15.2万件のラベル付きステップを収録する。

実験で示された改善

200件の留保証明から成るLeanPRM-Benchでは、LeanPRMで学習したQwen3-4B検証器のステップラベル完全一致精度が74.7%に達した。比較対象としてPRM800Kで学習した同じ規模のモデルは60.3%で、報告されたベースラインは48.2%だった。LeanPRMはIMOレベル問題におけるbest-of-Nの証明選択も改善した。また、外部の4つの検証ベンチマークのうち3つで、PRM800Kを使った検証器を上回った。0.6Bから8Bまでのモデル規模で、LeanPRMの学習効果が報告されている。

研究上の意味と注意点

この研究の重要性は、Leanを最終判定器として使うだけでなく、プロセス監督データを生み出す装置として位置付けた点にある。形式システムが実行可能なチェックを担い、言語モデルが自然言語推論と形式表現を橋渡しする。これにより、長い推論を人間が逐一確認する必要性を減らし、検証器により密度の高い学習信号を与えられる可能性がある。

一方で、自然言語証明とLean証明の対応品質には依存する。また、形式化の失敗と数学的な誤りを区別するフィルタリングも必要だ。Leanで受理されたことは、指定された形式環境で命題が成立することを示すが、自然言語の説明が完全か、意図した議論を忠実に表しているかまで自動的に保証するわけではない。

LeanPRMは、数学的推論を全面的に自動評価する解決策というより、検証器を訓練するための拡張可能なデータ生成パイプラインとして見るのが適切だろう。

出典：Hugging Face Daily Papers