Blog

2016.9.23

ICFP及び関連イベント参加レポート – ICFP 1日目 –

κeenです。ICFPに参加するために奈良に来ています。これはICFP本体の1日目のレポートです。ICFP本体は内容が難しい上に過密スケジュールでメモの量がハンパなくてまとめるだけで苦労しました。

TensorFlow: Learning Functions at Scale

Talker: Martin Abadi

キーノートはGoogle BrainのMartinさんからDeep LearningとTensorFlowの話。 google brainについては g.co/brain や g.co/brainresidency を参照とのこと。 TensorFlowの紹介なので様々な話題がぽつぽつとある感じです。

関数型言語の人たちが集まっているのでまずはディープラーニング自体の説明から。ディープラーニングでやっていることはニューラルネットワークを作ってそれのパラメータチューニング。ただし"Gigantic network"になるよ、と。そして逆伝搬に最急降下法を使うので活性化関数は微分可能じゃないとダメだよね、など。

ディープラーニングの興味深い点は

様々な領域に適用出来る
ほとんど関数的な計算
ベースのアイディアは単純
単純なプリミティブを組み合わせて出来ている

など関数型とも共通する点も多いよね、と話していました。

ただ、難しいこともあって

学習データが必要
データ表現やアルゴリズムなどに関するベストプラクティスがない

などの歯痒い点もあります。

学習データについてですが学習の正しさは学習のゴールによって変わるというのも難しいところです。カメラからの映像が不思議なことに車の運転に作用する訳です。

そしてTensorFlowですが、

柔軟性
訓練と予測
研究と実用
複数のアプローチ
様々なプラットフォーム
パフォーマンス

を目標に作られています。

様々なプラットフォームについてですがGoogleはTPU(Tensor Processing Unit)というハードウェアをプロダクションで16ヶ月以上動かしていて、普段のGoogleの検索やAlphaGoの対戦などにも使われたようです。

アーキテクチャはC++やPythonのフロントエンドがあって、TensorFlowのコア実行システムが複数のCPUやTPUで動きます。

Python APIについては、Tensorの演算グラフを作るAPIとSession APIとがあります。

データフロー計算は
data = tensor
node = operation
の図式になっていて、データが次の演算を発火する形になっています。そして、逆伝搬に関しても自動で計算されます。

ディープというだけあって計算量が酷いのでデータフローを分散することもあります。データ自体はホストCPUが持っていて計算はTPUが行うなど。

CPU     | TPU
        |
data1 --|--+
        |  |
        | [Add]--+
        |  |     |
data2 --|--+   [Mul]-[Result]
        |        |      |
data3 --|--------+      |
        |               |
 -------|---------------+

CPU | TPU

data1 --|--+

| |

| [Add]--+

| | |

data2 --|--+ [Mul]-[Result]

| | |

data3 --|--------+ |

| |

-------|---------------+

この時、CPUとTPUの境界でsend/recvが発生します。

CPU           | TPU
              |
data1 --[send]|[recv]--+
              |        |
              |       [Add]--+
              |        |     |
data2 --[send]|[recv]--+   [Mul]-[Result]
              |              |      |
data3 --[send]|[recv]--------+      |
              |                     |
 -------[recv]|[send]---------------+

CPU | TPU

data1 --[send]|[recv]--+

| |

| [Add]--+

| | |

data2 --[send]|[recv]--+ [Mul]-[Result]

| | |

data3 --[send]|[recv]--------+ |

| |

-------[recv]|[send]---------------+

並列性についても重要で、2種類の並列性を提供します。

Graphの内部を分割して1処理を速くする
Graphを複数作って全体の処理を速くする

この時、Paremeter Serverなんかの出番もあります。

これを実現するには、データフローのスケジューリングなんかも必要です。

CPU     | TPU
        |
data1 --|--+
        |  |
        | [Add]--+
        |  |     |
data2 --|--+   [Mul]-[Result]
        |        |      |
data3 --|--------+      |
        |               |
 -------|---------------+

CPU | TPU

data1 --|--+

| |

| [Add]--+

| | |

data2 --|--+ [Mul]-[Result]

| | |

data3 --|--------+ |

