- 数学の証明がより厳密に形式化されるにつれ、Leanのようなツールが人間の証明を検証し、大規模協業の信頼基盤を変えつつある
- mathlibのような標準ライブラリが蓄積され、学部レベルの定理から新しい分野まで形式化する参入障壁が下がりつつある
- PFR予想の形式化では20人を超える参加者が小さな証明ステップを分担し、テレンス・タオは行ごとの確認よりも全体の方向管理に集中した
- AIは当面、数学を「解く」よりも証明コパイロットとして形式化・検証・反復作業を支援する役割に近い
- 数学研究は、人間による方向設定、詳細な形式化、AI訓練、AIの証明の解釈のように、より明示的で分業化された作業へ変わる可能性がある
形式化が変える数学の協業
- 従来の数学研究は少人数での協業に近く、タオは通常、5人程度が協業規模の上限に近いと見ている
- 自動証明チェッカー(proof checker)があれば、互いを知らない何百人とでも協業できる
- Polynomial Freiman-Ruzsa(PFR)予想の最近の結果を形式化した際には、20人以上が参加した
- 証明を多数の小さな段階に分割した
- 各参加者が1つの段階の証明を担当した
- タオはすべての貢献を行単位で確認するのではなく、全体の進行方向を管理した
すべての数学者がプログラマーである必要はない
- 形式化プロジェクトでは役割分担が可能である
- ある人は数学的な方向性に集中する
- ある人は小さな数学的断片を形式証明へ変換する作業を専門的に担う
- Peter Scholzeのようにコンピュータに不慣れな数学者でもLeanプロジェクトに参加できる
- 大きな数学課題を小さな断片に分ければ、理論全体を理解していなくても特定のサブタスクに貢献できる
Lean、mathlib、検索が生んだ実用性
- 形式数学が実用化された大きな理由の1つは、標準数学ライブラリの発展である
- Leanにはmathlibという大規模プロジェクトがある
- 微積分や位相幾何学のような学部数学の基本定理が1つずつライブラリに入っている
- 目標はライブラリを大学院レベルまで引き上げることだ
- そうなれば、新しい数学分野を形式化しやすくなる
- 証明を作るには既に真と確認された定理を探す必要があるため、より賢い検索エンジンも重要になる
- PFRプロジェクト全体を形式化した後の検証コンパイルには約30分しかかからない
- ボトルネックは計算資源よりも、使い勝手、ユーザーフレンドリーさ、人々がツールに適応することにある
- Leanは現在、最も活発なコミュニティを持つ形式言語と評価されている
- 単著プロジェクトでは他の言語のほうが適している場合もある
- Leanは学びやすく、ライブラリとコミュニティが充実している
- 将来的に別の選択肢へ置き換わる可能性はあるが、現時点では支配的な形式言語である
依然として高い形式化コスト
- タオは、あるプロジェクトを形式化することはできても、現状では自分の時間を1か月使う必要があるかもしれないと見ている
- すべての結果を日常的に形式化する段階にはまだ至っていない
- Leanを学ぶ助けになる場合
- 結果の正確性への関心が大きい場合
- 形式化が実際の価値をもたらすプロジェクトを選ぶ必要がある
- 技術が進歩すれば形式化コストは下がる可能性がある
- 今は従来方式より10倍長くかかることがありうる
- 将来的には2倍程度、さらに1倍未満まで下がる可能性がある
AIは数学者のコパイロットになりうる
- タオは将来、数学者が証明を直接タイプするのではなく、GPTのようなシステムに説明し、AIが進行中にLean形式化を試みる形を想像している
- 検証が通れば、LaTeX論文とLean証明を一緒に提供できる
- ユーザーが望めば、ジャーナル投稿まで支援する助手になりうる
- 現在、最も速い形式化の経路は依然として、人間が先に証明のアイデアと草案を作ることだ
- 長期的には、人間が証明全体を知らない状態で小さな断片を形式化し、AIと人間が一緒につないで大きな定理を証明するプロジェクトも可能かもしれない
- タオは、この方式が可能になるには数年かかると見ている
- 現在の技術はまだ不十分で、形式化も依然として苦痛を伴う作業である
「数学が解決される」という見通しとの距離
- Tony WuとChristian Szegedyは、2〜3年以内に機械が人間よりもうまく証明を見つけるという意味で、数学が「解決」されるだろうと述べたことがある
- タオは、3年以内にAIが数学者にとって有用になり、明確な進展がある可能性は認めつつも、数学が解決されるとは見ていない
- AIは、証明のある段階が真らしいが人間にはすぐ見抜けないときに助けを求めるコパイロットになりうる
- AIが現在の人間レベルの数学を遂行できても、人間の数学者はさらに高いレベルの数学へ移ることができる
- AIによって一度に何百、何千もの定理を証明する方式も可能になりうる
- 人間の数学者はAIが何をするかを指揮する役割を担う
- タオは、この変化のタイムラインを2〜3年と見る見方はやや攻めすぎだと考えている
証明理解とAI生成証明
- 数学の証明は単に真偽を確認する手続きではなく、なぜ真なのかを理解する過程でもある
- 近い将来には、AIが退屈で些末な作業を先に自動化し、人間が依然として方向づけを担う可能性が高い
- AIが理解しにくく見栄えの悪い証明を出してきた場合でも、人間はその証明を再分析できる
- たとえば、10個の仮定から結論を導く証明で、仮定を1つ外しても成り立つかを確かめられる
- AI生成証明から洞察を抽出する新しいタイプの数学者が生まれる可能性がある
- 初期のAI証明には洞察がないように見えるかもしれない
- 人々はその証明をより理解しやすくし、構造を見いだせる
未解決問題とAIの限界
- 未解決予想を証明するには、まずより小さな断片へ分解する必要がある
- 問題をより易しい問題に変えるよりも、より難しい問題に変えるほうがはるかに簡単である
- タオは、AIがこの分解作業で人間より優れていることをまだ示していないと見ている
- AIが複数分野のあいだの接続可能性を提案する用途は興味深い
- 現在の成功率は低い
- 10件の提案のうち1件だけが興味深く、9件は役に立たないかもしれない
- タオは将来、この点は変わりうると見ている
数学知識のデータ問題
- 数学AIの訓練における問題の1つは、十分なデータがないことだ
- オンライン論文は訓練に使えるが、多くの数学的直観は論文に含まれていない
- 数学者同士の会話
- 講義
- 学生を指導するやり方
- 失敗した試みと修正の過程
- 出版された証明は圧縮された成果物であり、人々は成功事例だけを出版する傾向がある
- 本当に貴重なデータは、何かを試したがうまくいかず、どう修正したかを含む過程である
- 将来は研究の試行と失敗の過程が記録され、AI訓練や他の研究者の重複した失敗の防止に使われるかもしれない
- タオは、2040年の高度なAI Leanのようなシステムを使うために研究過程の記録に同意する状況を例に挙げている
より明示的な数学への変化
- 多くの数学知識は個々の数学者の頭の中に閉じ込められており、ごく一部だけが明示的に残される
- 形式化が進むほど、暗黙知がより多く明示知へと変わっていく
- 形式化された教科書は対話型教科書へつながる可能性がある
- 高レベルの証明説明から始める
- 理解できない段階はより詳しく展開できる
- 望めば公理レベルまで下りられる
- この方式により、ある分野の数学者が別の分野に貢献しやすくなる可能性がある
- 大きな課題のサブタスクを正確に指定できる
- 全体を理解していなくても必要な断片に参加できる
1件のコメント
Hacker Newsのコメント
https://archive.is/Idouw
project manager mathematicians という表現で、Edsger Dijkstraが1975年に書いた風刺文 “A letter to my old friend Jonathan” [1] と、その続編 [2] を思い出した。
ソフトウェアの作り方を数学に適用したらどれほど滑稽になるかを示して批判した文章だったが、ある意味では先見の明があった。
その要点は、知的財産権、とりわけ 数学的真理 に知的財産権を適用する不条理を批判することにあり、幸い今の機械化の流れでは、その点は大きな懸念ではなさそうだ。
[1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
[2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...
洞察に富んだ記事だが、抜けているのは、LLMがますます 超人的な形で抽象化 するようになるという点だと思う。
Taoは「問題をより難しく変えるのは簡単だが、より単純に変えるのは難しいし、AIがこの点で人間より優れていることを示したことはない」と述べているが、LLMの仕組み上、はるかに高いレベルの洞察が可能になり得る。
今は助手、ファクトチェッカー、退屈な作業の処理係に近いが、まもなく洞察を提案する存在になるだろう。すでにLLMは埋め込みと知識を圧縮しており、私たちには見えていない洞察を持っている。
Hintonが核爆弾と堆肥の山の関連性を例に出す場面: https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s
人間の書き方をまねるよう訓練された機械にすぎず、人間より賢い何かをまねるのに必要な訓練データがない。
機械学習が人間の知能を超えることに疑いはないが、ボトルネックは、世界中の文章全体に回帰する代わりに、人間の介入なしで自分の出力から自分で学習させる方法を見つけることだ。
Ramanujanは正規教育もなく、数冊の数学書に触れただけで輝かしい数学的発見をしたが、機械学習モデルの訓練データという観点では、ほとんど何もない量に等しい。
言葉にまとめるのに10秒ほどかかったが、必要な情報を知っていれば答えは明白だった。
Hintonはこれが類推的思考を示していると言うが、園芸関連の記事や堆肥の山の物理に関する話はオンラインに多く、ChatGPTが訓練中にすでに見ていた可能性が高い。
だからこの例は、LLMが訓練テキスト中で実質的に答えをすでに見ていた場合をコントロールできていない事例のように見える。
動画の後半でIlyaが「存在証明はある。人間の脳がニューラルネットワークだ」と言う部分（https://youtu.be/Gg-w_n9NJIE?t=4966）も興味深い。人間の脳もニューラルネットワークだという立場にはおおむね同意するが、実際のニューロンは8ビットで動作しているわけではなく、細胞の種類・DNA・ホルモンの化学的環境なども異なるという反論も多く、哲学的な分岐点があると思う。
数分から数時間で可能だ。
一方、人間の専門家をもう1人得るには、数学を職業として好きな人が現れ、数十年の教育と高度な専門化を経る必要があり、その人が最後までやり遂げて知識の最前線を押し広げられるレベルになる保証もない。
その時間を待っている間に、並列に動作するAI専門家を何兆個も作ることもできる。
人間の脳が新しい情報を吸収する帯域幅は低いが、機械は生涯分の知識を数秒で複製し、数千の会話を並列に行い、脳の一部をシリアライズして別のAIに送ることもできる。プログラマブル物質にまで到達すれば、computroniumを指数関数的に作り出し、数千年分の研究を数秒で行うようなオメガポイントも可能になる。
数学のことはまったく分からないが、ソフトウェアの歴史を思い起こさせる。昔は RollerCoaster Tycoon のような驚くべきプロジェクトが、ほぼ一人の手による作品だった。
その後、ソフトウェア工学はインタビューで描かれているのと似た形でモジュール化され、今では私のような人間が生業として React を量産する巨大な組み立てラインになり、一人当たりの生産性や求められる能力はほとんどゼロに近くなったように思える。
分野が全盛期にあるときは、一人の天才が頭の中に百のことを抱えて最高の仕事を成し遂げるが、それが組み立てラインに置き換わると、その分野は本当に価値あるものをもはや作れなくなる、という印象を受ける。
ソフトウェア工学は素晴らしいことをやめてはいないし、むしろ正反対だと思う。
冗談はさておき、いつか致命的なバグを直さなければならない時が来れば、実力は表に出る。製品やサービスが安定し収益性を持つようになったからといって、元の開発者たちが去ったとか、誰かが大仕事を成し遂げられないという意味ではない。
この分野が本当に価値あるものをもはや作っていない、というのは大きな間違いだ。
100人が100年かけて作った大聖堂と、一人が1か月で作った小屋を比べるようなものだ。小屋も立っているし住む場所にはなるが、大聖堂ではない。
Web 開発の分野では、Python だけを見ようとしても、歯車の小さな歯一つひとつにフレームワークや技術が多すぎて、本当についていくのが難しい。
実力はおおむね対数正規分布に従うため、例外的な人はもともと少ない。初期の小さな分野では支援インフラが不足しているため、極端な才能を持つ人だけが生き残り、トップ級人材の密度が非現実的に高くなることがある。
最新フレームワーク47個を無理やりつなぎ合わせて ToDo リストアプリを量産することと、意味のある影響を生むことは根本的に別のことだ。
費用対効果の観点では、大きなことに長期投資するより、安く大量のコードを吐き出す方向に強い局所最適点があり、分野が成熟するほどその地点に到達するための能力の下限は下がっていく。
トップ級人材の育成に集中する組織も多くない。だから分野が大きくなるほど平均的な実力が放置された状態で低下する現象は説明しやすく、分布の扱いを誤ると後で修正するのに高くつく可能性がある。
コンピュータ検証された証明は、AI がかなり近い将来に有用になり得る領域だ。ただし、完全な LLM というよりは、チェスエンジンのニューラルネットワークに近いものかもしれない。
すべてを手で証明するのは退屈で時間がかかるため、すでに多くのソルバーが使われているが、タクティックやソルバーは、定理や補題をあまりに多く投げ込まれると苦しくなる。
関連する補題をパターンマッチで見つける探索機械としてのニューラルネットワークは相性が良い。
帰納法と高階単一化も実質的にはコード合成であり、可能なすべての構文木を総当たりで反復するのは非常に非効率だ。
ソルバーはいずれにせよバックトラッキングするので、AI が95%役に立たない補題を出しても問題なく、手作業で探すより劇的に良くなる可能性がある。
ただし、コンピュータ検証された証明がコミュニケーションに必ずしも良いのかは確信がない。人間が読む証明は、分量以外にもさまざまな理由で高水準であり、細部を省略しているのだ。
核心的な問題は、証明で使う数学的対象の形式的定義と結び付いていなければならない点だ。
しかし人間は証明を書いたり読んだりするとき、そのようには考えない。普通は自分が「道義的に」何をしているのかについて高水準の非形式的な感覚があり、必要に応じて形式的な細部を埋めていく。
コンピュータコードは、言語の形式意味論がメンタルモデルにずっと近いため、ある程度は機能するが、数学では一般に目標が異なる。
Isabelle の sledgehammer 戦略は、E、Z3、SPASS、Vampire のような自動定理証明器を組み合わせ、目標を証明または反証しようとする。
理論上はよさそうに見えるが、実際には任意に見える補題を12個適用した再構成証明が出てきて、こうした証明は読めず、非常に壊れやすい。
AI がこの問題を魔法のように解決するとは思えない。
現在のニューラルネットワークはサンプル効率が極めて低く、形式数学のデータセットは Python コードのようなデータセットよりはるかに小さい。
Terence Tao は数か月前にこのテーマで素晴らしい講演を行っており、Lean の活用をより詳しく扱っている: https://www.youtube.com/watch?v=AayZuuDDKP0
ある現役の数学者が、研究中にGPT-4oに、おそらく新しい補題を証明させたという
「私のパートナーは数学者なのだが、先週初めてChatGPTを使って、研究用の補題をいくつか証明してみた。すでにそれらの定理は真だろうと疑っており、アプローチもおおよそあったが、その種の命題の専門家ではなかった。モデルから正確で有用な証明を得たのは今回が初めてだった
1つ目の補題は、共同研究者が小さな e の値に関する計算で見つけたものだ。ChatGPTは、メビウス関数を使ってみるよう伝えるまでは証明を見つけられなかった
https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
2つ目はもう少し標準的に見え、Mathematicaでもできたのではないかと思う。しかしMathematicaはすっきりした導出を示してくれないので、それでも有用だ
https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579...」
こういうものは、推論や重いテーマについて恐ろしいほど良くなっている
機械学習分野が、LLMのほぼシステム1的思考を補完するシステム2能力を加えることに引き続き集中すれば、状況は荒々しいものになりそうだ
印象的な記憶力ではあるが、新しい推論ではない
私たちは |τ|! 係数を持つ分割和ではなく、順序付き分割の和として考えていたが、両者は当然同じものだ
循環的に順序付けられた分割、つまり |τ|! の代わりに (|τ|-1)! 係数を使うと、(-1)^e ではなく 0 が出る
Berenの組合せ論的証明は、特別な元を1つ選び、その元が単独でいれば次の部分と結合し、単独でなければそれだけの部分に分ける、という方法で、偶数長と奇数長の循環順序付き分割の間に全単射を作るものだ
線形順序の場合も同様に最後の元から適用するが、最後の元が最後の部分で単独である分割はマッチしないため、次の元へ再帰的に進む
結局すべてがマッチし、すべての元が別々で、元の順序どおりに並んだ分割だけが残る。元の集合の大きさの偶奇に応じて、符号付き和が元の命題につながる
「τ ≤ τ」に関する和に項がいくつあるのかも分からないし、これが3番の左辺または右辺の一方を立ててから他方を結論することとどうつながるのかも合っていない
実際には、ChatGPTが分割束のメビウス関数を思い出して証明なしに繰り返し、その後は見た目だけそれらしいでたらめを吐いただけだ
そのメビウス関数を立てることが実質的な核心であり、問いはほとんど、その関数がその形であることを証明せよというのと同じだ
しかもChatGPTが出した一般公式も少し間違っており、現在の証明で重要な |σ| = 1 の場合にだけ合っている
この事実は、メビウス関数全体の装置を明示的に使わなくても、N(t,e) を t 個の同値類に分ける分割数とし、N(t,e+1)=N(t-1,e)+tN(t,e) という漸化式で初等的な帰納法を行えばすぐに示せる
このインタビューでは3つの点が際立っている
第一に、Taoは数学的洞察も社会の他の産出物と同じように「生産」される未来を描き、project manager mathematiciansについて語っている。数学がまだそのように産業化されていない理由をツール不足に見いだし、AIと証明支援系がこの点で革命的になり得ると見ている。ただし人間の相互作用と導きは依然として必要だ
第二に、論文に含まれない暗黙知が非常に多い。直観や失敗の知識のようなものは重要で、トップ数学者たちでさえ同じ間違いを繰り返さないためには互いに話す必要がある
第三に、数学はすでに十分に形式化されていると思いがちだが、論文には共通知識が多く前提とされている。証明支援系が理解できる形で証明を形式化すれば、より多くの人が実際に何が起きているのかを理解する助けになる
TaoがPolymathプロジェクトの講演で示したように、彼は常に数学研究の新しい方法を探している人物だということが表れている
当面は、TaoやScholzeのようなフィールズ賞受賞者が証明に10倍の時間を費やす余裕があるときに可能なプロジェクトかもしれない
最近、最上位クラスの数学科のポスドクと話したが、自分の周囲で実際の作業に lean4 を使っている人はいないと言っていた
キャリア初期の研究者なら、直観を信じて論文を出すほうがおそらくよいだろう
このテーマをきちんと見るには、数人の印象だけでは不十分だ
一方、低次元トポロジーのようにより直観的なスタイルの分野では、証明検査器を使う人は少ないと予想する
ここで直観的というのは、厳密さに欠けるという意味ではない。あるホモトピー同値に関する図による証明は、不等式の列挙よりも、Leanが理解できる形に移すのがはるかに難しい
ちなみに自分は幾何／トポロジー寄りにいるが、まだこうしたツールを使っている人を見たり聞いたりしたことはない
https://lean-lang.org/
https://github.com/leanprover/lean4
「AIが理解不能で不格好な証明を提示したら、それを分析できる。その証明が10個の仮定を使って1つの結論を得ているなら、仮定を1つ削っても証明はまだ機能するのか？ こうした科学は、AI生成の証明がまだ多くないため存在しないが、AI生成の数学を受け取り、より理解しやすくする新しいタイプの数学者が生まれるだろう」という部分は、コードの公開API設計に対する私の考えとまったく同じ
従来は熟練開発者だけが担っていた役割が、今では大幅に単純化され、誰もがアクセスできるものになり得る