ゼロから作るDeep Learningを読んだ
ゼロから作るDeep Learningを読み終わりました。おおよそ一ヶ月くらいかかりました。
機械学習自体(とpython)の全くの素人状態から読みましたが、とりあえず、単独で読み切れる本です。
その点は良いですね。
本全体を通して、MNISTと言われる手書き数字のデータセットを使って識別器を作っていきます。(と言っても形になるのはだいぶ後の方ですが。)
タイトルでは「ゼロから作る」と言ってますが、全部を作るとは言ってません。気をつけて下さい。
画像系のDeep Learningで重要になる(らしい)CNNの説明は最後辺りの章で出てきますが、「バックプロパゲーションは自明だから(リポジトリ中の)コード読んどいてね。」という感じになっています。加えて重要なアルゴリズムである im2col についても同様の扱いです。
他に注意点として、関数の導入時点での実装が使用時点では使えないというケースがあります。これについては文中に注意書きがありますが、使えない実装を紹介されても困りますよね…。
あとはエラッタが多い印象です。出来るだけ新しい版を買った方がいいと思います。
(エラッタは公式のgithubリポジトリにまとまっています。)
まとめると、
- 一人で読める
- deep learningについて基本なことが平易に書いてある(気がする)
- CNNについてはさほど丁寧じゃない
- pythonは破綻した言語
静的コード解析の会で停止性検証について発表してきた
静的コード解析の会#2でVeriFastによる停止性検証の導入の話をしてきました*1。
本当は私自身も発表するほど分かってないのですが、それでも楽しい部分はあるので「これまで理解している内容を詰め込んでみた」という感じでまとめてみました。(前日深夜から突貫だったので超眠かった…)
今回の発表で伝わったかは怪しいですが、停止性のために最低限の機能を導入し、既存の機能を活かした仕組みはとても素晴らしいと思います。
楽しい部分を端的に挙げると、
- 多重集合のある種の順序関係からどんどん「関数を呼ぶ権利」が出てくる
- 関数の順序関係をコード上の大小関係で決めた
まぁこれだけ聞いても絶対分からないので、詳しく知りたい方はModular termination verificationを読みましょう。
振り返り
前回に引き続きVeriFastの話ですが、今回の内容は前回と比べて取っつきにくい内容でした。
理論的にも難しい割には、そもそも停止性なんて検証して何がうれしいのかから分かりづらいと思い、検証のモチベーションから始めています。
VeriFastでは動的束縛を伴う(=関数ポインタを使った)関数の相互再帰関数といった、かなり複雑な関数の停止性を検証することが出来ます。が、発表としては面白い具体例をほとんど出せなかったのは悔やまれるところです。
他の人の発表では @tanaka_akr さんのCoq2Cの話を聞き逃したのが残念でした…。
静的コード解析の会 第0回 でVeriFastについて発表してきた
#静的コード解析の会 第0回でC言語(とJava)の検証器であるVeriFastについて発表してきました。
資料は公開してあるので興味ある人は見てください。動画もあります。
> https://metasepi.connpass.com/event/42141/presentation/
結構(私の理解が)きわどい質問も出ましたが、大体伝えたかった内容は伝わったんじゃないかと思います。
個人的には手ぶらで(ぐだぐだ)発表したProofSummit2016のリベンジでもあったので資料はかなり頑張って作りました。(内容は全然違いますが
本当に詳しく知りたい人は公式チュートリアル読むべきなのですが、これは結構ヘビーな量と内容です。これに対して私の発表は「忙しい人向けの入門」といった感じなのでお気軽にどうぞ(^^)
他の発表について
CSPというのを初めて知りました。プロセス代数というのは(多分大学生の時に)聞いたことはあったんですが、通信するプリミティブがあるなぁ、くらいのことしか分かりませんでした。
今になって説明を聞くと、多少理論的な話や記号が出てもビビらなくなったし、なんとなく理解できる部分も増えていたので嬉しみがありました(なお、日本語力は低下したもよう…)
あとCMLに似てますね(これは多分関係が逆だけど)。
自分がここ数年多少なりとも理論的な話として勉強してきた内容は、主に(型付き)ラムダ計算とその意味論だったので、実装でも仕様でもない(あるいはどちらにもなる？)ものと意味論を扱うというのは新鮮でした。
他には具体的に気になったものとしてトレース意味論というのが紹介されていました。これはプログラムの副作用を形式的に扱う方面でも出てきてよく分からなかったんですが、CSPでの扱いはかなり明快だなという感じを受けました。(プロセス間の作用が初めから限定されているから当たり前か？
あとは「coinductive」という単語も出ていたので、それを持ち出す気持ちくらいは知りたいなという感じです。
気になるワードは他にも幾つか出ていたので忘れないうちにフォローしておきたいですね。
最後にInferですが、やはり残念だという結論のようです…。
個人的には少なくともFalse Positiveは出てほしくないですねぇ。
ヒューリスティクスでなく理論的基礎がしっかりしているということに期待出来る/したいのはそこだと思うので。
次回
来年(2017)の2月に第1回を開催するみたいです。
私もネタはあるので体力があれば発表するかも知れません。
古の商用SML処理系MLWorksを動かす
2016年現在SMLの処理系はいくつもありますが、昔はMLWorksという商用の処理系がありました。
MLWorksは開発元のHarlequinが潰れて2000年くらいに姿を消していたのですが、突然2013年にオープンソースになりgithub上に公開されました。
実働していた頃は様々な環境で動作していたようですが、githubに公開当初は想定している動作環境自体が古すぎてビルド自体が困難な状態でした。現在ではellerhさんのおかげでLinux(x86)上でビルド;動作するようになっています。
ちょっとした修正を取り込んでもらってCentOS上での動作が確認できたので紹介します*1。
ちなみにこのHarlequinという会社、90年代後半の時点でMLで仕事してたのに加えてバージョン管理に内製のDVCSを使ったりしてたそうで楽しそうですね。(もう無いけど
ビルド
現在ではLinux上でsmlnjからbootstrapできます*2。
(大抵の人には)面倒な事にビルドにはlibXtとMotifが必要です。
$ git clone https://github.com/ellerh/mlworks.git $ cd mlworks mlworks$ git checkout --track origin/mono-array-slices # commit:75393c4 mlworks$ cd src mlworks/src$ make ARCH=I386 OS=Linux bootstrap
起動
今のところinstallターゲットはありません。
起動するには以下のようにします。
mlworks/src$ XUSERFILESEARCHPATH=app-defaults/MLWorks-mono LD_LIBRARY_PATH=rts/bin/I386/Linux/ rts/bin/I386/Linux/main-g -MLWpass xx -load images/I386/Linux/guib.img xx [-tty]
mainてファイル名はどうかと思う…。
`-tty` をつけて起動するとCUIのREPLが、付けずに起動するとMotifを使った対話環境が起動します。
ttyb.img を直接指定してもターミナル上で起動できます。
mlworks/src$ LD_LIBRARY_PATH=rts/bin/I386/Linux/ rts/bin/I386/Linux/main-g -MLWpass xx -load images/I386/Linux/ttyb.img xx MLWorks 2.1 Professional Edition Copyright (C) 1999 Harlequin Group plc. All rights reserved. MLWorks is a trademark of Harlequin Group plc. MLWorks> print "Hello, MLWorks!\n"; Hello, MLWorks! val it : unit = ()
以上
意外とあっさりREPLが動くので気が向いた人は触ってみましょう。
MLKitの謎のバグを修正してaobenchが動くようにした
AObench-SMLがSMLの処理系の一つであるMLKitに対応しました。
これまではMLKitにバグがあり、実数の指数表現リテラルのうち小文字の'e'を使ったもの(e.g. 2e3 10e~5 など)が使えませんでした。
単にレキサの規則が足りてなかっただけなんですが(基本的過ぎて)謎ですね。だれも気付かなかった…？
ま、ともかくこれの修正がマージされたのでmlkitでaobenchが動くようになりました！
自分で動かしてみたい方は、現時点でのMLKitの開発ヘッド(commit:1365653)以降でお試しください。
私の手元での実行結果を張っておきます。
動作環境は32bit Linuxです。
| 処理系 | real | user | sys |
|---|---|---|---|
| gcc | 0m3.846s | 0m3.846s | 0m0.006s |
| smlnj | 0m9.545s | 0m9.384s | 0m0.041s |
| mlton | 0m6.029s | 0m5.927s | 0m0.029s |
| mlkit | 0m26.194s | 0m25.850s | 0m0.037s |
| smlsharp2.0.0 | 0m31.322s | 0m30.846s | 0m0.089s |
| polyml | 0m12.467s | 0m12.062s | 0m0.261s |
注) SML#は更新できてないので2.0.0を使ってますがSML#の最新版は3.0.1です。
polymlが意外と健闘してるという印象ですが、mlkitはちょっと振るわないですねぇ。
配列を持ちまわってヘビーループで書き換えるベンチマークなのでメモリアロケート周りを工夫しているmlkitには不利なのかも知れません。
QCheckをSML#に対応させた
以前紹介したSML版QuickCheckであるところの QCheck を
SML#3.0.1で動作できるようにしてマージされましたヽ(ﾟｰﾟ*ヽ)(ﾉ*ﾟｰﾟ)ﾉ*1！！
そのマージに続いていくつか変更があって現在バージョンが v1.2 に上がっていますので今後はこれを使いましょう。
#どうでもいいけどREADMEにtravisバッジとか付いたら途端にそれらしく見えますよね
セットアップ
まずビルド方法ですが、これは make するだけです。
$ make -f Makefile.smlsharp
付属のBasisのテストも移植しました。
$ make -f Makefile.smlsharp test
恐らくString/from-toがいくつかfailしますが、これはBasisの仕様です(ﾟ∀ﾟ)。*2
使い方
QCheck のトップレベルのインターフェースファイル(qcheck.smi)を require します。
(* test.smi *) _require "basis.smi" _require "/path/to/qcheck.smi"
QCheck.checkGenを呼ぶコードを書きます。(コード例は前回と同じ)
(* test.sml *) structure Test = struct open QCheck (* 実装した(テストしたい)関数 *) fun succ x = x + 1 fun even x = x mod 2 = 0 fun odd x = x mod 2 = 1 (* 満たすべき性質 *) fun even_xor_odd x = even x <> odd x val int = (Gen.Int.int, SOME Int.toString) (* Check *) val _ = checkGen int ("even<>odd", pred even_xor_odd) end
後はリンクして実行するだけ。
$ smlsharp -I /path/to/qcheck.smi -o test test.smi $ ./test even<>odd..............ok (100 passed)
Infer Introduction
C言語の静的自動検証器である Infer の使い方がある程度分かってきたので紹介します。
Infer
Infer は、C言語(or [C++, Obj-C, Java])の検証器で、
自動で特定の種類のバグを発見してくれます。発見できるバグとして分かり易い例ではリソースリークを発見できます。
元々Inferを開発した会社をFacebookが買収してオープンソースになりました。(https://github.com/facebook/infer)
スマートフォン向けアプリの検証に使っているようです。
追記: 勘違いしてましたが C++サポートはこれからのようです。> https://github.com/facebook/infer/issues/24
Separation Logic(分離論理)
InferはSeparation logicという意味論に沿って静的検証を実行します。Separation logicというのは、Hoare logicを拡張した意味論で、共有された変更可能なデータやアドレスに対する算術演算を意味論で(うまく)扱うために考案されました。
適当に言えば「ポインタが扱える意味論」だと理解しています。(ものすごくいい加減な理解なので鵜呑みにしてはイケナイ)
適用例
実際的といえるかはかなり怪しいですが、aobench.c をそのままInferに渡してみたところ、2箇所のリークを見つけ修正しました。> aobench.cの修正
かなり簡単な例ですが、これくらいは全自動で見つかります。
Inferの使い方
Inferを使う最も単純な方法は、コンパイルのコマンドをそのまま infer コマンドに引き渡す方法です。
$ infer -- clang -c <input.c>
Makeを使っている場合は make コマンドごと引き渡すだけでよいです。
$ infer -- make
使用例
最も簡単な部類の使用例を示します。
// simple.c #include <stdlib.h> int main () { int * p = malloc(4); return 0; }
このコードをinferに渡す。
$ infer -- gcc simple.c Starting analysis (Infer version v0.8.0-44a6bf7) F. Analyzed 1 file Found 1 issue simple.c:4: error: MEMORY_LEAK memory dynamically allocated to p by call to malloc() at line 4, column 12 is not reachable after line 4, column 12 2. 3. int main () { 4. > int * p = malloc(4); 5. return 0; 6. } 7. Summary of the reports MEMORY_LEAK: 1
自明なバグですが、メモリリークが見つかってますね。
アノテーションの記述
以下のコードについて考えます。
// pass.c #include <stdio.h> #include <stdlib.h> int * new_int (int x) { int * p = malloc(sizeof(int)); if (p == NULL) exit(1); // (1) *p = x; // (2) return p; } int main () { int * p = new_int(42); printf("%d\n", *p); free(p); return 0; }
このコードには(Inferが報告する)バグはありません。
Inferが(1)のexitでプログラムが終了することを知っているため、(2)のデリファレンスが常に安全だと分かるからです。
しかし次のコードを見てください。
アロケーションに失敗した場合にライブラリ関数を呼び出して終了するコードです。
// ext.h // exit(3)のラッパー void lib_exit(int c); // ライブラリの提供する関数のシグネチャ // fail.c #include <stdio.h> #include <stdlib.h> #include "ext.h" int * new_int (int x) { int * p = malloc(sizeof(int)); if (p == NULL) lib_exit(1); // 終了することが分からない *p = x; return p; } int main () { int * p = new_int(42); printf("%d\n", *p); free(p); return 0; }
これを検証しようとすると…
$ infer -- gcc -c fail.c Starting analysis (Infer version v0.8.0-44a6bf7) F.. Analyzed 1 file Found 1 issue fail.c:9: error: NULL_DEREFERENCE pointer p last assigned on line 7 could be null and is dereferenced at line 9, column 2 7. int * p = malloc(sizeof(int)); 8. if (p == NULL) lib_exit(1); 9. > *p = x; 10. return p; 11. } 12. Summary of the reports NULL_DEREFERENCE: 1
NULL_DEREFERENCE バグが報告されました。
Inferには lib_exit の実装が見えないため、該当箇所のデリファレンスが安全だということが分かりません。
そこで以下のようにします。
// fail2pass.c #include <stdio.h> #include <stdlib.h> #include "ext.h" #include "infer_builtins.h" // (1) int * new_int (int x) { int * p = malloc(sizeof(int)); if (p == NULL) lib_exit(1); INFER_EXCLUDE_CONDITION(p == NULL); // (2) *p = x; return p; } int main () { int * p = new_int(42); printf("%d\n", *p); free(p); return 0; }
検証してみると…？
$ infer -- gcc -I ../../infer/models/c/src -c fail2pass.c Starting analysis (Infer version v0.8.0-44a6bf7) F.. Analyzed 1 file No issues found
エラーが無くなりました。
(1) で導入されるマクロ INFER_EXCLUDE_CONDITION を (2) で使用しています。
これは読んで字のごとく、指定した条件は「起きるはず無い(ので考えなくていいよ)」*1という指定です。
この指定によって Infer は p のNULLデリファレンスが起きないことが分かるので、エラーは報告されなくなります。
外部ライブラリを含むコードの検証
外部ライブラリを含むプロジェクトの場合も上の方法で Infer は正常に実行できますが、
コンパイラから実装が見えない(i.e. ヘッダしか見えない)関数が使用されている場合、それらの関数について必要な情報が得られないので、自明なバグでも発見できないことがあります。
ライブラリ関数を呼び出す箇所に INFER_EXCLUDE_CONDITION 等のアノテーションを書いてまわってもいいですが、冗長ですし、アノテーションの大半は通常の関数呼び出しとして提供されているため、実装コードと共存出来ない可能性があります。
これらの関数(e.g. 外部ライブラリの提供する関数)を使用するコードを検証するためには、
Infer が必要な性質が導出できるような関数の実装を(本物の実装とは)別に与える必要があります。この実装のことをモデルと呼びます。
標準(あるいは標準的な)ライブラリで提供される関数のモデルは Infer の一部として提供されており、/path/to/infer/infer/models/c/src/ 以下にあります。(これらは明示的な指定無しでもデフォルトで参照されます)
以下のようなコードを考えます。(ヘンな例ですいません…)
// extlib.h int getStatus (void); // uselib.c #include <stdio.h> #include <stdlib.h> #include "extlib.h" char const * stName (void) { switch (getStatus()) { case 0: return "St 0"; case 1: return "St 1"; case 2: return "St 2"; } return NULL; } int main () { char const * s = stName(); printf("%c\n", s[3]); return 0; }
$ infer -- gcc -c uselib.c Starting analysis (Infer version v0.8.0-44a6bf7) F.. Analyzed 1 file Found 1 issue uselib.c:17: error: NULL_DEREFERENCE pointer s last assigned on line 16 could be null and is dereferenced at line 17, column 17 15. int main () { 16. char * s = stName(); 17. > printf("%c\n", s[3]); 18. return 0; 19. } 20. Summary of the reports NULL_DEREFERENCE: 1
extlib で提供される getStatus 関数からは 0, 1, 2 のどれかの値しか戻りませんが、Infer には実装が見えないのでそれが分かりません。
そこで以下のようにモデルを与えます。
// mylib.c #include "extlib.h" // 本物のヘッダ #include "infer_builtins.h" int getStatus (void) { // 何が返って来るか知らない int s = __infer_nondet_int(); // けどとにかく !(s < 0 || 3 <= s) が成り立つよ INFER_EXCLUDE_CONDITION(s < 0 || 3 <= s); return s; }
モデルを解析。(infer/ 以下に解析結果が出力されます)*2
$ INFER_ANALYZE_MODELS=1 infer -o infer --models_mode --no_failures_allowed -- gcc -I ../../infer/models/c/src -c mylib.c
モデルの解析結果を参照して検証。
$ infer --specs-dir infer/specs -- gcc -c uselib.c Starting analysis (Infer version v0.8.0-44a6bf7) F.. Analyzed 1 file No issues found
エラーが出なくなりました(｀・ω・´)
このようにライブラリの提供する関数の性質を現すモデルを記述することで、より精度の高い静的解析が出来ます。
所感
Inferを使用するためには、対象とするコードにアノテーションの類を追加する必要がほぼ無いので簡単に利用できるように見えました。
が、外部ライブラリに依存しようとすると(つまり普通の開発として想定される状況だと)検証用のモデル(関数)を別ファイルで記述する必要があって、これが全く簡単ではないです((命題を直接書くわけではないから自明でもないし、ドキュメントも無い(#・∀・)))。
モデルはC言語で書く必要がありますが、
これは命題を直接書くわけではなくて、Inferが必要な命題を導出できるようなコードを書かないとイケナイ。これはとても迂遠に感じます。
ただし良さもあって、標準ライブラリの範囲(mallocとかfopen)か、あるいはモデルを記述してあれば単純なリソースリークを全自動で見つけてくれるのでお手軽ではあります。
他に、make に渡せばまともな規模のコードのビルド手順にも手を入れる必要が無いというのは良い点ですね。
まとめると、とりあえずmakefileだけ書いてあれば使用出来るので導入してみても良さそうです。
ただし外部ライブラリまで含めてまじめに検証したい場合は頑張ってモデルを記述する必要があるので、多少手間が掛かる。頑張れ。
インストール
LLVMのプラグイン(facebook-clang-plugins)を使用するので自分でビルドするのは時間が掛かりますが、
LLVMのバージョンに強く依存するので既存の環境を使わず、素直に全部ビルドした方がよさげです。
私は CentOS7 (x86_64) で動作を確認しています。
というか、おとなしく公式バイナリ http://fbinfer.com/docs/getting-started.html 使いましょう。
おまけ
文中で使用している INFER_EXCLUDE_CONDITION マクロですが、実装がちょっと面白いです。
#define INFER_EXCLUDE_CONDITION(cond) \ if (cond) \ while (1)
なるほどねー、という感じですよね。
無限ループはボトム(False？)(なのでその分岐は何も考えなくてよい)を体現してます。
ちなみに自分で同じマクロを書いてもちゃんと動作します。