| |

-------|---------------+

この時、どのデータをどの順番でいつTPUに読み込んだらいいかなんかも考える必要がある訳です。

さて、コントロールフローを作ることを考えましょう。RNNのように自己にループするものもあります。

実行モデルにフィットする
並列実行出来る
分散実行出来る
などなど

を考える必要があります。

ダイナミックデータフローのアーキテクチャについてですが、最も素朴に必要そうなプリミティブはSwitchとMergeですね。その他にも実行コンテキストとしてEnter, Exit, NextIterationなんかも必要です。

TensorFlowは逆伝搬もやってくれるという話がありましたが、コントロールフローの勾配を計算する必要が出てきます。条件式は和の公式で、While Loopは積の公式で微分することになります。また、計算が遅いので順方向の計算を再利用したりもするそうです。

ループを分散環境で実行する時に、テンソルの操作の部分だけを分散環境で実行していてはループの度にマスターノード相当のノードに終了条件などを訊きにいって遅くなってしまいます。なので、コントロールフローも分散ノードにコピーしてしまうなんかの話もありました。

さて、ここからはTensorFlowのコミュニティの話です。 TensorFlowは去年の11月に発表されましたが、他の機械学習ライブラリと比べてスターもフォークも圧倒的、2015年に最もフォークされたプロジェクトとなったそうです。

TensorFlowの話といえばきゅうり。

How a Japanese cucumber farmer is using deep learning and TensorFlow | Google Cloud Big Data and Machine Learning Blog | Google Cloud Platform

紹介ビデオを流そうとしましたが会場のWifiに繋がらず、座長の住井先生を"Eijiro Help!"と呼ぶ場面もありました。結局、ビデオは流せずに「きゅうりのビデオをYouTubeで見る」が会場への宿題として課されました（笑）。あとはぽつっときゅうりの分類って関数型だよね、など。

TensorFlow（というかDeep Learing）の使い道は関数だけに留まらず、例えば漢字の生成モデルだとかあるいは暗号だとかにも使えます。

さて、暗号の話について少し。ボブがアリスに暗号文を送りたいとします。でも、イブがその暗号文を盗聴しようとしているとします。そしてボブとアリスが共通鍵を持っているとします。

この時、ボブとアリスにとっては両者では暗号文が分かるようにしつつイブには分からないように、イブにとっては自分に暗号文が分かるようにしたいです。これらを目標にencrypt/decryptを学習します。

これの結果が少し面白くて、学習直後はアリスとボブで完全にコミュニケーションが出来ていて、イブも少し分かる状態になっています。そこから一瞬アリスとボブの間のコミュニケーションが壊れて、また元に戻りつつ、イブには完全に理解出来なくなっています。単調に精度が改善しない面白い例です。

因みに後で聞いたのですがこれは敵対的学習というそうです。

Farms, Pipes, Stream and Reforestation

Talker: Davide Castro University of St Andrews, UK
Paper: Farms, Pipes, Streams and Reforestation: Reasoning about Structured Parallel Processes using Types and Hylomorphisms

並列を型レベルでエンコードする話です。並列計算を抽象化したい、定式化して正しい変形などをしたいというのがモチベーション。

最初に導入としてParallel Farm(スレッドプール)、並列パイプライン、マージなどの並列計算で使われるツールを紹介します。

そして、並列計算のセマンティクスの等価性やSemantic Unification of StructuresをするためにParallelパターンを導入します。プログラムの変形前と変形後の等価性を調べるのに一旦parallelism erasureをして両者をsequencial programにして、program structureで比較したら出来そうだね、とのこと。

さて、プログラムの並列化ですが、分割統治が扱いやすいようです。分割にはanaを、統治にはcataを使います。つまり、hyloを使います。

さらに発展して、並列性を型レベルで表現しているようです(世界初)。

さて、この方法を使うとプログラムの機能を変えずに並列性を複数の方法で導入出来ますし、コストを見積ってあらかじめ評価することも出来ます。もうちょっというと、コストを見積れるということは自動的に最適な並列性を入れるようなことも可能な訳です。

将来的にはHaskellなんかで使えるようになるといいですね、とのことです。

