数学の基礎と型の理論と 計算機科学
【 数学の基礎と型の理論と計算機科学 】
今回のセミナーのテーマは、「人工知能と数学」ですが、このセッションでは、少し視点を変えて、もう少し広く「計算機科学と数学」の関係を考えてみようと思います。「計算機科学」と「数学の基礎」の関係が一つのテーマです。
数学の知識は、科学と技術のほとんどの分野で広く利用されています。ITの世界でも、数学の応用のスタイルは基本的には同じです。ただ、IT技術者が「数学の基礎」を意識すること -- 数学を利用・応用するだけでなく、なぜそれが可能なのかを考えることは、あまりないように思います。それは、IT技術者だけでなく、他の科学や技術の他の分野でも、数学との「距離感」は、基本的には同じかもしれません。
ただ、「人工知能」が日常的な話題になる今、数学の基礎をめぐる議論は、新しい形で甦りつつあります。
なぜなら、20世紀の「数学の基礎」をめぐる最初で最大の発見は、1930年代に行われた「論理的・数学的証明可能性は、計算可能性と等しい」という発見でした。それは、「チャーチ＝チューリングのテーゼ」という定式化を経て、「（機械によって）計算可能なもの は、証明可能である」という性質を明確に数学的に定式化することに成功します。
「（機械によって）」と括弧を付けたのには、理由があります。それは、この発見がなされた当時、「計算する機械」コンピュータは、まだ存在しなかったからです。
現代の「人工知能」をめぐる中心的な関心は、「計算機が計算可能な「知能」は、どのようなものか」という問いにあります。ただ、こうした問いに答えるのは、「応用数学」の知識ではなく、「数学の基礎」についての知識なのです。
今回のセッションでは、「数学の基礎」と「計算機科学」を結びつける「繋ぎ手」の領域として、「型の理論」に注意を喚起しています。この分野の重要性については、今回のセミナーでも説明していきたいと思います。
ただ、「数学の基礎」と「計算機科学」の距離は、想像以上に「遠い」ことも事実です。それには、いくつかの要因があります。
まず、「数学の基礎」の分野での基本的発見が、1930年代と、コンピュータのなかった遠い昔の出来事だったことが、一つの要因です。今から、90年前ですもの。ただ、科学的知識は、人間と違って経年劣化するものではありません。
もう一つには、この発見の口火を切ったのは、「ゲーデルの不完全性定理」なのですが、この定理は、名前が有名な割には、多くの人に「難解で理解困難なもの」と思われていることがあります。ただこの一連の研究の結論を、「論理的・数学的に 証明可能なものは、機械によって計算可能である」と言い換えれば、その主張はシンプルなものです。
ただ、それだけではありません。
今回のセッションでは、「数学の基礎」と「計算機科学」を結びつける「繋ぎ手」の領域として、「型の理論」に注目しているのですが、「型の理論」の成果が「計算機科学」でプログラム言語として実装されるまでの間に、大きな「時間的ギャップ」があるのです。その「時間的ギャップ」は、なんと、30年から40年もあるのです。
多くの人は、現代の科学技術の「最先端」に、「人工知能技術」があると感じているかもしれません。それは、ある意味では誤解です。「計算機科学」はある分野では、何十年もの単位で、数学的認識に遅れをとっています。
この「遅れ」の現在の最大の表れは、人間の知能の中心的能力の一つである「論理＝数学的推論能力」に、実践的にはDeep Learning という無駄な回り道を通じてアプローチしようとしていることです。
-------------------------------------
コメント
コメントを投稿