ニュース
OpenAI、数学論文722本を公開 形式証明なしの成果も混在
AI企業が数学の未解決問題を解いたと発表するたび、どこまで信じてよいか迷う読者も多いはずです。今回の公開は、その判断材料となる形式証明の有無や第三者機関の見解を含んでおり、企業がAIの性能主張を扱う際の目安になります。
何が起きたか
米OpenAIは10月6日（現地時間）、社内のフロンティアモデルが生み出した数学の新たな成果をまとめて公開したと発表しました。論文の原稿や証明支援系「Lean」による形式証明は、GitHubのリポジトリに置かれています。[1]
リポジトリに収録された原稿は722本で、372件の成果群にまとめられました。独立組織「Advisory Group on Mathematics and Artificial Intelligence」（AGMAI）によれば、この中には数百件の未解決問題への解答が含まれるといいます。[2]
OpenAIの説明では、多くの原稿にLeanによる形式証明が付いていますが、すべてに付いているわけではないとのことです。形式化していない結果には誤りが含まれる余地があるとし、見つかり次第修正する方針です。評価期間中にモデルへ与えた問題はおよそ4000問に上り、1件当たりの計算量は平均で「ChatGPT Pro」の思考機能を約3時間使った分に相当するといいます。[1]
背景・解説
Leanとは、数学の証明を機械的に検証できる形式で書くための証明支援系です。形式証明が付いていれば、論理展開に誤りがないかをコンピューターがそのまま確認できます。一方、形式化されていない原稿は、モデルが書いた文章としての体裁が整っているに過ぎず、専門家による個別の検証が欠かせません。[1]
OpenAIは9月、社内モデルがミレニアム懸賞問題の1つ「ナビエ・ストークス方程式」を解決したと発表し、先行研究を進めていた数学者から経緯を問題視され、論争になりました。その後、同社はAGMAIとの連携を公表し、社内モデルが100件以上の未解決問題を解決したと説明しています。AGMAIは9月29日の提言で、モデル名やプロンプト、推論の要約、計算コストの開示、Leanによる形式化などを求める一方、社内モデルを外部の研究者が使えない形で試す慣行自体への支持は明確に否定しました。[1]
仕事や業務への影響 — AI Topicaの見方
数学の未解決問題をAIが解いたという発表を、社内で鵜呑みにしない姿勢が大切です。形式証明が付いていない原稿は、専門家の査読を経るまで「候補」の段階にとどまります。例えば、従業員50人のシステム開発会社で技術広報を担当する1人が、この発表を自社のAI活用事例として紹介するなら、Leanによる形式証明の有無を1件ずつ確認してから引用すべきです。
今回の722本のうち形式証明が付いていない原稿も混在しており、OpenAI自身が誤りの余地を認めています。経営層がAIの数学的能力を自社の技術選定や投資判断の材料にするなら、数学界による査読の進展を数カ月単位で待つ姿勢で十分です。急いで結論を出すことは不要です。
AGMAIという数学者による外部組織が独自の提言を出し、企業の発表姿勢そのものをけん制している点も実務の参考になります。AI企業の発表を鵜呑みにせず、第三者の評価機関が存在するかどうかを確かめる習慣は、数学分野に限らずAIの性能主張全般に当てはめるべきです。例えば、情報システム部門が30人規模の企業でAIベンダーの性能比較表を作る担当者なら、ベンダー発表の数値だけでなく独立した評価機関のコメントの有無を比較項目に加えることが実務で役立ちます。
不確かな点・注意
今回の成果がどこまで数学界に認められるかは、まだ定まっていません。AGMAIは、助言をしたことと成果の影響を判断することは別だと強調し、評価を担えるのは数学界だけだとしています。[1]
形式化されていない原稿にどの程度の誤りが含まれるかも明らかではありません。OpenAIは問題が見つかり次第修正するとしていますが、具体的な検証の時期や方法は示されていません。リーマンゼータ関数に関する成果の一部は人間が文章を手直ししており、ほかの原稿とどこまで同じ基準で作られたのかという点は未確認です。[1]