機械的な推論のことばっかり考えて何がうれしいのか
2019年6月24日のコメントペーパーより。レジュメは古典述語論理。
コメント：他の講義でも論理学を扱う話が出てきたのだが、論理学は「適切な設定さえあれば自動的に解を導出できる」ことを担保するのみであり、この「適切な設定」の決定、つまり人間が人間として関与できる唯一の部分に踏み込めていない感が依然として残る。
回答：論理学者としては、まずは、「適切な設定さえあれば自動的に解を導出できる」ことそれ自体に驚いていただきたいと思います。論理学というものが生まれて2000年以上、満足いく自動化はできなかったわけですから。そして、そのような自動化の仕組みを作ること自体も、ある意味で「適切な設定」を求める営みの一部であり、そこに多くの人の英知が注がれてきていることも理解いただければと思います。
これは、「論理学者の苦労をわかってください」という浪花節にとどまる話ではなく、推論の自動化を目指す過程で例えば、計算可能性理論が生まれ、現代のコンピュータの理論的基礎が築かれましたし、論理学 (述語論理) はそのなかで計算 (決定) 不能性という興味深い現象の実例を提供しています。推論の自動化は、人間の科学的な概念枠組みに大きな進展と変容をもたらした出来事だったわけです*1。
また、推論の自動化はさいきんでは十分に実用化されて、数学ではコンピュータによる自動証明が行われるようになっています。囲碁や将棋においてAIが人間を大きく凌駕しつつあるのと同じように、数学でも「人間の理解を超えた証明」というものの登場が現実味を増してきています。機械的に計算され、それゆえに形式的には正しいが、難しすぎて人間の理解を超える証明というのは、「証明」とみなされうるでしょうか。推論の自動化は、「人間が人間として関与できる」部分、すなわち「理解」の領域にある意味で踏み込みつつあります。少し手前味噌になりますが、
第1章Bなどを読むと、問題の所在がわかるのではないかと思います。
もう一つ付け加えておくと、このような種類の議論においては、「自動的」ないし「機械的」なものの領域と、「人間的」なものの領域との境界線をあまり固定的に考えないのがよいと思います。昨今のディープラーニングは、いわゆる「人間らしい」領域、例えば美的判断などにも適用範囲を伸ばしつつありますね。他方で、人間がむしろ機械を模倣し、それを通して自らの直観や理解を拡張するということも、数学ではよく起こることです。これについては、
森田真生 (2018) 「計算と仮説」,『新潮』2018年3月号, pp.175-190.
昨日発売された『新潮』（3月号）に「計算と仮説」と題した論考を寄稿しています。小題の構成は以下の通りです。《純粋計算批判としての認知科学／計算という生命現象／記号操作の場／リーマンと「仮説の詩」》計算の生命性と普遍性を同じ地平で把握しようという試みです。 pic.twitter.com/OpFO80FT9b
— 森田 真生 (@orionis23) February 7, 2018
がとてもおもしろく、またわかりやすいので、ぜひ読んでみてください。
