神託、魔法使い、数学的証明 （２）
先に、数学の「複雑性理論」という分野には "Oracle（神託）" という考え方があることを紹介した。どんな問題にも、「正しい」答えをすぐに返してくれるという、架空の「全知全能」であるシステムのことだ。
ただ、まったくの「御都合主義」にも見えるそうした仮定は、実は、現代の我々の日常に深く入り込んでいる。古代ギリシャのOracleを引き合いに出さなくても、僕は、"Google" という用語を使った方がわかりやすいと思うのだが。
今回は、このOracleの少し変わったバージョンMerlinを紹介する。ランダムな振る舞いをするOracleだと思えばいい。このMerlinは「全知全能」である点は「普通」のOracleと変わりないのだが、ただ、クセがある。不誠実なのだ。人間の問いかけに、いつも「正しい」答えを返すとは限らない。ときどき、わざと間違った答えを返す。（こっちを、"Google"と呼んだ方がいいのかも）
ただ、これだけだと、単なる「神頼み」にしかならないので、人間の知の数学的モデルとしてはつまらない。そこで、もう一人のAuthurが登場する。Authurは、Merlinほどの能力はないのだが、誠実である。その上、彼は、Merlinがいうことが正しいか正しくないかの判断を「正しく」行う能力は持っている。
Merlinが「数学的証明」を提供し、Authurがその証明を「検証」するというシステムがあった時、このシステムで何がわかるかを考えるのを「Merlin-Authur問題」という。
僕は、Scott Aaronsonの"Quantum Computing since Democritus" https://goo.gl/dwjtsc で、この問題を知ったのだが、そうでなければ、ずっと「Merlin-Authur問題」を、二人のMerlinとAuthurという名前の数学者が考えた問題だと思っていた可能性がある。（原論文は、L.Babal "Trading group theory for randomness" https://dl.acm.org/citation.cfm?id=22192 )
実は、Merlinは魔法使いで、Arthurはその主君である、「アーサー王伝説」のあのAuthurである。（僕は、huluで「魔術師マーリンの冒険」を見ていた。https://goo.gl/HfwZCf 「円卓の騎士」とは随分アレンジが違うけど、楽しかった。）
「神託」の次は、不誠実な「全知全能の魔法使い」！
でも、この「誤る可能性のある証明者」とその「検証者」というフレームは、数学の証明の現実を考えると、とても説得力があるのだ。いくつか例を挙げよう。
「フェルマーの定理」は、最終的には、1995年のAndrew Wilesの論文によって証明されたが、フェルマー自身は、この定理を証明出来たと信じていた。それが、誤った「証明」であったのは確かである。Wiles自身も、95年の論文以前に一度、「証明した」とする発表を行うが、誤りが見つかり、それを撤回している。
2000年頃、Voevodskyは、1993年に自分が発表した論文の重要な補題が間違っていたことに気づく。でも、その頃には、その論文は広く出回っていて、多くの数学者がその証明を「信じて」いた。彼が、その間違った補題なしでも、論文の結論が正しいことを証明できたのは、2006年になってからだった。
世紀の難問である「リーマン予想」は、何度か「証明」が発表されている。今までのところ、それは誤った「証明」だった。（最近のAtiyah !）
Grigory Perelmanは、2002年から2003年にかけて arXiv に投稿した論文で、「三次元のポアンカレ予想」を解いたと主張した。arXivは、学会の論文誌とは異なり、掲載の可否を決める査読が基本的にないので、発表の時点では、彼の論文以外に、彼の証明が正しいという裏付けはなかった。彼の証明の検証は、複数の数学者のグループで取り組まれ、最終的に彼の証明の正しさが「検証」されたのは、2006年のことだった。
重要なことは、先の最後にも書いたのだが、人間の知のあり方には、それに対応する数学的モデルが存在するということだ。
「人工知能」を考察する基本的なフレームワークとして「複雑性理論」に、僕が注目するのは、ベタ・レベルでの人工知能の礼賛や否定とは異なって、それが、そうしたメタ・レベルでの考察を可能にする切り口を豊富に提供してくれるからである。
哲学的には、こうした考察をデカルトは既にしている。「我思う、故に、我あり」というフレーズを、皆知っていると思うけど、この結論に至る過程で、彼は「欺く神」という思考実験をしている。「Merlin-Arthur問題」は、このデカルトの「欺く神」の現代版だと思っていい。
ただ、まったくの「御都合主義」にも見えるそうした仮定は、実は、現代の我々の日常に深く入り込んでいる。古代ギリシャのOracleを引き合いに出さなくても、僕は、"Google" という用語を使った方がわかりやすいと思うのだが。
今回は、このOracleの少し変わったバージョンMerlinを紹介する。ランダムな振る舞いをするOracleだと思えばいい。このMerlinは「全知全能」である点は「普通」のOracleと変わりないのだが、ただ、クセがある。不誠実なのだ。人間の問いかけに、いつも「正しい」答えを返すとは限らない。ときどき、わざと間違った答えを返す。（こっちを、"Google"と呼んだ方がいいのかも）
ただ、これだけだと、単なる「神頼み」にしかならないので、人間の知の数学的モデルとしてはつまらない。そこで、もう一人のAuthurが登場する。Authurは、Merlinほどの能力はないのだが、誠実である。その上、彼は、Merlinがいうことが正しいか正しくないかの判断を「正しく」行う能力は持っている。
Merlinが「数学的証明」を提供し、Authurがその証明を「検証」するというシステムがあった時、このシステムで何がわかるかを考えるのを「Merlin-Authur問題」という。
僕は、Scott Aaronsonの"Quantum Computing since Democritus" https://goo.gl/dwjtsc で、この問題を知ったのだが、そうでなければ、ずっと「Merlin-Authur問題」を、二人のMerlinとAuthurという名前の数学者が考えた問題だと思っていた可能性がある。（原論文は、L.Babal "Trading group theory for randomness" https://dl.acm.org/citation.cfm?id=22192 )
実は、Merlinは魔法使いで、Arthurはその主君である、「アーサー王伝説」のあのAuthurである。（僕は、huluで「魔術師マーリンの冒険」を見ていた。https://goo.gl/HfwZCf 「円卓の騎士」とは随分アレンジが違うけど、楽しかった。）
「神託」の次は、不誠実な「全知全能の魔法使い」！
でも、この「誤る可能性のある証明者」とその「検証者」というフレームは、数学の証明の現実を考えると、とても説得力があるのだ。いくつか例を挙げよう。
「フェルマーの定理」は、最終的には、1995年のAndrew Wilesの論文によって証明されたが、フェルマー自身は、この定理を証明出来たと信じていた。それが、誤った「証明」であったのは確かである。Wiles自身も、95年の論文以前に一度、「証明した」とする発表を行うが、誤りが見つかり、それを撤回している。
2000年頃、Voevodskyは、1993年に自分が発表した論文の重要な補題が間違っていたことに気づく。でも、その頃には、その論文は広く出回っていて、多くの数学者がその証明を「信じて」いた。彼が、その間違った補題なしでも、論文の結論が正しいことを証明できたのは、2006年になってからだった。
世紀の難問である「リーマン予想」は、何度か「証明」が発表されている。今までのところ、それは誤った「証明」だった。（最近のAtiyah !）
それらは「誤った証明」の例だが、逆の例もある。
重要なことは、先の最後にも書いたのだが、人間の知のあり方には、それに対応する数学的モデルが存在するということだ。
「人工知能」を考察する基本的なフレームワークとして「複雑性理論」に、僕が注目するのは、ベタ・レベルでの人工知能の礼賛や否定とは異なって、それが、そうしたメタ・レベルでの考察を可能にする切り口を豊富に提供してくれるからである。
哲学的には、こうした考察をデカルトは既にしている。「我思う、故に、我あり」というフレーズを、皆知っていると思うけど、この結論に至る過程で、彼は「欺く神」という思考実験をしている。「Merlin-Arthur問題」は、このデカルトの「欺く神」の現代版だと思っていい。
コメント
コメントを投稿