Dag-Calculus: A Calculus for Parallel Computation

Talker: Umut Acar, Arthur Charguéraud, Mike Rainey, Filip Sieczkowski
Paper: Dag-Calculus: A Calculus for Parallel Computation

並列計算には複数のモデルがあります。fork-join, async-finish, futureなど。これらを統一するモデルはあるでしょうか？

fork join

function fib (n) (∗ Fibonacci with fork − join ∗)
    if n <= 1
    then n
    else let (x,y) = forkjoin (fib (n-1), fib (n-2))
         in x + y

function fib (n) (∗ Fibonacci with fork − join ∗)

if n <= 1

then n

else let (x,y) = forkjoin (fib (n-1), fib (n-2))

in x + y

async-finish

function fib (n) (∗ Fibonacci with async − finish ∗)
  if n <= 1
  then n
  else let (x,y) = (ref 0, ref 0)
  in finish {async (x := fib (n-1));
             async (y := fib (n-2)) };
     !x + !y

function fib (n) (∗ Fibonacci with async − finish ∗)

if n <= 1

then n

else let (x,y) = (ref 0, ref 0)

in finish {async (x := fib (n-1));

async (y := fib (n-2)) };

!x + !y

future

function fib (n) (∗ Fibonacci with futures ∗)
  if n <= 1
  then n
  else let (x,y) = (future fib (n-1), future fib (n-2))
       in (force x) + (force y)

function fib (n) (∗ Fibonacci with futures ∗)

if n <= 1

then n

else let (x,y) = (future fib (n-1), future fib (n-2))

in (force x) + (force y)

実は、futureだけ少しだけ違いがあります。fork-join, async-finishはそれぞれjoin, finishの所で両方の結果を待ち合わせているのに対して、Futureは最後に足し算する時に片方ずつ待ち合わせています。つまり、call tree(DAG)を考えた時に木(DAG)の育ち方に違いがあるのです。

この計算する時のDAGの辿り方をちゃんと定式化してあげようというのがベースとなるアイディアのよう。

計算の状態はDAGの頂点(V)、辺(E)、ミュータブルな共有状態(σ)を用いて(V, E, σ)と表わせます。

そしてDAGを構成するには5つの操作

