Googleの研究は数学の問題をコードに変換することで、機械証明の精度を大幅に向上させた。

コンピュータは以前から数学の証明を検証するために使用されてきましたが、特別に設計された証明言語を使用して問題が準備されている場合にのみ可能であり、数学者が使用する数学記号と文章の混合を処理することはできません。

自然言語で書かれた数学の問題を正式なコードに変換すると、コンピューターが問題を解きやすくなるため、数学における新たな発見ができる機械の構築に役立つ可能性があります。

このプロセスは形式化と呼ばれますが、1 つの証明だけでも何年もの作業が必要になるため、数学のごく一部だけが形式化され、機械によって証明されます。

自動形式化とは、自然言語の数学を形式言語に自動的に翻訳する作業を指します。自動形式化ツールが成功すれば、実用的かつ哲学的に大きな意義が得られ、現在過剰な形式化コストが削減され、長期的にはさまざまな研究分野における数学的推論の自動化された側面が結び付けられることになります。

最近の研究では、Google の Yuhuai Wu 氏とその協力者は、OpenAI Codex のニューラル ネットワークを使用して作業を自動的に形式化しました。 Codex は Web からの大量のテキストとプログラミング データでトレーニングされており、プログラマーはこれを使用して信頼性の高いコードを生成できます。

論文リンク: https://arxiv.org/pdf/2205.12615.pdf

高校数学コンテスト問題12,500問を形式化する

大規模言語モデルにおける最近の多くの進歩は、形式言語を理解するためのモデルの潜在能力を実証しています。しかし、既存の成功例は、Web 上に大規模なコーパスが存在する形式言語 (Python など) に限られています。対照的に、形式的な数学データは非常に不足しています。最大規模の形式的な数学言語ライブラリの 1 つである Archive of Formal Proofs のサイズはわずか 180 MB で、これは大規模言語モデル Codex のトレーニング データの 0.18% 未満です。

さらに、自然言語のドキュメント文字列が広く利用できる汎用プログラミング言語の場合とは異なり、自然言語と形式的な数学言語間の整合に関するデータはほとんどありません。したがって、大規模言語モデルの成功が自動形式化の開発を直接促進できるかどうかは不明のままです。

証明言語とプログラミング言語の類似性を考慮して、チームは Codex が 12,500 個の高校数学競技問題のライブラリを形式化できるかどうかを確認することにしました。問題の 4 分の 1 を、形式証明ソルバー Isabelle と互換性のある形式に変換することができました。

ウー氏は、多くの変換失敗はシステムが特定の数学的概念を理解していないことが原因であると述べた。 「モデルに概念を説明する例を見せれば、モデルはすぐにそれを理解できます。」

この研究は、大規模言語モデルの自動形式化の見通しを探るものであり、研究者らは、大規模言語モデルがすでにインタラクティブな定理証明器で自然言語の数学を形式化するかなり優れた能力を持っていることを発見しました。

下の図 1 は自動形式化の完璧な例です。このモデルは、文法的に正しい Isabelle コードを変換するだけでなく、自然言語の重要な推論ポイントも把握します。

この自動形式化手順の有効性をテストするために、研究チームは、人間がすでに形式化したバージョンがあり、Codex が独自の形式化も生成した一連の問題に Codex を適用しました。チームは、MiniF2F と呼ばれる別の AI を使用して、両方のバージョンの問題を解決しました。

質問を自動的に形式化することで、MiniF2F の成功率が 29% から 35% に向上し、Codex が問題の形式化において重要な進歩を遂げたことがわかります。

多くの数学コンテストにおけるプレゼンテーションは、与えられた命題を証明するのではなく、特定の問題に対する答えを見つけるように求められる形式であることが多いことに注目すべきです。しかし、正式な数学的記述は命題の形式であり、問​​題の形ではありません。

質問を命題に変換するために、研究者は質問の後に「最終回答」を付け加えました。

自動形式化に使用されるプロンプト形式は次のとおりです。

AIは人間の数学者と競争するのでしょうか?

これは興味深い展開だが、ウー氏はチームの取り組みは単なる概念実証に過ぎないと述べた。 「機械を訓練して最高の人間の数学者と同等の性能を発揮させることが目標であれば、自動形式化がこの目標を達成するための重要な道筋となると思われます。」

ケンブリッジ大学チームの一員であるアルバート・ジャン氏は、成功率がさらに向上すれば、AIは人間の数学者と競争できるようになるだろうと述べた。 「 100% に到達すれば、国際数学オリンピックの金メダルを獲得する AI エージェントが必ず誕生します。 」

チームの当面の目標は、自動化された形式モデルと自動化された証明マシンを改善することですが、研究結果の将来的な影響はさらに広範囲に及ぶでしょう。ウー氏は、これらのモデルによって、現在人類が知らない数学の領域が明らかになる可能性があると述べた。

このマシンの推論機能は、より幅広い分野の検証タスクにも適しています。 「ソフトウェアが期待通りに動作するかを検証したり、ハードウェア チップを検証したりできるので、金融取引アルゴリズムとハードウェア設計の両方に応用できます。」

ロンドンの数学科学研究所のヤン・フイ・ヘ氏は、機械を使って数学を研究するのは刺激的な進歩だが、本当の課題は、そのモデルを数学研究に使うことだと語る。数学研究のほとんどはLaTeXで書かれている。 「LaTex を使用するのは、入力が簡単だからです。LaTex はある意味で自然言語であり、独自のルールがあります。」

同氏は、ユーザーは LaTeX で独自の関数や記号を定義できるが、それらは数学の論文でしか使用できない可能性があるため、プレーンテキストのみでトレーニングされたニューラル ネットワークにとっては扱いにくい可能性があると述べた。