我々は知らねばならない – 我々は知るだろう
Wir müssen wissen – wir werden wissen (remy.wang)
要約
この記事は、数学におけるヒルベルト・プログラムの挫折と、それが現代のAIとコンピューターサイエンスに与える影響について論じています。ゲーデルの不完全性定理とチューリングの決定不能性定理により、数学の完全な公理化と自動証明は不可能であることが示されましたが、皮肉にもこれらの発見がAIとコンピューターサイエンスの発展を促しました。著者は、AIが生成したコードや数学的証明を人間が理解することを放棄する傾向に警鐘を鳴らし、科学の本質である「知る」という探求心を失わないよう訴えています。
全文翻訳
我々は知らねばならない – 我々は知るだろう
100年前、数学の世界は基礎的な危機に直面しました。いくつかのパラドックスの発見が、数学のあらゆる分野を支える柱に亀裂を生じさせたのです。その中でも最も有名なのがラッセルのパラドックスで、「自身を含まない全ての集合の集合」という矛盾した概念を示し、素朴集合論の不整合性を露呈しました。これにより、数学者たちは矛盾のない厳密な基礎を求めて探求を始めました。特に、ダフィット・ヒルベルトは、完全かつ一貫性のある公理系を設計するプログラムに着手しました。これは、公理から全ての数学的真理を導き出せる一方で、パラドックスを回避するというものでした。「真実、全てを、そして真実のみ」を目指したのです。このような目標は、数学者たちにとってその研究をより確固たるものにする自然なものでした。そのため、ゲーデルが不完全性定理によってヒルベルト・プログラムに致命的な一撃を与えたことは、まさに衝撃的な出来事でした。数学のための完全で一貫性のあるシステムは存在し得ないというのです！
このような不可能性の結果は、存在論的な危機をさらに深めるはずでしたが、数学者たちはすぐに回復し、研究を続けました。ラッセルの型理論のような素朴集合論の改善案が提案されました。そして、そのようなシステムはゲーデルの結果により形式的に一貫性を証明することは依然として不可能でしたが、それらは概ね一貫性があると信じられており、基礎の亀裂は人々が気にする種類の数学にはほとんど影響を与えないことが判明しました。実際、型理論は非常に成熟し、Leanのような対話型定理証明器の基盤を形成するまでになり、数学の大部分をコンピューター言語で形式化することが可能になり、証明をゼロからプログラムによって自動的にチェックできるようになりました。
公理系とは別に、ヒルベルトはプログラムの中で関連する目標も提案しました。それは、任意の数学的命題の真偽を自動的に判定するアルゴリズムの開発であり、これにより定理証明を規則の機械的な適用に還元することでした。この目標もまた、アラン・チューリングによって不可能であることが示されました。彼は、停止性問題の決定不能性に関する画期的な証明によって、コンピューターサイエンスという豊饒な分野を生み出したのです。ヒルベルト・プログラムの不可能性を確立することによって、ゲーデルとチューリングが、実際にできる最も強力な計算機を生み出したというのは、非常に詩的な矛盾です。
ヒルベルト、ゲーデル、チューリングの時代から一世紀が経過しました。あらゆる困難にもかかわらず、私たちは今、Leanのような証明支援システムに見られる機械化された形式システムを武装したAIエージェントとして具現化された、ヒルベルトの「証明マシン」の実現を目撃しています。この発展は、ヒルベルト・プログラムの崩壊と比較して、数学界に遥かに壊滅的な影響を与えたことが判明しました。ヒルベルト自身が、もし彼のプログラムが成功した場合の結末を考慮していたかは定かではありませんが、フォン・ノイマンは驚くべき先見の明を示しました[1]：
非決定性が失敗すれば、今日理解されているような数学は存在しなくなるだろう。その代わりに、任意の文が証明可能かどうかを決定できる、完全に機械的な処方箋が存在するだろう。
私は数学者ではなく、コンピューターサイエンティストです。コンピューティングにおいて、AIの影響はそれほど激しいものではなく、そのほとんどはコードをますます高速に生成することに貢献し、多くの人々がそれを称賛しています。しかし、私が感じているのは、見捨てられているという空気です。AIが生成したコードを読まなくなることが、標準的な実践になりつつあります。これはコンピューターサイエンスにとって大きな悲劇です。私たちは、物事の根本までたどり着くことができる、数少ない学問分野の一つです。ソースコードさえあれば、プログラムが何をするかを正確に理解できます。それなのに、私たちは今これを手放そうとしているのです！私たちは、ヒルベルトが夢見たことをすべて実行できる機械を持っていますが、彼が科学の魂とさえ考えていたものを放棄しようとしています。
我々は、今日、哲学的な態度と熟慮的な口調で、文化の衰退を予言し、ignorabimus（我々は知らない）を受け入れるような人々を信じてはならない。我々にとってignorabimusはなく、私の意見では、自然科学においても全くない。愚かなignorabimusとは対照的に、我々のスローガンはWir müssen wissen – wir werden wissen（我々は知らねばならない – 我々は知るだろう）であるべきだ。
コンピューターサイエンティストとして、私たちは数学で起きていることを考慮すべきです。すべてのテストに合格したプログラムのコードを読まないこと、たとえ形式検証済みであっても、それはLeanでAIが定理を解決した瞬間に証明を読むのを無視するのと同等です。実際、チャーチ・チューリングの提唱する計算モデルによれば、プログラムは証明であり、それがまさにLeanのような定理証明器が動作する仕組みです。AIが生成した証明が長すぎて読めない場合、数学者は理解することを諦めるのではなく、それを消化できるまで証明を単純化するために多大な努力を払います。私たちはコンピューティングにおいても同じ態度をとるべきです。抽象化を利用し、リファクタリングし、スコープを洗練し、より高レベルな言語を発明・採用し、コードを頭で理解できるようになるまで。
AIが最終的にすべての活動において人間を超えるかどうかは分かりません。私は、私たちは異なるアーキテクチャを持つ生物学的コンピューターにすぎない脳で考えていると信じていますが、機械に思考を委ねてしまえば、私たちは悲惨な結末を迎えることになるだろうと知っています。医療アドバイスのためにAIに依存して命を落とすケースが増えていることを考えてみてください。機械の言葉を当然のこととして受け入れるほど、私たちは自分たちの運命をコントロールできなくなります。我々は知らねばならない – 我々は知るだろう。
- Zur Hilbertschen Beweistheorie, Philip WelchによるTuring Centenary Lectureで見つかった翻訳。↩︎