newTd(e) – DAGの新しい頂点を作る
newEdge(e, e') – 新しいエッジを作る
release(e) eがスケジュール可能であることを伝える
self() 今いる頂点自身を返す
yield() 依存関係が解決されるまでスケジューリングから外す

そしてそれぞれの頂点は(N, R, X, F)、すなわち

N – 作られてすぐ
R – release された
X – 実行中
F – 終了した

があります。

さて、この体系を使ってfork-joinやasync-finish、futureを実装していました。

ということで中間言語なんかに丁度いい体系が出来ました、と。

A Lambda-Calculus Foundation for Universal Probabilistic Programming

Talker: Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, Marcin Szymczak
Paper: A Lambda-Calculus Foundation for Universal Probabilistic Programming

確率を体系に組み込んだ言語が欲しいというのがモチベーション。 CHURCH、ANGLICAN、VENTUREなどの確率を組み込んだ言語実装はありますが、それらの基礎となるべく型なしλ計算の操作的意味論に確率を組込みました。そしてそれを用いてtrace MCMC(マルコフ連鎖モンテカルロ)を定式化して正当性を証明しました。

やっていること自体はすごいのですが割と「詳細は論文で」的な内容なのと発表が情報を詰め込みすぎた早口のフランス人英語で聞き取れなかったのでまあ、論文を読んで下さい。

Deriving a Probability Density Calculator (Functional Pearl)

Talker: Wazim Mohammed Ismail, Chung-chieh Shan
Paper: Deriving a Probability Density Calculator (Functional Pearl)

これはFunctional Pearl、つまり複雑な問題を関数型で綺麗に解けたよ、という論文です。

この論文で扱っているのは確率分布とその確率密度の関係です。

不確実な問題に答えるのに確率分布は有用です。確率分布から期待値や密度関数が出てきます。複雑な確率分布も簡単な確率分布の組み合わせで表現出来ることがほとんどですが、そこから出てくる期待値や密度関数はそうなりません。残念ですよね。そこでプログラミングテクニックを使って確率分布を合成したら期待値や密度関数も一緒に出てくるような仕組みを考えたよ、というのが主旨。

そのテクニック雑に紹介します。考えるのは以下の言語です。

e = StdRandom | Lit x | Neg e | Log | Add e e
Lit :: Rational -> Expr Real
Neg :: Expr Real -> Expr Real
Log :: Expr Real -> Expr Real
Add :: Expr Real -> Expr Real -> Expr Real

e = StdRandom | Lit x | Neg e | Log | Add e e

Lit :: Rational -> Expr Real

Neg :: Expr Real -> Expr Real

Log :: Expr Real -> Expr Real

Add :: Expr Real -> Expr Real -> Expr Real

リテラル、負化、対数、可算があります。

これの期待値をこう定義してあげます。

expect:: Expr a -> (a -> Real) -> Real
expect StdRandom   _ c = ∫_0^1 λx.c x
expect (Lit x)     _ c = c (fromRational x)
expect (Neg e)     p c = expect e p (λx. c(negate x))
expect (Log e)     p c = expect e p (λx. c(log x))
expect (Add e1 e2) p c = expect e1 p (λx.
                         expect e2 p (λy. c(x+y)))

expect:: Expr a -> (a -> Real) -> Real

expect StdRandom _ c = ∫_0^1 λx.c x

expect (Lit x) _ c = c (fromRational x)

expect (Neg e) p c = expect e p (λx. c(negate x))

expect (Log e) p c = expect e p (λx. c(log x))

expect (Add e1 e2) p c = expect e1 p (λx.

expect e2 p (λy. c(x+y)))

まあ、なんかCPSですね。これでなんか上手いこと計算が出来るという寸法です。

論文には密度関数についてとか、応用とか色々書いてありますので詳しくはそちらを参照して下さい。

A New Verified Compiler Backend for CakeML

Talker: Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, Michael Norrish
Paper: A New Verified Compiler Backend for CakeML

はい。証明されたMLコンパイラとして有名なCakeMLのバージョン2.0のレポートです。テンション上がるやつですね。 big-stepスタイルでHOL4で形式化されています。

1.0の頃はとりあえず証明されてるブートストラップするコンパイラというだけでやや苦しい部分がったりターゲットアーキテクチャが1つだったりしましたが2.0ではバックエンドをガラっと書き換えて最適化の証明をしやすいようにし、バイナリ表現やターゲットも複数、さらにはFFIのサポートも入りました。

発表の内容はだいたい普通のコンパイラならやってそうなことをちゃんとやりましたというもの。SSAだとかレジスタ割り当てだとか。ただし全て健全性の証明つき。すごい。 End-to-Endで証明されているのでパーサからアセンブラ吐くところまで全て健全です。

今は覗き穴最適化だとかを入れようとしてたりv2.0でブートストラップしようとしてたり世代別GCを入れようとしてたりしているそうです。

因みに証明のしやすさとか作業の分割とかから12個の中間言語を使っているそうです。壮絶ですね。

Sequent Calculus as a Compiler Intermediate Language

Talker: Paul Downen, Luke Maurer, Zena M. Ariola, Simon Peyton Jones
Paper: Sequent Calculus as a Compiler Intermediate Language

多くのコンパイラの中間言語で使われるλ計算はカリーハワードで考えると自然演繹に対応します。自然演繹は数学者が頭の中で考えるのに便利ですが、形式的な証明はシーケントが便利です。

因みにシーケントはこういうやつですね。

------- (I)
A |- A
-------- (WL)
A, A -> A |- A
---------------- (->R)
A |- (A -> A) -> A
-------------------- (->R)
|- A -> (A -> A) -> A

------- (I)

A |- A

-------- (WL)

A, A -> A |- A

---------------- (->R)

A |- (A -> A) -> A

-------------------- (->R)

|- A -> (A -> A) -> A

では、シーケントの型側の対応はなんでしょう。シーケント計算です。実はシーケント計算もコンパイラの中間言語には向いてるというのが今回の話題。シーケントの |- の左が値で右が継続でって考えると丁度ラムダ計算とCPSの中間くらいの扱い心地になるそう。

で、GHCの中間言語で使われているCoreをシーケント計算にしたSequent Coreというのを作ったよというもの。もうちょっと言うと現在のCoreとSequent Coreをいったり来たり出来るようにしてそれぞれで向いている最適化をするようにしたというもの。 Coreはデータフローを扱うのに向いていてSequent Coreはdata-flowとcontrol-flowを対比します。

やはりここでもcase-of-caseのコントロールフローを問題にしているようです。ところでHaskellは遅延評価なので普通の関数呼び出しではスタックを消費せずにtail callになっていて、 case ... of に式が出てくると WHNFに評価するのでそこで初めてスタックを使うそう。だから case case ... of of のように case がネストするとtail callじゃなくなるとのこと。なるほど。そういう嬉しくないことが起こるところでさらに分岐が起きるからjoin point (SSAでいうphi node)がさらに問題になるんですね。

あとは継続って評価のコンテキストという意味とJoin Pointという意味と2つあるよねー、だとかCoreだと継続がなくてjoint pointの情報が落ちてしまうのでSequent Coreに直すときにそれっぽいのを復元するとかベンチマークとかの話をしてました。

Talker: Liam O’Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby Murray, Yutaka Nagashima, Thomas Sewell, Gerwin Klein
Paper: Refinement through Restraint: Bringing Down the Cost of Verification

seL4という証明されたマイクロカーネルなOSを引き合いに、継続的な開発のためにはコードを書く人にも検証する人にも優しいシステムプログラミング言語が必要だというのが導入。カーネルを開発したあとは10個くらいファイルシステム実装するけどそれも証明するの？って。証明というのはバグの他にセキュリティだとか最悪実行時間だとかそいうのも含まれます。

ということでシステムプログラミングがしやすい、つまりC FFIがあったりパフォーマンスが良かったりランタイムがない/安定していたりメモリアロケーションをプログラマが管理出来たりしていてかつ検証もしやすい、つまり定理証明器と統合されていてセマンティクスが検証しやすくて simp で証明出来るくらい単純で無駄なランタイムのない言語って欲しいよね。Cogentっていうやつを作りました、と。

Cogentは関数は全て全関数でメモリ安全で純粋関数型でHOLへのShallow embeddingと破壊的変更をするCのコードの両方を吐けてC FFIがあってparametric polymorphismがあってランタイムのない言語です。

さて、純粋関数型なのに破壊的変更とはこれいかに？という感じですが一意型の場合にそういう最適化をしているようですね。

因みにパフォーマンスは良好なよう。

将来的にはメモリ管理に便利なリージョンだとか検証に便利な依存型だとかrefinement型だとか並行だとかを入れたいとのこと。

因みに質問ではRustについてどう思う？って飛んできてました。やっぱり安全な言語でありかつ証明器へのshallow embeddingが出来るというのが効いているよう。

Fully Abstract Compilation via Universal Embedding

Talker: Max New, William J. Bowman, Amal Ahmed
Paper: Fully abstract compilation via universal embedding

Abstract Compilationというのが分からなかったので置いてけぼりにされたやつ。

どうやらソース言語からターゲット言語への変換で振舞いを変えないのがAbstract Compilationとのこと。ソースコード上はそういう振舞いをしない筈だけどバイナリになるとよく分からん挙動が追加されてそこがセキュリティホールになるみたいなことがないとのこと。あるいはリファクタリングみたいな仕様を変えたくない変換だとか。

さて、コンパイラがFully Abstractなことを証明するのは一筋縄ではいかなくて、例えばMLからアセンブラにコンパイルした時にアセンブラにはgotoがありますがそれがちゃんともとのMLに戻せることを証明しないといけません。が、この論文では例外のない言語から例外のある言語へのコンパイラがFully Abstractであることを証明したとのこと。あとはclosure translationとかも。

私は発表聞いてもよく分からなかったので興味のある方は論文読んで下さい。

Oh Lord, Please Don’t Let Contracts Be Misunderstood (Functional Pearl)

Talker: Christos Dimoulas, Max New, Robby Findler, Matthias Felleisen
Paper: Oh Lord, please don’t let contracts be misunderstood (functional pearl)

なんか契約プログラミングは特に関数型の人たちに誤解されてる！けしからん！ってやつ。

誤解以前に契約プログラミングについてそこまで知らないのでよく分からなかった。

A Type Theory for Incremental Computational Complexity with Control Flow Changes

Talker: Ezgi Çiçek, Zoe Paraskevopoulou, Deepak Garg
Paper: A type theory for incremental computational complexity with control flow changes

例えばエディタのシンタックスハイライトだとかの入力がちょっとずつ変わる計算では前回との入力の差分を処理するのが賢いやり方です。じゃあ、Incrementalにやった時のコストはどのくらいになるの？というので先行研究としてCostItというのがあったそうですが、Control-Flowを変更出来ないだとかの制約があったのでその制約をとっぱらったDuCostItというのを作ったというのがこの論文。

あ、コストの話を型システムでやるんだ、って感じ。

Compact Bit Encoding Schemes for Simply-Typed Lambda-Terms

Talker: Kotaro Takeda, Naoki Kobayashi, Kazuya Yaguchi, Ayumi Shinohara
Paper: Compact bit encoding schemes for simply-typed lambda-terms

東大小林先生の発表。λ項をビット列にエンコードする時の賢いやり方の話。 ~~因みに後で小林研の人に聞いたら特にモチベーションがある訳ではなくて今のところ面白いよねーくらいのものとのこと。~~ 2016-09-24 12:03:44訂正: モチベーションがないという点は誤りでした。公開モデル検査をするための「高階圧縮」からきているとのこと。ただ、まだリアルなデータを圧縮するまではいっていないので「面白いよねーくらい」とのことです。/訂正

雑にいうとネストした項を一旦シーケンスに変換した後型情報を全体のメタデータにしてあげればそれで一意にデコード出来るようになるのでシーケンス自体のエンコードが短かくなるというもの。メタデータ自体の大きさは？というと例え何百万とλ項があってもカインドはそんなに多くないので膨れ上がらないという仮定の元に作られているとのこと。

Queueing and Glueing for Optimal Partitioning (Functional Pearl)

Talker: Shin-Cheng Mu, Yu-Hsi Chiang, Yu-Han Lyu
Paper: Queueing and glueing for optimal partitioning (functional pearl)

ある性質を満たす最適分割を線型時間で求める綺麗なやり方を見付けたよ、という素晴しいPearl。

例えば、6つのジョブがあって、それらを何回かに分けて分割したいとします。そしてコストの計算はうんたらかんたらでとかいった問題が解けます。

なんか1つ1つQueueingして「ここで分けることは無さそうだろう」って思ったらそこはGlueingして、っていうのをやっていくアルゴリズムです。

スライドは図で非常に分かりやすかったのですがここにその図を貼れないのと論文に図が載っていないので厳しいと思いますが興味のある方は読んでみて下さい。

因みに「関数プログラミング珠玉のアルゴリズムデザイン」の訳者の山下先生が本に追記しようかって言ってました。良いですね。

All Sorts of Permutations (Functional Pearl)

Talker: Jan Christiansen, Nikita Danilenko, Sandra Dylus
Paper: All sorts of permutations (functional pearl)

type ND a = [a]
filterND :: (a -> ND Bool) -> [a] -> ND [a]

1 2	type ND a = [a] filterND :: (a -> ND Bool) -> [a] -> ND [a]

という非決定性計算を考えた時に、あるリストの全てのサブリストを得る操作は

sublists :: [a] -> [[a]]
sublists = filterND (const [True, False])

1 2	sublists :: [a] -> [[a]] sublists = filterND (const [True, False])

で書けてしまいます。じゃあ、あるリストの全ての並べ替え(permutation)は？ sortND に [True, False] を返す比較関数を渡せば出来そうな気がしませんか？

実は少し問題があって、ソート(sort)アルゴリズム毎に微妙に性質が違ったりします。そこの解析とあとはNDをモナドに発展させたよ、という話。

タイトルが良い感じの洒落ですね。

最後に

1日目で割とぐったりきましたがまだまだICFPは続きます。

Author

admin