MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

あなたは、天才的だが少し不器用なロボットに、純粋な論理の言語を教えようとしているところだと想像してください。このロボット、すなわち大規模言語モデル（LLM）は、普通の英語で物語を読み、詩を書き、数学のパズルを解くことには長けています。しかし、一つ問題があります。数学の定理を絶対的な確実性をもって証明するためには、単に言葉を使うだけでは不十分であり、「Lean 4」と呼ばれる非常に厳格なコンピュータ言語で記述しなければならないということです。Lean 4は、あらゆる単語、記号、ルールが完璧でなければ、金庫の扉が開かないような、高度なセキュリティを備えた金庫のようなものだと考えてください。問題は、このロボットは数学を知ってはいるものの、Lean 4が使用する特定の「ルールブック（Mathlibと呼ばれる）」を知らないことです。それは、完璧なステーキを調理する方法を知っているシェフに対して、見たこともない言語で書かれたレシピに従い、名前も知らない食材を使うように頼むようなものです。シェフは推測することはできても、おそらく間違えてしまうでしょう。

ここで「オートフォーマライゼーション（自動形式化）」が登場します。これは、人間の数学を厳格なコンピュータコードへと翻訳する技術です。長い間、研究者たちは、ロボットがトレーニング時の記憶に頼ることを期待して、単に数学を「翻訳」するようにロボットに依頼しようとしてきました。しかし、ロボットは記憶だけに頼ろうとするため、間違った食材を使ったり、重要なステップを忘れたりといったミスを繰り返しました。彼らの手法は、単なる「推測と希望」に基づいたものでした。これに対し、新しい論文「MathForm」は、この「推測しては期待する」というアプローチは壊れていると主張しています。代わりに、彼らはロボットが書き始める「前」にルールブックを検索することを許可し、もし間違いが発生した場合、厳格なエディターが単にその成果物を投げ捨てるのではなく、どこがどう間違っていたのかを正確に伝え、正しくなるまで再試行させるシステムを構築しました。

MathFormの研究者たちは、ロボットに形式的な数学の言語を完璧に話させるためには、ただ下書きを書いて上手くいくのを待つだけでは不十分であることに気づきました。彼らは、ロボットのワークフローを修正するために、3段階の組み立てラインを構築しました。第一に、ロボットがコードを一行も書く前に、「研究者（Researcher）」エージェントが膨大なMathlibライブラリをスキャンし、その特定の問題に必要な正確な定義とルールを見つけ出します。これは、シェフがナイフを手に取る前に、「ステーキ」に関する特定のレシピのページを渡すようなものです。第二に、ロボブルがコードを書くと、次に「検査官（Inspector）」がそれをチェックします。もしコードに構文エラー（カンマの欠落など）があれば、検査官はそれを指摘します。もしコードがコンパイル可能であっても、意味が間違っている場合（例えば、問題が「正の数のみ」を意図しているのに「すべての数」と言ってしまった場合など）は、検査官はその意味的な誤りを説明します。第三に、諦める代わりに、ロボットはこのフィードバックを利用してコードを書き直します。コードが完璧になるまで、この「書く・チェックする・直す」というサイクルを繰り返します。

この巧妙なループを用いて、チームは約36万7千の検証済み数学例を含む、FormalVerseという大規模な新しいデータセットを作成しました。そして、このデータを用いて新しいモデルであるMathForm-8Bを学習させました。結果は驚くべきものでした。この比較的規模の小さいモデル（80億パラメータ）は、従来の「推測と希望」の手法に頼っていた、より大規模な特化型モデル（320億パラメータ）よりも、数学の形式化において優れた性能を示しました。6つの異なる難解な数学テストにおいて、MathForm-8Bは「整合性チェック（つまり、コードが実際に人間の問題が意図するものと一致しているか）」を約72.4%の割合でパスし、従来の最高水準のモデルを打ち破りました。最も困難で抽象的な代数学の問題においてさえ、このモデルはより大きなライバルたちを大幅に上回りました。この論文は、モデルに情報を検索するための適切なツールを与え、間違いから学ぶ機会を与えることで、巨大な脳を持たずとも数学の天才になれることを示唆しています。必要なのは、スマートなワークフローなのです。