ビッグ・データとビッグ・ソフトウェア

この間、大規模システムでのディープラーニング技術の応用事例を調べていたのだが、こういう文章に出会う。

「ビッグ・ソフトウェアは、人間が一人で設計、展開、運用することができない（？）ような、非常に多くの動く部分で構成されたソフトウェアのクラスである。これらは、そもそもは単一のマシンに格納できないビッグデータを呼び起こすことを目的としていた。 」

まあいいだろう。現代は、ビッグ・ソフトウェアの時代なのは確かだ。確かに、大規模システムの管理は難しい。

「ここにこそ、AIが登場する。我々は、ディープラーニングが大規模システム管理の未来だと考えている。ニューラルネットは、大量のデータから、干し草の山から、針を見つけることができる。ニューラルネットは、従来のシステム管理者の能力を大幅に拡張し、その役割を変革するツールとなる。」

これも、まあいいだろう。大規模システムの管理に使えるツールがあるなら、なんでも使えばいい。ただ、次の未来像は怪しい。

「AIが学ぶにつれて、最後には、自己修復型データセンターが標準になる。 AIは、手元のリソースに適応したより優れたモデルを発見するので、最終的にはインフラストラクチャを改善および再構築するためにコードを修正することができる。」

ディープラーニングには、プログラムのロジックが理解できない。コードを読んでバグを見つけて、それを修正するなんて、ディープラーニングには、逆立ちしたってできないのだ。

多少、鼻が歪んでいても、目がつり上がっていても、ディープラーニングは、それを同じ人間だと同定できる。それはそれで素晴らしい。ただ、ソフトウェアの場合には、それがどんなに大きなソフトウェアでも、一箇所でもバグがあれば、それがシステム全体をダウンさせる可能性がある。

ビッグ・データとビッグ・ソフトウェアを、どちらも「ビッグ」だからと、同じ仲間だと考えるのは大きな間違いだ。

幸いなことに、このビッグ・ソフトウェアの分野では、ディープラーニングではない「Yet Another AI」技術が、花開こうとしている。

どういうムーブメント（ディープラーニングに対して、「ディープ・スペシフィケーション」 Deep Specification と言ったり、あるいは、数学基礎論にならって、「ソフトウェア基礎論」と言ったりする）かは、次のビデオを見るのがいい。

「もうじき来るぞ。毎日のソフトとハードの開発に、機械がチェックする数学的証明が。Coming Soon: Machine-Checked Mathematical Proofs in Everyday Software and Hardware Development 」
https://media.ccc.de/v/34c3-9105-coming_soon_machine-checked_mathematical_proofs_in_everyday_software_and_hardware_development

彼は MITのAdam Chlipalaだ。RISC-Vのプロジェクトにも参加している。

チッパラは、現在利用されているコードは、ほとんど信頼性のチェックを受けていないのだが、この10年のうちに、全てのコードが「上から下まで」（ハードウェア設計、ファームウェア、CPU、機械語、コンパイラー、開発言語、アプリケーション、仕様）、機械による信頼性チェックを受けるようになるだろうという。

その手段として、急速に能力と応用が拡大しているCOQ等の「証明支援システム」を使う。それで、大幅に時間もコストも下げられる。そうして、デバックも、テストも、コードレビューもなくて済むという。デバッグは「証明」に、テストは「仕様」に、コードレビューは「仕様のレビュー」に代わられる。

こうした構想は、ビッグ・ソフトウェアの時代への対応として、僕にはとても説得力のあるものだ。

彼の本を二冊紹介しよう。

"Formal Reasoning About Programs"  http://adam.chlipala.net/frap/
Coqを紹介しながら、プログラムの意味論とその証明の方法を解説している。

"Certified Programming with Dependent Types"
http://adam.chlipala.net/cpdt/cpdt.pdf

年配のプログラマーなら、プログラムの「証明」といえば、 {P} c {Q}といったHoareの「三つ組」を目にしたことのある人も多いだろう。ただ、この古典的な方法では、ヒープをアロケートして、そこへのポインターとそれが参照する値を操作するというような「副作用」のあるプログラムでは対応が難しい。この本の8章以降で、Hoareの理論を「型の理論」に拡張した、Hoare Type Theory というのを提案している。これは、もちろん、monadoの拡張にもなっている。素晴らしい！

チッパラは、ソフトウェアの歴史に精通し数学に強い、とても優秀な人だ。そのうち、彼の時代が来るだろう。