Profile cover photo
Profile photo
Masahiro Sakai
813 followers
813 followers
About
Masahiro's posts

Post has attachment
ERATO MMSD キックオフワークショップ https://groups.google.com/forum/#!topic/sonoteno/87RUedFrmUU 気になりつつも結局行かなかったんだけど、資料とか公開されないのかなあ。

Takamasa Okudono さんの Generating Polynomial Interpolant with Semidefinite Programming (Numerical Optimization and Formal Methods) は、タイトルでググると別の人の論文 https://arxiv.org/abs/1302.4739 が引っかかるけど、内容的には関係する内容?


Post has attachment

Post has attachment
‪Earth mover's distance というのを教えてもらった。 https://en.wikipedia.org/wiki/Earth_mover%27s_distance 輸送問題はこんなことにも使われてるのね。‬

Post has attachment
ちょっと前に「Chainer: ビギナー向けチュートリアル Vol.1
http://qiita.com/mitmul/items/eccf4e0a84cb784ba84a をCPUで試したときにロスの謎の爆上げに遭遇してたのだけど、どうも https://twitter.com/akira_funahashi/status/875351714164953088 と同じくvecLibの問題だったっぽい。 その環境でnumpy.show_config()したら、vecLib使ってた…… しかし、闇だ……
Photo

Post has attachment
DeepXplore: Automated Whitebox Testing of Deep Learning Systems https://arxiv.org/abs/1705.06640 DNNのテストのために、複数のDNNで予測結果が異なる、もしくは各ニューロンが活性化したかどうかで定義されるニューロンカバレッジを増やすようなテストケースの生成を行うというもの。 「あるDNNだけ予測結果が異なる」ことと「まだ活性化したことのないニューロンが活性化する」ことの2つを組み合わせた目的関数で勾配法で最適化する(ただし、それだとあり得ない入力を生成してしまうので、勾配をそのまま適用する代わりにドメインの制約を反映した形に変更したうえで適用してる)。

DNNの振る舞いのコーナーケースを突くような入力の生成という意味では、敵対的サンプル(adversarial example)を生成などもあったが、敵対的サンプルではシードとなるサンプルから大きく変化させないためニューロンカバレッジの向上は限定的で、提案手法が敵対的サンプルやランダムサンプリングよりも優れているとのこと。 評価はMNIST, ImageNet, 自動運転, Contagio(PDFのマルウェア検知), Drebin(Androidのマルウェア検知)で実施。

比較対象として、ソフトウェアのコードカバレッジしか言及されていないけれど、ニューロンカバレッジの概念やこういったテスト手法は電子回路やFBDのテスト手法(自分の関わっていたものだと[1][2])にむしろ近い。

また、こういうテスト生成の観点でみると、バックプロパゲーションの情報を残しながら計算を行うのは、コンコリッック実行(concolic execution)とある意味で似ているなと思ったり。

Pythonコードのコードカバレッジとの比較はちょっとひどい。 Chainerとかならともかく、TensorFlowとKerasを使っているので、そりゃネットワークを定義するために基本的にはすべてのコードが実行されるに決まっている気がする。

他の応用としてデータセット中で間違ってラベル付けされているサンプルの検出みたいな話にもちょっと触れられている。 これは汚染されていないデータセットで学習したDNNと、汚染されたデータセットで学習したDNNで結果が異なるような入力をDeepXploreで求めて、それと類似度が高いサンプルを探すというもの。 汚染されていないデータセットで十分な学習ができているDNNがあるなら「単にそれを使えばいいじゃん」と思うわけで状況設定に疑問もあるけど、面白い。 例えば、Poisoning Attacks against Support Vector Machines [3] みたいな攻撃を実際に検出できると面白いかも。

しかし、こういうDNN自体を分析するメタなことをしようとすると、Tensorflowだとどうやればよいか自明だけど、Chainerだと結構悩ましい気がする。 「あるDNNだけ予測結果が異なる」方の目的関数は簡単だけど、ニューロンカバレッジの方の目的関数は、中間ノードが活性化済みかどうかを判断するためにノードの同一性を定義するのが自明ではないような(参考: On graph merging in Chainer visualization [4])

[1] "MC/DC-like Structural Coverage Criteria for Function Block Diagrams" http://dx.doi.org/10.1109/ICSTW.2014.27
[2] 「シーケンス制御プログラムのテストに適した新しいカバレッジ基準の提案」 http://id.nii.ac.jp/1001/00090467/
[3] "Poisoning Attacks against Support Vector Machines" http://arxiv.org/abs/1206.6389
[4] "On graph merging in Chainer visualization" https://www.youtube.com/watch?v=jOw0kJe3-vE


Post has attachment
ニューラルネットの学習で forward mode AD よりも reverse mode AD (back propagation) の方を使うのは何故かと思ったら Wikipedia に書いてあった。

「勾配を求める場合に必要なボトムアップ型自動微分の実行回数は入力変数の個数と等しく、トップダウン型自動微分では出力変数の個数に等しい。そのため、微分する関数f : ℝn → ℝm が m ≫ n を満たす場合、ボトムアップ型自動微分はトップダウン型自動微分よりも効率的である」
https://ja.wikipedia.org/wiki/%E8%87%AA%E5%8B%95%E5%BE%AE%E5%88%86

なるほど。

Post has attachment
http://profs.sci.univr.it/~farinelli/courses/ar/slides/paramodulation.pdf 自動定理証明で等号を扱うための推論規則であるParamodulationについての、分かりやすい説明。

Post has attachment
A Coalgebraic Paige-Tarjan Algorithm https://arxiv.org/abs/1705.08362 ここしばらく通勤中にずっと読んでた論文。 Paige-Tarjanの partition refinement アルゴリズムを、余代数で表現できる遷移系に一般化。

面白かったのだけど、同値関係 ≒ kernel や分割 ≒ regular epi を行き来する議論に不慣れで、ついていくのが中々大変で、だいぶ読むのに時間がかかってしまった。

あと、すごく一般化したアルゴリズムから初めて、高速化の工夫を入れて現実的なアルゴリズムにしてるのだけど、結局すべての工夫が入れられるのは実質的にラベル付き状態遷移系に帰着できる場合だけなので、だとしたら、ここまで一般的な話にしなくてもという気がしないでもない(いや、面白いんだけど)。


Post has attachment
SMT-COMP 2017 http://smtcomp.sourceforge.net/2017/ こっちもすっかり忘れてた…… ソルバの締切は延長されて6/7(anywhere on earth)だけど、むー

Post has attachment
MaxSAT Evaluation 2017 http://mse17.cs.helsinki.fi/ : 色々あったけど、結局主催者が代わって、今年も開催されることになったのね。 6/15日が締切と。 投稿出来るかな……?
Wait while more posts are being loaded