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