OpenAIは今週、高度な問題に取り組む自社モデルの能力を示そうとして、難しい数学の問題に対する数百件の解答とされるものを公表した。しかし、この公開は数学研究者で構成される諮問グループが策定した指針に完全には従っておらず、根本的な問いを再び浮上させた。モデルがプログラムとして形式化可能な解答を生成すれば十分なのか、それとも数学者が理解し、検証できるものでなければならないのか、という問いである。
Advisory Group on Mathematics and Artificial Intelligence (AGMAI)は9人の著名な研究者で構成され、プリンストン大学高等研究所が受け入れている。同グループは9月末、数学の問題を解く高度なモデルを開発する研究所向けの指針を公表していた。
研究者の指針への部分的な遵守
AGMAIは、自らの勧告がどの程度遵守されているかの評価は、最終的には数学界に委ねられると指摘した。同グループの主要な勧告の一つは、高度な数学の問題を商用の独占モデルでテストすることをやめることだった。一方、OpenAIは、自社モデルの評価に公開された研究問題を使用していることを明確にした。
OpenAIはいくつかの原則には従った。例えば、成果を迅速に公表し、モデルがどのように結論に到達したかに関する情報を提供した。しかし、719件中、モデルの思考連鎖を含んでいた原稿はわずか10件だった。また、公表された証明の42％は形式化されていなかった。
同グループは、人間が理解するのが難しい証明は形式的な形に変換すべきだと考えている。しかし同時に、成果の公開に先立って人間による理解が伴うことを保証する責任は研究所にあると強調し、これらの成果を実際に科学的な意味を持つものにするため、数学者への資金提供を提案した。
自然言語とLeanコードの間の隔たり
モデルは通常、まず自然言語による説明を作成し、次にそれをLeanへ変換しようとする。Leanは、コンパイラーによって証明の整合性を実行可能な形式で確認できるプログラミング言語である。しかし、自動変換によって証明の内容が変わったり、説明が述べていることとコードが証明していることとの間に隔たりが生じたりする可能性がある。
ケンブリッジ大学とキングス・カレッジ・ロンドンの数学者が発表した論文は、OpenAIが複雑な流体の挙動に関するNavier-Stokes方程式から派生した問題への解答として提示したものについて、自然言語による証明と、それに関連するLeanコードの間に少なくとも2つの相違点があることを記録した。これらの相違は、必ずしもどちらかの解答が誤っていることを証明するものではないが、人間の介入なしにモデルに解答の形式化を任せることへの疑念を生じさせる。
またAGMAIは、本文による証明と正式版を結び付ける、機械可読なメタデータを含めるよう求めていたが、OpenAIは今回の公開でそれを提供しなかった。「lost in translation」として知られるこの論文の著者らは、自然言語による証明と自動変換されたLeanの証明は、他の証明が受けるものと同等の査読と精査なしには、原則として受け入れるべきではないと結論づけた。
なぜこのニュースが重要なのか
問題は、コードが正常にコンパイルされることを示すことだけではなく、そのコードが実際に本文で説明されている数学的な考えを表していることを示すことにある。従来の研究では、科学者が自らの成果に責任を負い、論文、講義、セミナーを通じてそれを議論する。この過程は、誤りを発見し、再利用可能な手法を理解する助けとなる。
一方、モデルが難しい問題への解答を生成する場合、公開時点でこのような人間による理解が得られていない可能性がある。そのため、現在のOpenAIの成果は、問題の終着点というより科学的検証のプロセスの出発点に近いように見える。数学界でこれらの証明を採用する前に、人間によるレビューと、本文による出力と正式な出力を結び付けることが、依然として未解決の条件となっている。