Hatena::ブログ(Diary)

::Eldesh a b = LEFT a | RIGHT b このページをアンテナに追加 RSSフィード Twitter

2017-07-17

ゼロから作るDeep Learningを読んだ

ゼロから作るDeep Learningを読み終わりました。おおよそ一ヶ月くらいかかりました。

機械学習自体(とpython)の全くの素人状態から読みましたが、とりあえず、単独で読み切れる本です。

その点は良いですね。


本全体を通して、MNISTと言われる手書き数字のデータセットを使って識別器を作っていきます。(と言っても形になるのはだいぶ後の方ですが。)


タイトルでは「ゼロから作る」と言ってますが、全部を作るとは言ってません。気をつけて下さい。

画像系のDeep Learningで重要になる(らしい)CNN説明は最後辺りの章で出てきますが、「バックプロパゲーションは自明だから(リポジトリ中の)コード読んどいてね。」という感じになっています。加えて重要なアルゴリズムである im2col についても同様の扱いです。

他に注意点として、関数の導入時点での実装が使用時点では使えないというケースがあります。これについては文中に注意書きがありますが、使えない実装を紹介されても困りますよね…。


あとはエラッタが多い印象です。出来るだけ新しい版を買った方がいいと思います。

(エラッタは公式のgithubリポジトリにまとまっています。)


まとめると、

  • 一人で読める
  • deep learningについて基本なことが平易に書いてある(気がする)
  • CNNについてはさほど丁寧じゃない
  • pythonは破綻した言語

2017-05-02

静的コード解析の会で停止性検証について発表してきた

静的コード解析の会#2でVeriFastによる停止性検証の導入の話をしてきました*1

本当は私自身も発表するほど分かってないのですが、それでも楽しい部分はあるので「これまで理解している内容を詰め込んでみた」という感じでまとめてみました。(前日深夜から突貫だったので超眠かった…)

今回の発表で伝わったかは怪しいですが、停止性のために最低限の機能を導入し、既存の機能を活かした仕組みはとても素晴らしいと思います。

楽しい部分を端的に挙げると、

  • 多重集合のある種の順序関係からどんどん「関数を呼ぶ権利」が出てくる
  • 関数の順序関係をコード上の大小関係で決めた

まぁこれだけ聞いても絶対分からないので、詳しく知りたい方はModular termination verificationを読みましょう。

振り返り

前回に引き続きVeriFastの話ですが、今回の内容は前回と比べて取っつきにくい内容でした。

理論的にも難しい割には、そもそも停止性なんて検証して何がうれしいのかから分かりづらいと思い、検証のモチベーションから始めています。

VeriFastでは動的束縛を伴う(=関数ポインタを使った)関数の相互再帰関数といった、かなり複雑な関数の停止性を検証することが出来ます。が、発表としては面白い具体例をほとんど出せなかったのは悔やまれるところです。

他の人の発表では @tanaka_akr さんのCoq2Cの話を聞き逃したのが残念でした…。

次回

このスライドでは序論といった範囲止まりですので、実際にC言語(あるいはJava)コードの停止性を検査するために覚えるべきことはもう少しあります。

次回はそのあたりまで理解して紹介できたらいいなぁという気持ちです。

あとは、今回の発表中から意図的に省いた単語として「整礎(関係|集合)」というモノがあるのですが、これは多重集合などと言うモノを持ち出した意味をはっきり述べるために必須の概念ですので、…勉強しておきます。はい。

2016-11-21

静的コード解析の会 第0回 でVeriFastについて発表してきた

#静的コード解析の会 第0回C言語(とJava)の検証器であるVeriFastについて発表してきました。

資料は公開してあるので興味ある人は見てください。動画もあります。

> https://metasepi.connpass.com/event/42141/presentation/

D

結構(私の理解が)きわどい質問も出ましたが、大体伝えたかった内容は伝わったんじゃないかと思います。

個人的には手ぶらで(ぐだぐだ)発表したProofSummit2016のリベンジでもあったので資料はかなり頑張って作りました。(内容は全然違いますが


本当に詳しく知りたい人は公式チュートリアル読むべきなのですが、これは結構ヘビーな量と内容です。これに対して私の発表は「忙しい人向けの入門」といった感じなのでお気軽にどうぞ(^^)

他の発表について

CSPというのを初めて知りました。プロセス代数というのは(多分大学生の時に)聞いたことはあったんですが、通信するプリミティブがあるなぁ、くらいのことしか分かりませんでした。

今になって説明を聞くと、多少理論的な話や記号が出てもビビらなくなったし、なんとなく理解できる部分も増えていたので嬉しみがありました(なお、日本語力は低下したもよう…)

あとCMLに似てますね(これは多分関係が逆だけど)。


自分がここ数年多少なりとも理論的な話として勉強してきた内容は、主に(型付き)ラムダ計算とその意味論だったので、実装でも仕様でもない(あるいはどちらにもなる?)ものと意味論を扱うというのは新鮮でした。


他には具体的に気になったものとしてトレース意味論というのが紹介されていました。これはプログラム副作用を形式的に扱う方面でも出てきてよく分からなかったんですが、CSPでの扱いはかなり明快だなという感じを受けました。(プロセス間の作用が初めから限定されているから当たり前か?

あとは「coinductive」という単語も出ていたので、それを持ち出す気持ちくらいは知りたいなという感じです。

気になるワードは他にも幾つか出ていたので忘れないうちにフォローしておきたいですね。


最後にInferですが、やはり残念だという結論のようです…。

個人的には少なくともFalse Positiveは出てほしくないですねぇ。

ヒューリスティクスでなく理論的基礎がしっかりしているということに期待出来る/したいのはそこだと思うので。

次回

来年(2017)の2月に第1回を開催するみたいです。

私もネタはあるので体力があれば発表するかも知れません。

2016-06-24

古の商用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` をつけて起動するとCUIREPLが、付けずに起動すると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が動くので気が向いた人は触ってみましょう。

*1:特にこれといった面白機能があるわけでは無さそうなんですが、まぁSML freakとしては動かさないわけにはいかないですよね

*2:手元ではsml/nj110.79で確認

2016-06-03

MLKitの謎のバグを修正してaobenchが動くようにした

AObench-SMLがSMLの処理系の一つであるMLKitに対応しました。

これまではMLKitにバグがあり、実数の指数表現リテラルのうち小文字の'e'を使ったもの(e.g. 2e3 10e~5 など)が使えませんでした。

単にレキサの規則が足りてなかっただけなんですが(基本的過ぎて)謎ですね。だれも気付かなかった…?


ま、ともかくこれの修正がマージされたのでmlkitでaobenchが動くようになりました!

自分で動かしてみたい方は、現時点でのMLKitの開発ヘッド(commit:1365653)以降でお試しください。


私の手元での実行結果を張っておきます。

動作環境は32bit Linuxです。

処理系realusersys
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.850s0m0.037s
smlsharp2.0.0 0m31.322s 0m30.846s0m0.089s
polyml 0m12.467s 0m12.062s0m0.261s

注) SML#は更新できてないので2.0.0を使ってますがSML#の最新版は3.0.1です。

polymlが意外と健闘してるという印象ですが、mlkitはちょっと振るわないですねぇ。

配列を持ちまわってヘビーループで書き換えるベンチマークなのでメモリアロケート周りを工夫しているmlkitには不利なのかも知れません。