Line 1: Error: Invalid Blog('by Esehara' )

または私は如何にして心配するのを止めてバグを愛するようになったか

>> Zanmemo

あと何かあれは 「esehara あっと じーめーる」 か @esehara まで

もう一つの人工知能の物語ーー『コンピュータは数学者になれるのか?』

今日の風景

f:id:nisemono_san:20160604143224j:plain

類似性について

まえおき

言いわけになってしまうが、著者はこの手の文献を正確に把握する知性について欠けているところがあるため、もしこの文章を読んで本書について興味を持ったら、是非購入してほしい。以下は、あくまでも購入の参考にして頂ければと思う。

なぜ囲碁をコンピュータにやらせるのか

例えば、近年に話題になったトピックとして、AlphaGoがある。僕はAlphaGoのことについて詳しくはわからないけれど、ディープランニングによって棋譜を大量に学習した結果、囲碁を専門にやっていた人間からすれば意味のわからない手を打ちまくった挙句勝利したということらしい。

この結果については色々と考えることができる。この手の知性に関して、既に機械は我々を越え、その地位をおびやかすのではないか、とか、その手の問題だ。でも、今回の書評の文脈で考えたいのは、そこではなく、この手の「機械にやらせる」ということは、この手の人間の知性についての洞察を与えることに繋っているのではないか、ということだ。実際、このAlphaGoの打ち手は、人間の囲碁に対する接し方の死角をついていたわけで、それによって、自分達の知性なるものについて、内省させられた筈なのだ(たぶん)。

ならば、コンピュータに数学をやらせてみる

で、話題は変わるけれども、もう一つの知性のあり方として「数学」というものがある。本書の定義するところだと、「数学的真理とは、証明が与えられて初めて真理と認められるもの(p.13)」としている。そこで、証明を構成するためには「これこれの手順を使ったものが証明である」という「証明のルール」みたいなものが必要になる。それが「推論規則」だ。

例えば、足し算に対して、「1 + 2 = 3」というものを証明しようとした場合、まず2、3、5を表現しなければならない。本書では(そして、このブログでも何度も出てきている)後続者関数S0で表わそうとする。もしS(0)ならば1だし、S(S(0))ならば2だ。このように数字を表現すると、上の式はS(0) + S(S(0)) = S(S(S(0))))となる。

さて、これだけだと、果して「1 + 2 = 3」が正しいかどうかはわからない。我々の場合、長年の教育結果によって、「1 + 2 = 3」は正しいということが間髪入れずにわかるわけだけれど、しかし相手がコンピュータだった場合、まだこれが正しいとも判断ができない。したがって、推論規則を定義してあげないといけない。本書ではかけ算の場合もあるが、今回は足し算に限って考えてみよう。

t = v かつ u = v なら t = u (e2)
S(t) = S(u) なら t = u (e5)
t + 0 = t (a3)
t + S(u) = S(t + u) (a4)

この四つを使えば、「1 + 2 = 3」を規則として展開することができる。疑似言語っぽく記述するならば:

S(0) + S(S(0)) = S(S(S(0))) by (e2) {
  S(0) + S(S(0)) = S(S(0) + S(0)) by (a4)
  S(S(S(0)))) = S(S(0)) + S(0))
  => S(S(0)) + S(0)) = S(S(S(0))) by (e5) {
    S(0) + S(0) = S(S(0)) by (e2) {
      S(0) + S(0) = S(S(0) + 0) by (a4)
      S(S(0)) = S(S(0) + 0)
      => S(S(0) + 0) = S(S(0)) by (e5) {
        S(0) + 0 = S(0) by (a3) {};
      }
    }
  }
}

といった規則になるだろう。慧眼な読者ならば、この形式的な証明が、いわばプログラミングにおける導出に近いものであるということに気がつかされると思う。実際、プログラムの判断もまだ、このような形式化によって達成されている側面があるし、「証明とはプログラミングである」という話題が第四章で展開される。このように、形式化し、拡張していけば、ある程度の証明を書きくだすことのできるコンピュータは作成できる。

しかし、本書の言うところによれば、これは「原理的能力」、つまり「どのようなことができるのか」ということであって、じゃあ「どのようにやっていくのか」については別問題であり、そこに数学者の才能があらわれる、と本書では提起している。

決定可能と半決定可能

本書では、自然数よりも実数の集合のほうが濃度が濃いことを示す対角線論法であったり、はやあしではあるけれども、ゲーデル数の話題も扱っている。自分の中で面白かったのは、決定可能な計算と、決定不可能な計算というものだろう。

簡単に言ってしまえば、前者は正解と間違いの場合を出力できるのに対して、後者は正解の場合のみにしか出力できない。例えば、素数に判定に関しては、約数が見つかれば「素数ではない」と決定できるわけだし、約数が見つからず、ある規定値まで調べ終ってしまえば「素数」とすることが可能である。

従って、二つの答えを出すことができるわけだから、これは決定可能だということができる。後者の半決定可能に関しては「プログラムの停止問題」(「プログラムPと自然数nを与えた場合に、プログラムPは停止するのか?」という問題)が属しているという。

