- yoshihiro503
- 1956
- 6
- 1
- 0
「Spark, TensarFlowとか向けの中間言語であるNVL(Nested Vector Language)というのを開発中で、それのCoq版を証明した」 #ProofSummit2016
2016-09-25 13:43:34NVL:Spark、TensorFlowなどの中間言語になるように作られている。これのCoq版を作る #ProofSummit2016
2016-09-25 13:43:37行列とベクトルかけて定数ベクトル加えたのに関数かますのがSingle Layer Neural Network #ProofSummit2016
2016-09-25 13:51:24「x |-> ρ(Wx + l) (Wはmn行列、lはm次元ベクトル)というカタチのR^n -> R^nの関数をsingle layerとする。こういうカタチの関数で欲しい関数を近似する」 #ProofSummit2016
2016-09-25 13:55:57「関数ρは誰かが最初にヒューリスティックに決める。例えばtanhとか」 #ProofSummit2016
2016-09-25 13:57:48「CoqライブラリFiatというのがある。最新版は一般人には見えない」 #ProofSummit2016 #Coq #Fiat
2016-09-25 14:03:55「Fiatというのは仕様を書いて、そこからプログラムを作っていくというのをサポートする」 #ProofSummit2016
2016-09-25 14:04:48「例: is_grad (f f': R->R) : Prop のとき Definition grad (f: R->R): Comp(R->R) := {f' | is_grad f f'}%comp. のように書ける」 #ProofSummit2016 #Fiat #coq
2016-09-25 14:08:06Comp(R->R)で「今は断言できないけどR->Rの関数と置く」ような記述? #ProofSummit2016
2016-09-25 14:08:10値はsigとそっくりの書き方をする(%compとして文脈を指定する必要がある) #ProofSummit2016
2016-09-25 14:08:53Compの値はComp内では取り出せる。連鎖的に生成する感じか?記法はモナドのdo記法に似てるような・・・ #Proofsummit2016
2016-09-25 14:11:20これ普通にMaybe, computation, powersetモナドあたりにしか見えない #ProofSummit2016
2016-09-25 14:12:46