「ＡＩが数学の未解決問題を解いた」報告ラッシュ、リーマン予想もいずれ… 高まる思考力、疲れ知らずの働き者。人間に残された仕事は？
２０２６年が明けてすぐに「人工知能（ＡＩ）が未解決の数学の定理を証明した」とする論文の公表が世界で相次いだ。近年のＡＩの進化はめざましく、数学者が長年答えを出せなかった問題が次々と解かれている。専門家は「２０２６年はＡＩが安定して数学の未解決問題を解けるようになった最初の年といえる」と話す。
この勢いで超難問とされるリーマン予想も攻略してしまうのか？ ＡＩによる数学の可能性を探った。（共同通信＝浅見英一）
▽世界的数学者が「ＡＩが自律的に証明した」と宣言
１月、米カリフォルニア大のフィールズ賞数学者、テレンス・タオ氏が自身のＳＮＳで、約５０年も未解決だった「エルデシュ問題７２８番」という数学の予想について「ＡＩが自律的に解決した」と宣言した。
エルデシュ問題は、２０世紀ハンガリーの大数学者ポール・エルデシュが生涯に残した問題の数々を指し、千近くある。７２８番はその一つで、（ａ＋ｂ－ｎ）の階乗とｎの階乗をかけたものが、ａの階乗とｂの階乗をかけたもので割り切れるとき、この（ａ＋ｂ－ｎ）の値はｎと比較して、どれぐらいの大きさになるのか、という問題だ。答えは「ｎと比べると圧倒的に小さい」だった。
既に解答が分かっている問題の答えを再現したのではなく、誰も知らなかった答えをＡＩが出したことに、タオ氏は「本物の能力向上を示した。ＡＩツールの（数学への）応用はマイルストーンを達成した」と興奮が伝わってくるような書き込みをした。
数日後には米国の別の研究者が、同じエルデシュの別の問題「３９７番」が「チャットＧＰＴプロ５・２で作成した証明」によって解決したと発表。証明にかかった時間がわずか１５分だったこともあり、話題は沸騰した。
この後も「新しいベルマン方程式の解をＧｒｏｋで見つけた」、「エルデシュの７２９、４０１番も解けた」、「ガロア理論の複雑な計算をＡＩが数学者のような推論をして解いた」など続々と報告された。
ジェミニを使って代数幾何学の新しい定理を証明したという論文の共著者の１人、ラビ・バキル米スタンフォード大教授は「自分が思いついていたら誇りに思うような洞察」で証明がなされたとのコメントを公表した。
▽「思考の連鎖」ができるようになり、ＡＩの進化が深まる
ＡＩは既に数学者の能力を超えているのだろうか？ １５０年以上解かれず、解いたら１億円の懸賞問題リーマン予想も解かれるのか？ それを探るため、ＡＩのこれまでの歩みと現状についてまとめた。
コンピューターに何かをしてもらおうと働きかけるには、かつてはプログラミング言語に“翻訳”して命令する必要があった。それが２０２２年、チャットＧＰＴの登場により、私たちが日常会話で使う「自然言語」でＡＩと対話できるようになった。
これで「ＡＩに相談すること」が、かなり一般に普及した。ただ、この時点ではＡＩに何か尋ねても、ＡＩは膨大に記憶しているデータの在庫から、回答として最も正解に近いものを差し出すだけ。何かを深く考えるというより、聞かれたことに決まった答えを反射的に返すイメージだった。
２０２４年、ＡＩに推論をさせる「思考の連鎖（ＣｏＴ）」技術を搭載したＯｐｅｎＡＩｏ１が登場したことで大きく進歩した。機械学習の研究者である園田翔さん（理化学研究所／サイバーエージェント）によると、まるで人間のように段階を追って考え、考えた中身を覚えておいて、後に思い出しながら精度の高い結論を導き出せるようになったという。「ＡＩが初めてちゃんと考えて答えられるようになった」と評する。
この技術の進展に伴って、ＡＩの能力の進化は加速する。２０２５年２月ごろには東大入試の数学、９月には数学オリンピックなどの問題が７～９割解けるようになる。１１月に大学レベルの知識が必要な問題に対処できるようになったと思えば、年末までには答えがどこにも書いていない未解決の問題まで解けるようになった。その結果が２０２６年年明けに続々披露されているというわけだ。
今の実力はどのぐらいなのか？
数々の未解決問題の解決で果たした役割について、園田さんは「優秀なポスドク（駆け出しの研究者）にアイデアを投げて、詳細を詰めてもらった感じだ」と話す。
ＡＩは、１人でやるには労力も時間もかかる作業を代わってくれる。言ってみれば面倒な仕事を、力業でゴリゴリと、スピーディーにやる人がいなかったからこそ、問題が未解決のまま残されていたとの見方もある。実力のほどが「駆け出しの若手」なら、さらに難しい未解決問題を次々解くのは、まだ先かもしれない。
▽Ｌｅａｎという重要な相棒
ところで我々が使っているＡＩはよく間違うし、よく嘘もつくと感じてはいないだろうか？ そんなＡＩによる証明は信用できるのか。
ここで登場するのが、数学の証明支援ソフト「Ｌｅａｎ（リーン）」だ。ブラジル人の科学者が作り上げ、多くの数学者も関わったというこのソフトは、ある命題（例：ＰならばＱである）に対する証明を書いて渡すと、それに誤りがないかどうかを判定してくれる。
これまで「ＡＩが解いた」としている学者たちはほぼ、ＡＩの思考過程をＬｅａｎで検証しながら間違いを回避している。
数学の証明とは、例えば「ＰならばＱ」と「ＱならばＲ」という前提から「ＰならばＲ」を導く、三段論法のような推論ステップの繰り返しだ。大きな問題なら、この命題が何百、何千と積み重なることも珍しくない。Ｌｅａｎは命題の証明の一つ一つのステップについて、正しいかどうかを判定してくれる。
ただ、このＬｅａｎの利用にはちょっとした難関がある。Ｌｅａｎ語ともいえる特殊な機械言語しか理解しないのだ。そのような仕様になっている理由の一つは、数学の命題を話し言葉で表現しようとすると、どうしてもあいまいな部分が生じてしまうため、数学者が理解している命題の内容を、厳密な、その他の意味に取られることはあり得ないＬｅａｎ語で表現する作業が必要になる。自然言語からＬｅａｎ語への翻訳、これを数学の世界では「形式化」と呼んでいる。
大事なのは、最終的に示したい命題の前提と結論を正しく翻訳すること。これができていれば、途中で間違う心配はまずないという。
逆に命題の翻訳が間違っていると、本来の問題とは違うものを証明してしまったり、証明の完成に至らないことになる。イメージで言うなら、最初の作業は広い海の上で、出発しようとしている孤島の位置と到着する孤島の位置を正しく示すこと。証明作業は小さなボートを並べて舟橋にし、その上を通って目的地を目指すようなものだ。
このポイントを指し示す作業は実は簡単ではない。命題の数学的な中身を厳密、正確に理解していることと、それを着実に翻訳できるＬｅａｎ語の知識が必要になるという。園田さんは「数学とＬｅａｎの両方を兼ね備えた研究者は、まだ少ないのが現状だ」と話す。
ちなみにリーマン予想でいうなら、前提の部分は「ｓがリーマン・ゼータ関数ζ（ｓ）の非自明な零点であるならば」で結論は「ｓの実部は１／２である」だ。
この命題の意味を正確に理解していないと翻訳は難しい。翻訳が間違っていれば何か別の命題を証明してしまうかもしれないし、そもそも結論に行き着かないことも考えられる。完全にＡＩ任せにはできそうにない作業だ。
▽ピラミッドの頂点は頂点だけでは存在できない
世界中の数学者やコンピューター科学者からなる「Ｌｅａｎコミュニティ」が管理・運営する「Ｍａｔｈｌｉｂ（マスリブ）」という数学のコンピューター上の保管庫がある。ここには数学の広範囲な知識や概念が形式化されて書き込まれているが、実は既にリーマン予想が形式化されたものも記述されている。この形式化に間違いがないとしたら、もはや解決は目前なのだろうか？
園田さんは「近いうちに解けるかも知れない」と期待を示す一方で、平たんな一本道でないとも話す。「おそらくリーマン予想という大きな命題の証明の前に必要となる、部品となるような小さな問題の数が膨大になる」と指摘する。
予想の証明を巨大なピラミッドの頂点の石に例えると、小さな問題とはそのほかの石の切り出しや成形、積み上げなどの作業だ。必要な部品を見つけ、証明していく作業が非常に多くなると、ＡＩといえども時間がかかる可能性はある。
タオ氏は米国のインターネットラジオのインタビューで「四色定理のように、ＡＩが人間には到底不可能な規模の計算力を駆使し、力任せに証明した例がある」としつつ、リーマン予想を含めた全ての未解決問題がこの延長線上で解決されるわけではないと指摘する。
四色問題とは「地図を国ごとに色づけすることを考えた場合、境界線を共有する国同士は異なる色に塗るには四色で十分だ」という定理だ。約２０００パターンをコンピューターで網羅的に調査することで解決した。
リーマン予想については「まったく新しいタイプの数学が創り出されるか、あるいは、これまで互いに無関係だった二つの数学分野の間に新しい結びつきが見い出されなければ、解決には至らないだろうとほぼ確信している」と話す。
このため「非常に賢い人たちが、極めて強力なＡＩツールの助けを借りて解くことになるのではないか」と展望を語っている。
▽数学という営みに終わりはない
現在の方法でＡＩを走らせ続ければ、リーマン予想を取り巻く理論は進展するだろう。その先はどうなるのか。
園田さんは建築を例に挙げる。コンピューター利用設計システム（ＣＡＤ）が普及したことで、設計は構造計算や設備の取り回しなどが容易になってコストも下がり、建築士はデザインなど高付加価値の仕事に注力できるようになった。今まで手作業や、大人数でやっていた仕事が１人で簡単にできるようになる。
近ごろ米国の企業Ｍａｔｈ，Ｉｎｃ．が、２０２２年にフィールズ賞が授与された「８次元および２４次元空間における球充填問題」の証明について、ガウスというＡＩが問題の形式化と証明の確認を行ったと発表した。ただし、その証明記述は１８万行を超え、人が全てを読める量ではないことが話題になっている。全体像を人が把握できないことをどう考えるかは今後の課題の一つだ。
ＡＩは人間に置き換わるのだろうか。タオ氏は３月末にインターネットに公開した論文で「人間の役割は消えない」と指摘する。
形式的、反復的な作業ではＡＩは人間を大きく上回るとしながらも、ＡＩが生成した証明が「直感的に理解可能か」「数学的な意味があるのか」といった点は、人間の判断と価値観に依存する。そういう意味で「知的労働の分業化が進む」とした。
さらに、この変化によって「教育や研究、評価制度を見直す必要が生じるだろう」と予測した。
園田さんは「数学という営みはなくならないだろう」と指摘。「できることは増えており、何を作っていくかが大事になる。大航海時代が始まったときの、世界の果てに思いをはせる人の気分だ」と語った。
0 件のコメント:
コメントを投稿