OpenAIが、難しい数学の問題に対するAIの解答原稿719本をGitHubに公開しました。事前に一流の数学者による助言グループへ相談したと説明しています。ところがTechCrunchの報道によると、その助言グループ自身が9月末に示した指針と照らすと、満たしていない点が目立ちます。Terence Tao氏ら数学者からも、疑問の声が上がっています。
背景と文脈
AIが数学の未解決問題に挑む動きは、ここ1年で加速しました。一方で、以前のモデルが長年の難問を解いたとされた際には、証明の確かさや公表の仕方をめぐって論争が起きました。OpenAIは今回、その反省から数学界との調整を図ったと述べています。
相談先はAGMAI（Advisory Group on Mathematics and Artificial Intelligence）です。プリンストン高等研究所が拠点を置く9人の助言グループで、9月末に、AI企業が数学の問題を解く際の指針を公表しました。最初の勧告は、高度な問題を非公開（プロプライエタリ）のモデルで試すのをやめることでした。指針をどれだけ守ったかは数学界が判断するとも述べています。
この勧告は、OpenAIが自社の非公開モデルで未解決問題を評価している立場と、そもそもぶつかります。報道では、OpenAIから批判への直接の回答は確認されていません。
技術/ビジネス面
指針と今回の公開を突き合わせると、満たした点と満たさなかった点が分かれます。満たしたのは、結果を素早く公開したことと、モデルが結論に至った経緯の情報を一部添えたことです。
満たさなかった点は複数あります。まず、モデルの思考の連鎖（chain-of-thought、答えに至るまでの推論の文章）を付けた原稿は、719本のうち10本だけでした。次に形式化です。形式化とは、証明をLean（証明を機械で検証できるプログラミング言語型の道具）のコードに書き直し、正しさを自動で確かめられるようにすることで、人間が追いにくい証明には指針が勧めています。OpenAIの証明で形式化済みなのは42%でした。
さらに、自然言語の証明と形式化したコードを結ぶ機械可読のメタデータ（付随情報）も提供されませんでした。結果を人間が理解する責任を企業が負い、意味づけを行う数学者への資金提供も検討すべきだとの提案についても、実施の有無は不明です。
数学者からの批判も具体的です。Terence Tao氏はSNSで、AIの利用者が問題を解いて次へ進むだけで、内容を理解して講演したり分野と対話したりできていないと指摘しました。ハーバード大のMelanie Wood教授は、公開時点では人間の理解が伴わず、本当の仕事はそこから始まると述べています。
ケンブリッジ大とキングス・カレッジ・ロンドンの数学者らは論文で、100万ドルの懸賞が付くミレニアム問題の1つ、ナビエ・ストークス方程式に関するOpenAIの解答を検討しました。自然言語の証明とLeanコードの間に、少なくとも2か所の食い違いを見つけています。著者らは、これが解答の誤りを直ちに意味しないとしつつ、モデルが作った証明と形式化は通常の査読なしに信頼すべきでないと結論づけました。
これからどうなるか
AIが出した証明の価値は、正しさに加えて、人間が理解し検証できるかで決まります。今回の議論は、そうした共通認識が数学界で固まりつつあることを示しています。AI企業は、量を競う公開から、検証可能性を備えた公開へ移る圧力を受けるでしょう。
開発者にも他人事ではありません。AIが生成したコードやドキュメントを、レビューなしに本番へ入れる運用と、構図は同じです。形式化が証明の自動検証にあたるなら、コードではテストや型検査が対応します。生成物を機械で確かめる仕組みを先に整えておく発想が、ここから学べます。
今後の注目点は、OpenAIが形式化率を上げるか、思考過程の公開を広げるかです。AGMAIが数学界の判断として何を示すのかも、重要な指標になります。
まとめ
OpenAIは719本の数学解答を公開しましたが、思考過程の添付は10本、形式化は42%にとどまり、数学者団体の指針を一部しか満たしていません。AIの成果を検証する仕組みと、人間の理解を伴わせる責任が問われています。生成物を機械で検証する発想は、コード生成の現場にも通じます。
参考リンク
アイキャッチ画像: Photo by Bozhin Karaivanov on Unsplash
