本記事ではLLMによる定理証明における重要な進展を紹介します。

定理証明は、LLMの推論能力を客観的に評価できる重要な指標としても注目されていますが、学習データの不足が大きな課題となっています。スタンフォード大学の研究チームは、人間の学習プロセスからヒントを得て、予想生成と証明を組み合わせた新しい学習手法を開発しました。

背景

定理証明の世界に、新たな風が吹き始めています。LLMを用いた形式的定理証明に、研究者たちの注目が集まっているのです。

定理証明の中でも、コンピュータが証明の正しさを厳密に検証できる形式で書かれた証明のことを形式的定理証明と言います。これが、LLMの推論能力を客観的に評価できる重要な指標としても注目されています。

人間がLLMと力を合わせて新たな定理証明を効率的にできるようになれば、さまざまな分野でその恩恵を得る可能性があります。

しかし、形式的定理証明の学習に使えるデータを集めることは、極めて困難な課題となっています。なぜなら、定理や証明は専門家によって作成される必要があり、他の機械学習のデータソースと比べて、利用可能な量が何桁も少ないからです。

これまでの研究では強化学習や専門家反復（expert iteration）と呼ばれる手法が試されてきました。LLMに証明を生成させ、正しい証明が得られた場合にそれを用いて再学習を行うというアプローチです。
しかしこの方法では未証明の定理に対して正しい証明を生成するために必要なサンプル数が指数関数的に増加してしまうため、性能はすぐに限界に達してしまいます。
さらに、強化学習には「訓練データの質による制約」も存在します。たとえば、高校レベルの問題だけで訓練されたモデルが、大学レベルの証明技術を習得することは原理的に困難とされています。つまり、オープンな数学の問題に対して、既存の強化学習手法では十分な訓練データを得ることができないのです。

そこで今回スタンフォード大学の研究者たちは、人間の数学者の学習プロセスに着目しました。数学者は既存の定理を変形したり、拡張したり、組み合わせたりすることで理解を深め、証明スキルを磨いています。また、新しい予想を提案し公表することも、証明と同様に重要な活動とされています。

このような洞察に基づき、研究チームは予想生成と証明を組み合わせた新しい学習手法の開発に着手したのです。

以下で詳しく紹介します。