id:bonotake（今井健男）さんから、「こんな論説を書きました」と連絡をいただきました。
- 計算機科学から見たディープラーニング
この論説を紹介し、僕の感想を述べたいと思います。「計算機科学から見たディープラーニング」は、『n月刊ラムダノート〈エヌゲッカンラムダノート〉』の Vol.1, No.2 に掲載された記事です。関連するブログ記事もあります。
ちなみに、この号（Vol.1, No.2）には、他に次の記事もあります。
三つとも面白そうですね。
内容：
プログラムとしてのディープラーニング
この論説においてbonotakeさんは、ディープラーニングの現状を要領よくおさらいした後で、ひとつの提案をしています。その提案をまず紹介しましょう。
ディープラーニング技術により何らかのタスクを遂行することを、「プログラムの作成／作ったプログラムの実行」と考えよう、とbonotakeさんは言っています。ディープラーニング・ソフトウェアもプログラムなのだ、ということですね。この観点は、当たり前のこと（「そりゃそうだろ」なこと）を言っているようですが、それに引き続く主張(すぐ下)と組み合わせると、まったくもって非自明な課題を突きつける事になります。
- ディープラーニング・ソフトウェアがプログラムであるならば、プログラム意味論があって然るべき。
技術的論説ですから、特にケレンもないフラットな語り口なんですが、内容としては随分と強烈なアジテーションだな、と僕は感じました*1。
僕自身はディープラーニングに無知ですし*2当事者でもありませんが、それにもかかわらず、食道から胃にかけて鈍痛が走り、体調が悪くなりそうでした。
「プログラムなら、プログラム意味論が必要でしょ」もまた、当たり前の主張ではありますが、ディープラーニング・ソフトウェアのプログラム意味論を構成することは、部外者をして胃痛をもたらすほどに、チャレンジングな課題です。
従来のプログラムとは著しく異なったパラダイム
「ディープラーニング・ソフトウェアもプログラムである」とはいえ、従来のプログラムとはだいぶ違ったプログラムです。「オブジェクト指向と関数型は違う」とかいうレベルの違いではなくて、もっと根本的な違いがあります。
そのため、従来のソフトウェア開発とディープラーニング・ソフトウェア開発では、互いに対応を取る（類似性を探る）のさえ困難です。この「対応」については、bonotakeさん論説に解説があります。ここでは、「何を／誰が／どうやるのか」を表にまとめてみます。
| 作業 | 従来プログラミング | ディープラーニング |
|---|---|---|
| 仕様作成 | 人間が、 | 人間が、 |
| 仕様の作成手段 | 文書により行う。 | ある種のコードにより行う。 |
| ソフトウェア実装 | 人間が、 | コンピュータが、 |
| 実装の作成手段 | コードにより行う。 | データからの学習により行う。 |
| 最終成果物 | ソースコードのファイル*3 | 最適化問題の解としてのパラメータ群 |
人間が文字を連ねてなにか書く作業を「コーディング」と呼ぶなら、ディープラーニングにおけるコーディングは仕様文書ライティングに相当します。ディープラーニングの実装における作業者はコンピュータであり、人間はデータを与える役割を担います。
最終成果物であるパラメータ群は数十万個にも及び、まったく人間可読ではないので、コードレビューのようなことは不可能です。コードレビューに代わる効果的デバッグ手段もないようです。
そもそもテストやデバッグをするには、「これが正しい動作だ」と事前に分かっている必要があります。しかし一方、プログラムの正しさがハッキリとは確定できない状況でディープラーニングが利用されることを考えると、従来型のテスト／デバッグも（そのままでは）意味を失います。
今までのプログラミング・パラダイム間の違いは「似たり寄ったりだから同類でいいだろう」と見なせるほどに、今までとは違った・異なったプログラミング・パラダイムが登場しつつあるのです（と、bonotakeさんが言ってます）。
ホーア論理とプログラム意味論
プログラム意味論を含む形式手法〈formal method〉の基本としてホーア論理があります。「釣りはフナに始まりフナに終わる*4」とか「フレンチはオムレツに始まりオムレツに終わる」とか言いますが、僕は「形式手法はホーア論理に始まりホーア論理に終わる」と思っています。
なにかを形式的に扱いたいとき、「ホーア論理から始めてみる」というのは良いアプローチです。実際、bonotakeさんは、このアプローチを（少なくとも当面は）採用しています。
ホーア論理*5は、ホーアトリプル（あるいはホーア式）と呼ばれる表現を論理式とする論理です。事前条件と呼ばれる（通常の）論理式P、プログラムコードC、事後条件と呼ばれる論理式Qを組み合わせた {P}C{Q} がホーアトリプルです。その意味は：
- プログラムコードCの実行前の状態がPを満たしていたなら、プログラムコードCの実行後の状態はQを満たす。
プログラムの状態空間をS、プログラムコードCは状態空間の自己写像 S→S と解釈して、通常の古典論理の論理式に翻訳するなら：
- ∀x∈S.( P(x) ⇒ Q(C(x)) )
今の説明は、あくまで従来型のプログラミングでのこと。ディープラーニングでの状況となると、プログラムコードCというのがハッキリしません。状態空間Sの確定も簡単ではないでしょう。古典論理やその変種をそのまま使うわけにもいきません。真偽がTrue, Falseの二値で決まるような世界ではないですから*6。
先に「ホーア論理に始まりホーア論理に終わる」と言いましたが、「ホーア論理がすべてだ」とは言ってません。論理体系による定式化（公理的意味論）だけでなく、ディープラーニングの表示的意味論〈denotational semantics〉も欲しくなります。でも、ディープラーニングのデノテーション〈表示〉とは何なのでしょう、何であるべきなのでしょう？-- 部外者の檜山でも胃が痛くなる感じが、少しは伝わったでしょうか。
しかし、それでも意味論は必要
プログラムが動くメカニズムはどうであれ、実行系と経験だけでは正しいプログラムは作成できません。いや、何が正しいかさえ不明のままです。ディープラーニング・ソフトウェアもまたプログラムであるならば、意味論〈セマンティクス〉は確かに必要なのです。
ディープラーニングはソフトウェア技術のなかでも新しくて異質です。従来型のプログラムの意味論が出来るまでには長い年月がかかっている（今でも出来上がったかどうかは定かではない）ことを考えると、現時点で「ディープラーニングの意味論を作るのは大変そう」なのは当然かも知れません。
いずれにしても、ディープラーニングの現状と課題を把握したいなら／緒に就いたばかりのディープラーニングの意味論を知りたいなら、「計算機科学から見たディープラーニング」の一読をおすすめします。
*1:[追記]bonotakeさんご本人によると、アジテーションというよりは、この分野・理論に対するプロモーション活動だそうです[/追記]
*2:このブログ記事を書くにあたって、ひととおり調べようと試みたのですが、一夜漬け・付け焼き刃でどうこうなるものではありませんでした。
*3:バイナリの実行可能ファイルのみを納品するケースもあります。
*4:フナが、ヘラブナなのかマブナなのかは議論があるようです。
*5:このブログ内の過去記事は「ホーア」の検索結果としてリストできます。
*6:統計的な真偽値をとる論理に関しては「ベイズ確率論、ジェイコブス達の新しい風」参照。