計算とはなにか

とはいえ、本書によれば、これは別段コンピュータがあって考えられたものではなく、チューリングが「計算する」ということがどういうことなのか、について厳密に捉えようとした結果だとしている。そして、計算の本質は「あらかじめ決められだ規則に従って基本ステップを繰り返すこと」だとしている。だとすると、最初にルールを作り、そこの規則に従うことをやっていたのは、まさに「計算とは何か」ということを形式化したことに他ならない。

とはいえ、形式化したことによって、何がよろこばしいのか、といえば、現代の数学的な能力というものが何なのか、というのが明確になるからだ。だが、本書で伸べられているように、「人間数学者は直感やインスピレーションにより真理を看破し、証明の道筋を見抜く(p.133)」からこそ、人間数学者は圧勝しているといってもいい。しかし、これは疑問点が残る。

ここからは本書の意見というよりかは、自分の意見となるのだが、乱暴に言ってしまえば、ディープランニングが衝撃的だったのは、このような「直感」そのものが、「実装可能なもの」なのではないか、ということだった。実際、本書においては、この手の推論規則を「将棋の駒の動きのような」という例えをしている。

もし、運用にさいする直感を機械学習的に学ぶことができたとすると……と妄想するのだが、僕は、これらに詳しいわけではない。でも、直感自体が、何か別のフレームによって強化される、というのは十分にありえるシナリオなんじゃないかな、と思ったりもする(とはいえ、公平に本書では339頁において、機械学習の支援を受けた自動証明システムの話題について、振れている)

計算が停るということは、証明も終わるということ

第3章から第4章に関しては、『コンピュータは数学者になれるのか』という本題である以上、コンピュータの問題を扱っている。実際に、4章に関しては「N、NP問題」について取りあつかっている。

自分でも、このあたりになると、自分の理解がおいつけなくなる問題ではある。第3章の話題は次のようになる:

ざっくりと言ってしまうならば、「なんらかの集合との大小関係において、そのXの要素からなる無限下降列が存在しないときは、整列集合」と呼ぶ。

このとき、整列集合とは、いつかは一番底が来てしまうことだと説明ができる。この一番底が来るとき、プログラミングなら「終り」ということができるし、証明ならば完了ということができる。そして、この整列集合みたいなものは、証明における形式系ても作れるということだ。

そのあたりについて、本書で伸べている寓話に沿って説明すると、次のようになる。

ある国では、金貨と銀貨と銅貨がある。金貨は銀貨に対して絶対的な価値を持つ。同様にして、銀貨も銅貨に対して絶対的な価値を持つ。絶対的な価値、というのは、銀貨は幾ら集めても、金貨と交換できないのに対して、金貨は、銀貨に対して有限の、どれだけものお金を請求できる。金貨一つで収入の無い、買いものだけの生活をした場合、無限のステップにおいてはいずれ破産する、というものである。

このようなものの一つとしてヒドラゲームというのが紹介されている。これも尋常ではないほど増幅する可能性はあるが、しかし無限のステップを踏んでいけば、いずれはヒドラの首は退治できる。これを証明図にも応用すれば、同じように証明図ができるという。

プログラミングは証明であるということ

第5章は、恐らくこの本書の中でも一番スリリングになる部分だろう。本書はとにかく広範な話題を拾いながらも、なんとか二つのテーマを横断しようとしているように見える。一つには、数学における証明とは何か、そしてその限界とは何か。もう片方は、計算とはなにか。特にコンピュータにとって、という二つの問題が出てくる。その、証明と計算とのであいが、第5章において語られる。

その主役は、ラムダ計算である。

第5章においては、ラムダ計算と論理図の類似性について語られる。また、Coq Proof Asistantの紹介に関しても振れられている。

まとめ

というわけで、さらっと本書について概説をしてみた。最後のほうはまだ理解できていない部分ではあるので、後日 じっくり読むとは思う。

本書に関しては、とても興味深く、刺激的な本であり、書きかたも専門的なところと、砕けたところがいい意味でマッチしていると思う。まだ、いわばゲーデルの不完全定理のような「何ができないか」ということから、「じゃあ、どこまでいけるのか」というポジティヴさに持っていくところも論点として面白い。

もし難点があるとするならば、様々なトピックを早足でかけぬけているために、議論をおいかけようとすると、やや省略されていると思わしき点が若干でてくるため、興味を持ったトピックに関しては、また別に専門の本で深める必要はあると思う。

また、やはり興味が付きない点としては、「証明支援系+自動定理証明+機械学習」という点だろう。最初に伸べたように、もしかしたら、数学の証明それ自体が、「人間にとって自然な運用」といったところに束縛されていて、既存の証明では全く奇々怪々ながらも「認めざるを得ない証明」というのを出す機械というのはでるかもしれない。

そうすれば、我々が行なっている数学というものについて、より深い洞察を与えてくれるかもしれない。それは、とてもポジティヴなことだと思う。そういうことを考えさせてくれる良い本だった。