7月14日、Scientific Americanが「ChatGPT just proved another 50-year-old math conjecture」と題した記事を公開した。OpenAIの新モデル(元記事では"ChatGPT"と表記)が50年以上未解決だった数学の予想を証明したというものだ。注目すべきは証明の内容だけでなく、そのプロセスを制御したプロンプト設計にある。
成功を引き出したプロンプト設計
今回の成果で最も示唆に富むのは、証明に使われたプロンプトの中身だ。OpenAIはその詳細を公開しており、エンジニア的な視点から興味深い工夫が随所に施されている。
MITの数学者Andrew Sutherland氏はこう指摘する。「プロンプトの大部分は、LLMに問題解決に必要な努力を実際にさせるためのスキャフォールディング(足場)だ」。具体的には以下の工夫が施された。
- 最大64のエージェントを並列で動作させ、それぞれがタスクを分担
- 複数AIが互いに通信しながら作業することで、誤った証明や幻覚的な参照文献を抑制
- 「この問題は未解決だから解けない」とモデルが逃げないよう、そのような姿勢を取らないよう明示的に指示
- そして最も特徴的な一文:「諦めることを考える前に、最低8時間はこの問題に取り組め」
多くの数学者が経験則として語るように、LLMは新しい証明を見つける代わりに「人間の失敗例」を指摘して逃げようとする傾向がある。有効なアプローチは、称賛と厳しい指示を組み合わせた「教師的な接し方」のようだ。
「サイクル二重被覆予想」とは何か
OpenAIは今回の公開に合わせて「**サイクル二重被覆予想(cycle double cover conjecture)**」の証明を発表した。この予想は1970年代にPaul Seymour氏とGunnar Szekeres氏が独立に提唱したもので、以来半世紀にわたり未解決のままだった。未解決グラフ理論問題の一覧にも長く名を連ねてきた問題だ。
予想の内容を簡単に説明する。**グラフ**とは、頂点(ドット)と辺(線)で構成される数学的な構造だ。インターネットなどの実世界のネットワーク解析にも応用される。グラフ内の「サイクル」とは、出発点に戻ってくるループのことで、「サイクル二重被覆」とはグラフ内のすべての辺をちょうど2回カバーするループの集合を指す。
今回の証明は、対象となるグラフが最大8つのループで二重被覆できることを示した(技術的な理由から、単一の辺でのみ接続された大きな部分を持つグラフは対象外)。
プリンストン大学の数学者Noga Alon氏はこの成果を「長年にわたり多くの注目を集めた有名な予想で、驚くことに証明は短い」と評し、「AIツールが数学研究をすでに大きく変えつつあることを示す印象的な事例だ」とコメントしている。
新しいアイデアではなく、組み合わせで突破
この証明が持つ重要な含意は、モデルが人間の思いつかなかった全く新しい手法で問題を解いたわけではない点だ。証明は人間がこれまで試みてきた手法を組み合わせ、そこから少し多くを引き出すことで成立した。
Sutherland氏はこう指摘する。「ある問題が『難しい』という評判を持つと、専門家も学生もそこに時間を使わなくなる。難しさの認識が自己成就的予言になってしまう。LLMが『簡単な』解を持つ『難しい』問題を次々と発見するケースが、今後も続くと予想している。」
数学をAIのベンチマークとして使う動き
OpenAIをはじめとするAI企業が純粋数学に重点投資しているのは、モデルの推論能力を測るベンチマークとして機能するからだ。コーディングやチェスとは異なり、数学の証明は正誤が明確で、かつ自動検証も可能という特性がある。
昨年には80年前のErdős問題をAIが解いた事例もあり、今回の成果はその延長線上にある。「難問」として棚上げにされてきた問題が、実は手の届く範囲にあったケースをAIが掘り起こし続けている構図だ。
詳細はChatGPT just proved another 50-year-old math conjectureを参照していただきたい。