Hatena::ブログ(Diary)

shi3zの長文日記 RSSフィード Twitter

2017-02-16

バグのないプログラムを書くことは理論上は可能である 08:22

プログラムのわからないえらい人「バグのないプログラムを書くことはできないのか?難しいかもしれないが、十分に気を付けていれば防げるのではないか?」にどう返したらいいのかわからない

http://anond.hatelabo.jp/20170214114736

バグのないプログラムを書くことは理論上は可能である。

そのためのツールもノウハウもある。


それを定理証明支援系言語と呼ぶ。


定理証明支援システムまたは自動証明器のためのツールとしてはCoqやAgdaが有名


Coq - Wikipedia

Agda - Wikipedia


そしてそんなことはどうやら今どきの女子大生でも常識らしい


証明プログラミング超入門

http://www.slideshare.net/ussopyon/ss-43846794


だけど数学的証明を普通の人が理解するのは難しい。

なぜなら数学が人間の自然な知能には受け入れがたい概念だからだ。


ディープラーニング以前の人工知能研究は一言で言えば全て失敗してきた。

人工知能が作れる見込みもないのに膨大な予算と人員が投入され、なんの成果もでないまま何十年と過ごしてきた。


その理由は、もともとの人工知能研究は、人間の脳の構造ではなく、人間の思考の様式について研究してきたものだからだ。


しかし、人間の思考にとって数学的、論理的思考は、決して自然なことではなかった。

単に我々人類は、それが不自然なことであると気づかなかっただけなのだ。


直感や経験則に頼ることが、恥ずかしく、みっともなく、知性的(Intelligence)な行為ではないと断じるところから人工知能の研究がスタートしていた。ディープラーニングが明らかにしたのは、単にその考えが間違っていたということだ。


人間の持つ直感こそが、知性というものの正体の大部分である。その発見こそがディープラーニングによって停滞していた人工知能研究が息を吹き返し、ついに真の人工知能の実現に向けて大きく前進しだした。


これは、それまで人間の認知のなかで支配的だった、絶対的全能者としての神を想定し、我々人類は神の御心のままに生きるしかないという宗教的観念に対し、「我々は無知である。絶対的なものは自然環境しか無く、自然環境そのものは我々に全く無関心である」とという「無知の発見」から出発した科学の発生と近しい前進といえる。


「無知の発見」から、我々にとって確かな拠り所は論理だけであるという結論を導き、論理を積み重ねることが知性そのものを意味するようになって数世紀が経ち、我々人類は論理的思考能力こそが人間の知性の真価であると思い込んだ。


ところが実際には囲碁に勝利したAIは、全く非論理的なものだった。

囲碁やチェスで勝つプレイヤーは頭の中が高度に論理的なのだと信じられていたのだが、実は直感力だけで勝ち進めることが分かった。


すると、数学という論理構造のみによって成り立つ巨大な思想体系は、実は人間にとって後天的な知性であり、人類の多くは数学という論理構造全体を受け入れることが難しい。


プログラムにバグがつきものというごく自然に思える性質は、数学的証明には間違いがないという論理構造の体系と正面からぶつかる。


プログラムにバグがつきものなのは、人間の知能の大部分が非論理的な直感によって成立しているからで、ディープラーニングによって学習された人工知能が100%正しい答えを出すことはできないという性質そのものと酷似している。


反対に、一度、数学的証明がなされた数式は、絶対永久的に不滅である。これが数学という論理体系が人類最強の武器でもある理由だ。


その数学的証明の性質を用いて、バグのないプログラムを作る、いわばあるプログラムにバグがないことを「証明」する手法が、定理証明支援系言語である。



ただ、まだまだ難しいし、そもそも数学的証明が人類には難しいので、ここらへんを自動的にやってくれる人工知能が生まれたら、きっと我々人類はさらに強力な道具を手にすることになるんだろうなあ