2017-02-13

数理論理学：ノート4

本読み数理論理学

読んでいる本（出典）：数理論理学 | 戸次大介 |本 | 通販 | Amazon

前回：ノート3 ／次回：まだ
目次：数理論理学

以下、第5章後半の自分の理解。
最後の節（標準形）がまだ読めていないので、後でこの記事に加筆するか、新しい記事にまとめる。

前回までのあらすじ（一階述語論理の統語論）

命題論理では扱えない「すべての $x$ について～」「ある $x$ が存在して～」のような知見を表現すべく、論理式を名前と述語に分けます。
$\forall$ や $\exists$ といった量化子を導入します。
論理式がすごい増えてしまいそうですが、自然数で番号付けできます（ゲーデル数）。
- 但し、論理式のパーツになる記号の集合 $\mathcal{A}$ は高々可算集合とする。

一階述語論理の意味論

命題論理のときと同様、「論理式の集合真偽の領域」であるような解釈を考える。
命題論理のときは、は「原子命題の真偽の組合せの全パターン」ということで原子命題の数個あった。
一方、一階述語論理では原子命題がさらに項と述語に分かれるので、「各項が指し示しているもの」「各述語について、項が指し示しているものに対応する、論理式の真偽」として考えるのがよい（構造）。
あと変項もあるので、変項に何を割り当てたかも論理式の真偽にかかわる（割り当て ）。
つまり、ある1つの解釈を与えるには、以下を完全に決めればよい。
- そもそもどんなものたちについて命題を述べるのか（存在物）の集合： $D_M$
- 名前記号が指す存在物は何か： $F_M : \{ a_1, a_2, \cdots \} \to D_M$
- $n$ 個の存在物に $n$ 項演算子を適用したときに指す存在物は何か： $F_M : \{ o_{n,1}, o_{n,2}, \cdots \} \to {D_M}^{{D_M}^n}$
- $n$ 個の存在物に $n$ 項述語を適用したときの真偽はどうか： $F_M : \{ \theta_{n,1}, \theta_{n,2}, \cdots \} \to {D_t}^{{D_M}^n}$
- 変項に何を割り当てたか： $g : \{\xi_1 , \xi_2, \cdots \} \to D_M$

Ex．あるゲームのキャラクターたちについて命題を述べるとする（以下、ネタバレな上にしようもない例）。

　　 $M_1$ をダンガンロンパのキャラクターの構造とすると、 $D_{M_1}=\{$ 苗木誠, 舞園さやか, 桑田怜恩, $\cdots \}$ 。
　　名前記号から存在物への対応付けは例えば、 $F_{M_1}(a_1)=$ 苗木誠 , $F_{M_1}(a_2)=$ 舞園さやか , $\cdots$ 。
　　例えば $o_{1,1}(\tau_1)$ が「 $\tau_1$ を殺した犯人」のような1項演算子なら、 $F_{M_1}(o_{1,1})($ 舞園さやか $) =$ 桑田怜恩。
　　例えば $\theta_{2,1}(\tau_1, \tau_2)$ が「 $\tau_1$ は $\tau_2$ を殺した」のような2項述語なら、 $F_{M_1}(\theta_{2,1})($ 苗木誠, 舞園さやか $) = 0$ 。
　　このように、各名前記号が指す存在物、各 $n$ 項演算子が指す存在物（項が指す存在物による）、各 $n$ 項述語の
　　真偽（項が指す存在物による）を完全に決めれば、この論理体系のすべての基本述語の真偽は完全に決まる。

　　※ ここで、「桑田怜恩が舞園さやかを殺したから $F_{M_1}(o_{1,1})($ 舞園さやか $) =$ 桑田怜恩」ということではなく、
　　　あくまで $o_{1,1}(\tau_1)$ という1項演算子をこの写像で定義したということに注意。
　　※ ただ、 $o_{1,1}(\tau_1)$ が本当に「 $\tau_1$ を殺した犯人」になるように定義されていて、 $\theta_{2,1}(\tau_1, \tau_2)$ が本当に「 $\tau_1$ が
　　　 $\tau_2$ を殺した」かどうかを表すように定義されているなら、 $\theta_{2,1}(o_{1,1}(\tau_1), \tau_1)$ はどの解釈でも真になりそう。
　　　殺されていないキャラクターを代入したときの取り扱いは適切にする必要があるけど。

　　他方、別の解釈の下では、論理体系にはスーパーダンガンロンパ2のキャラクターの構造 $M_2$ が当てはめられて
　　いるかもしれない。 $D_{M_2}=\{$ 日向創, 七海千秋, $\cdots \}$ 。
　　この場合の名前記号の対応付けは例えば、 $F_{M_2}(a_1)=$ 日向創 , $F_{M_2}(a_2)=$ 七海千秋 , $\cdots$ かもしれない。

量化論理式の真偽を解釈するには、への割り当てをすべての存在物に変異させる（というより、これがという論理式の定義そのものである）。
- $\langle M, g \rangle (\forall \xi \varphi)=1 \; \Longleftrightarrow \;$ すべての $a \in D_M$ について $\langle M, g \rangle [ \xi \mapsto a] (\varphi) = 1$ である．
- $\langle M, g \rangle (\exists \xi \varphi)=1 \; \Longleftrightarrow \; \langle M, g \rangle [ \xi \mapsto a] (\varphi) = 1$ となる $a \in D_M$ が存在する．
解釈について、以下が成り立つ。
- その変項が項／論理式の自由変項でないなら、その変項を変異させても項が指す存在物／論理式の真偽は変わらない。
- 項／論理式の変項にある項を代入した上で解釈しても、解釈の割り当ての変異によって変項をある項に変えても、どちらの場合も項が指す存在物／論理式の真偽は変わらない。
- 項 $\tau_1$ と $\tau_2$ が指す存在物が同じなら、項／論理式の変項を $\tau_1$ に変異させても $\tau_2$ に変異させても項が指す存在物／論理式の真偽は変わらない（外延性）。

一階述語論理における妥当な推論

意味論的含意の概念は一階命題論理のときと同じ。
量化論理式が推論の前提 or 帰結になる場合に色々な定理が成り立つ。

練習問題5.48
$n$ 項述語に渡せる項のセットのパターン数は、 $|D_M|^n$ パターンある。
それぞれのパターンが1か0を取りうるので $n$ 項述語は $2^{|D_M|^n}$ 種類ありうる。
例えば、 $D_M =\{A_1, A_2\}$ で、 $n=2$ だったら、 $2$ 項述語 $\theta_{2, i}$ は16種類ある。

$\tau_1$	$\tau_2$	$\theta_{2,1}$	$\theta_{2,2}$	$\theta_{2,3}$	$\theta_{2,4}$	$\theta_{2,5}$	$\theta_{2,6}$	$\theta_{2,7}$	$\theta_{2,8}$	$\theta_{2,9}$	$\theta_{2,10}$	$\theta_{2,11}$	$\theta_{2,12}$	$\theta_{2,13}$	$\theta_{2,14}$	$\theta_{2,15}$	$\theta_{2,16}$
$A_1$	$A_1$	1	1	1	1	1	1	1	1	0	0	0	0	0	0	0	0
$A_1$	$A_2$	1	1	1	1	0	0	0	0	1	1	1	1	0	0	0	0
$A_2$	$A_1$	1	1	0	0	1	1	0	0	1	1	0	0	1	1	0	0
$A_2$	$A_2$	1	0	1	0	1	0	1	0	1	0	1	0	1	0	1	0

練習問題5.55

「奇数の二乗は奇数である」は真だが、 $\forall x ($ 奇数 $(x) \; \land$ 奇数 $(x \times x) \, )$ は、 $x$ に例えば $2$ を割り当てたとき偽。
「二乗が奇数であるような奇数が存在する」は真で、 $\exists x ($ 奇数 $(x) \to$ 奇数 $(x \times x) \, )$ も真だが、前者は $2$ を割り当てると偽で、後者は $2$ を割り当てても真（というか後者はどんな数を割り当てても真）。

練習問題5.58　面倒なので略。

練習問題5.60　面倒なので略。

練習問題5.62　面倒なので略。

練習問題5.65　面倒なので略。

練習問題5.82　面倒なので略。

練習問題5.84　面倒なので略。

練習問題5.86　面倒なので略。

練習問題5.88　面倒なので略。

練習問題5.90　面倒なので略。

練習問題5.91
$\forall x (F(x)) \land G(a) = \! \! \! | | \! \! \! = \forall x (\lnot \lnot F(x)) \land G(a)$ を証明するには、二重否定律より $F(x) = \! \! \! | | \! \! \! = \lnot \lnot F(x)$ なので、これに量化論理式の置き換えを用いて $\forall x (F(x)) = \! \! \! | | \! \! \! = \forall x (\lnot \lnot F(x))$ 。これと $G(a) = \! \! \! | | \! \! \! = G(a)$ に対し複合論理式の置き換えを適用。

所感

「 $x$ は哺乳類である」「 $x$ は卵生である」の変項 $x$ に「友達の鈴木君」を割り当てる（98ページ）：確かに友達の鈴木君は哺乳類だし、卵生ではないけど、鈴木君的には友達からの扱いが「哺乳類の一個体」でいいのだろうか…。
集合における外延性は、「集合はそれが含む要素によって一意に定まる」。外延性の公理 - Wikipedia
一階述語論理の解釈の外延性（定理5.64）は、「論理式の真偽は項が指す存在物によって一意に定まる」。当たり前に感じられすぎてよくわからない。「定義されたこと以外は知らないふりをする《知らないふりゲーム》」（数学ガールゲーデルの不完全性定理の31ページ）は、こと「ある論理式が真か偽か」については経験がありすぎるので難しい。
ラムダ計算（114ページ）って何。
- ラムダ計算 - Wikipedia

2017-01-19

入門機械学習による異常検知―Rによる実践ガイド：ノート2

本読み機械学習

読んでいる本（出典）：入門機械学習による異常検知―Rによる実践ガイド | 井手剛 |本 | 通販 | Amazon

前回：ノート1 ／次回：ノート3
目次：入門機械学習による異常検知―Rによる実践ガイド

読んだページ： 23～44ページ
以下、メモと雑談。

前回までのあらすじ

観測値の異常度は、正常なデータ群の分布に対する対数尤度で測るよ。
- 例．サイコロを10回ふって出た目の和が20以下か50以上になる確率は1%未満なので、もしサイコロをふった結果そうなってしまったらあまり尤もらしくなく、異常なのではないか（サイコロかあなたが）。
異常度の閾値をどう設定するべきかについて、観測データが i.i.d. に正規分布にしたがうなら、異常度が F 分布にしたがうよ（ホテリング理論）。
- 例．東京の2017年1月1日～18日の日ごとの平均気温は以下だった。気象庁｜過去の気象データ検索
  x <- c(7.4, 7.2, 8.0, 8.5, 6.7, 4.5, 4.1, 3.9, 7.2, 8.1, 6.9, 6.0, 6.2, 2.4, 0.7, 3.2, 5.4, 5.8)
  もし1月19日の平均気温が0℃だったら異常なのかどうか考える。日ごとの平均気温が i.i.d. に正規分布にしたがうと仮定するのは気象学的には駄目かもしれないけど、ここではいいことにして、「1% も起こりそうにないこと」を異常とみなすなら、0.30℃未満か 11.06℃超が異常になる。つまり、1月19日の平均気温が0℃なら異常である。
  > qnorm(mean=mean(x), sd=sqrt(var(x)*(18-1)/18), 0.005)
  [1] 0.2975372
  > qnorm(mean=mean(x), sd=sqrt(var(x)*(18-1)/18), 0.995)
  [1] 11.05802
  ただ、上の議論では、「1月1日～18日の平均気温は正規分布から歪んでいなかったのか」が考慮されていない。そもそも18点しかサンプルがないなら、平均や分散の推定値には区間幅があるだろう。それも考慮すれば、 $(x' - \hat{\mu})^2 / \hat{\sigma}^2 \sim (N+1)/(N-1) \cdot \mathcal{F}(1, N-1)$ が成り立つので（ホテリング理論）、以下のように正常と判定される範囲が少し広がり、-0.72℃未満か 12.08℃超が異常になる。つまり、1月19日の平均気温が0℃ならぎりぎり異常ではない。あまり0℃になってほしくはないけど。
  > F_0.01 <- qf(df1=1, df2=18-1, 0.99)
  > F_0.01
  [1] 8.39974
  > mean(x) - sqrt(var(x) * (18+1) / 18 * F_0.01)
  [1] -0.7220735
  > mean(x) + sqrt(var(x) * (18+1) / 18 * F_0.01)
  [1] 12.07763
  なお、各日の異常度とF分布上側1%の閾値ラインをプロットすると以下。1月1日～18日の平均気温に異常値はなかった。15日の日曜日は特に寒かったけど、異常ラインに達するほどではなかった。
- 1変数のホテリング理論の証明（26～36ページ）について。
  - 定理2.3（30ページ）は以下でも示せる。
    正規分布の二乗和がカイ二乗分布に従うことの証明 | 高校数学の美しい物語
  - 式2.26（33ページ）の ${\rm H}_N$ について、 ${\rm H}_N = {\rm H}_N^{\rm T}$ かつ ${\rm H}_N^2 = {\rm H}_N$ に注意。
  - 定理2.5（35ページ）を、教科書のやり方を追っていないけど自分でやってみる。
    $x \sim \chi^2(m, a), \; y \sim \chi^2(n, b)$ のとき、 $\displaystyle z \equiv \frac{x/(am)}{y/(bn)} \sim \mathcal{F}(m, n)$ を示せ。
    とりあえず分布の式をちゃんと書いておく。
    $\displaystyle f_X(x) = \frac{1}{2a \Gamma (m/2)} \left( \frac{x}{2a} \right) ^{m/2 -1} \exp \left( -\frac{x}{2a} \right)$
    $\displaystyle f_Y(y) = \frac{1}{2b \Gamma (n/2)} \left( \frac{y}{2b} \right) ^{n/2 -1} \exp \left( -\frac{y}{2b} \right)$
    $\displaystyle f_Z(z) = \frac{\Gamma (m/2 + n/2)}{\Gamma(m/2) \Gamma(n/2)} \left( \frac{m}{n} \right) ^{m/2} z^{m/2 - 1} \left( 1 + \frac{mz}{n} \right) ^{-(m+n)/2}$
    $w=y, \; z=bnx/(amy)$ に変数変換する。 $x = amwz/(bn), y = w$ のヤコビアンは、
    $\displaystyle J(w, z) = \begin{vmatrix} amz/(bn) & amw/(bn) \\ 1 & 0 \end{vmatrix} = -\frac{amw}{bn}$
    $w, \; z$ の同時確率密度関数は、統計検定の教科書の22ページより、
    $f_{WZ}(w, z) = f_{XY}\bigl( amwz/(bn), \; w \bigr) \bigl| J(w, z) \bigr|$
    　　　　　 $\; \displaystyle = \frac{1}{2a \Gamma (m/2)} \left( \frac{mwz}{2bn} \right) ^{m/2 -1} \exp \left( -\frac{mwz}{2bn} \right) \cdot \frac{1}{2b \Gamma (n/2)} \left( \frac{w}{2b} \right) ^{n/2 -1} \exp \left( -\frac{w}{2b} \right) \cdot \frac{amw}{bn}$
    　　　　　 $\; \displaystyle = \frac{z^{m/2 -1}}{2b \Gamma (m/2) \Gamma (n/2)} \left( \frac{m}{n} \right) ^{m/2} \left( \frac{w}{2b} \right) ^{(m+n)/2 - 1} \exp \left( -\frac{w}{2b} \bigl( \frac{mz}{n} + 1 \bigr) \right)$
    $z$ の分布を出すには、これを $w$ について積分して周辺化すればよい。
    $\displaystyle f_Z(z) = \int_0^{\infty} dw f_{WZ}(w, z)$
    　　　 $\displaystyle \, = \frac{z^{m/2 -1}}{2b \Gamma (m/2) \Gamma (n/2)} \left( \frac{m}{n} \right) ^{m/2} \int_0^{\infty} dw \left( \frac{w}{2b} \right) ^{(m+n)/2 - 1} \exp \left( -\frac{w}{2b} \bigl( \frac{mz}{n} + 1 \bigr) \right)$
    　　　 $\displaystyle \, = \frac{z^{m/2 -1}}{\Gamma (m/2) \Gamma (n/2)} \left( \frac{m}{n} \right) ^{m/2} \left( 1 + \frac{mz}{n} \right) ^{-(m+n)/2} \int_0^{\infty} dt \cdot t ^{(m+n)/2 - 1} \exp (-t)$
    　　　 $\displaystyle \, = \frac{\Gamma (m/2 + n/2)}{\Gamma(m/2) \Gamma(n/2)} \left( \frac{m}{n} \right) ^{m/2} z^{m/2 - 1} \left( 1 + \frac{mz}{n} \right) ^{-(m+n)/2}$
    なんかちゃんと出たからこれでいいや。

今回のお話

データが多次元正規分布にしたがう場合も、同様にで異常度を定義できる。
- これもマハラノビス距離の2乗。雑記 - クッキーの日記
- 例．東京の2017年1月1日～18日の最低／最高気温は以下だった。気象庁｜過去の気象データ検索
  x1 <- c(2.0, 3.8, 3.5, 3.6, 3.7, 1.5, 0.1, 1.6, 3.8, 3.5, 3.9, 0.7, 1.4, -1.3, -2.3, -2.0, 0.7, 1.1)
  x2 <- c(13.8, 13.3, 13.7, 14.0, 10.4, 8.8, 8.7, 6.0, 11.1, 12.7, 11.0, 12.1, 12.7, 6.3, 4.7, 8.0, 10.9, 10.3)
  どの日が異常っぽいというか、あまりまとまっていない…。
  
  とりあえず各日の異常度を求める。
  mu <- colMeans(cbind(x1, x2))
  xc <- cbind(x1, x2) - matrix(1, 18, 1) %*% mu
  sigma <- t(xc) %*% xc / 18
  a <- rowSums( (xc %*% solve(sigma) ) * xc)
  a <- a * (18 - 2) / ((18 + 1) * 2)
  th <- qf(df1=2, df2=18-2, 0.99)
  案の定、1%基準で異常ラインに達した日はなかった。特に寒かった15日よりも、上図においてデータ点が対角線から離れ気味の（最低気温と最高気温の差が他の日付に比べてかなり小さい）8日の方が異常度が微妙に大きかった。

2017-01-18

ゼロから作るDeep Learning：読了メモ

本読み深層学習

とてもわかりやすいという巷の評判に流されてこの本を読みました。

ゼロから作るDeep Learning ―Pythonで学ぶディープラーニングの理論と実装
斎藤康毅

オライリージャパン 2016-09-24
売り上げランキング : 58

Amazonで詳しく見る by G-Tools

一貫して読み手の理解を考慮して書かれたすばらしい本だと思います（その分トピックは絞られていますが）。
1章だけではなく最後まで・隅々までそれをやり切っている本というのが実はあまりないと思います。
モデルや手法の義務的な紹介にはなっておらず、伝えるべき心にたくさんページを割いていると思います。
これから深層学習を学ぶ人、ライブラリをつかうのでゼロから作るつもりはないという場合も、よほど中身はどうでもいい主義者でない限りよい本と思います。数式が苦手でない人には易しすぎると感じられる面もあるでしょうが、他のオムニバス本を読み解くより時短で要点を抑えられると思います。
説明が丁寧な分、CNN の話はありますが、RNN / 自己符号化器 / 制限ボルツマンマシンはありません（最終章に言葉のみ）。

以下、読んでいていいなあと思った箇所や自分なりの補足のメモです。

各章末にまとめ（「本章で学んだこと」）があり、各章の位置付けがわかりやすい。
要所要所で、そのアルゴリズムは全体図としてどんなステップからなるか確認している。
本のサブタイトルに「理論と『実装』」とあるように、実装する上での数値誤差等の注意・対策も抜かりない。実装が切り離されずすぐ傍にあるので、理論が一層理解しやすい。
まず、いきなり多層パーセプトロンの数学的モデルを説明するのではなく、なぜ多層化しないといけないのか、なぜ活性化しないといけないのかから入っている（2章）。
- つまり、入力データ空間が1枚の分離超平面で仕切れるなら多層化も活性化もしなくてよい。
- （以下は教科書の雑なアレンジ）例えば、2次元の入力データが4点あり、各点に "OK" / "NG" のラベルがついているとする。この4点を教師データに、未知の点の "OK" / "NG" を判定するニューラルネットを学習したいとする。
  下図の一番左のように、右上の3点が "OK" なら、1つの仕切りを入れられる。
  左から2番目のように、左下の3点が "OK" でも1つの仕切りを入れられる。
  ただし、左から3番目のように、左上と右下が "OK" だった場合、1つのまっすぐな仕切りではどうにもならない。仕切りを複数入れるか、仕切りをねじ曲げるかしないといけない。そうなると、1層パーセプトロン（入力データの線形変換しかできない）では対応できない。これが2層になると対応できる（下図一番右）。

f:id:cookie-box:20170117170802p:plain:w640

「2層のパーセプトロン（中略）を用いれば、任意の関数を表現可能であることが証明されています（36ページ）。」
- 原論文は以下の方の記事に詳しい。
  mathetake.hatenablog.com
2層ニューラルネット（隠れ層のノード数：50、隠れ層の活性化関数：シグモイド）の MNIST 認識精度（16エポック後）が、目算 95% 弱くらいか（121ページ）。
- 隠れ層なしの単層でも 92% くらい出るが（以下： TensorFlow チュートリアル）この差は大きい。
  https://www.tensorflow.org/tutorials/mnist/beginners/#softmax_regressions
誤差逆伝播法（5章）は、20ページ以上かけて絵本のように説明しているのでこの手法の意図がわかりやすい。
Momentum（171ページ）はハミルトニアンモンテカルロ法っぽい。Momentum は損失関数が小さい方へパラメータを転がす。HMC法では事後確率が大きい方へパラメータを転がす。
- 基礎からのベイズ統計学 Skype読書会(13)：参加メモ - クッキーの日記
Weight decay（193ページ）や Dropout（195ページ）で過学習を抑えられているけど汎化能力も上がっていないようには見える。
7章は CNN で、以下はもう教科書関係ないけど、最近見て面白かったアニメーションと、読んでおきたいサーベイ。
- GitHub - vdumoulin/conv_arithmetic: A technical report on convolution arithmetic in the context of deep learning
- Recent Advances in Convolutional Neural Networks
  https://arxiv.org/pdf/1512.07108v5.pdf

ただ、全体図の確認がなくても、章末にまとめがなくても、章末のまとめがまとめになっていなくても、自分でまとめるというのが勉強になるとは思う。とはいっても、あらゆる本をじっくり読む時間はないので。
「なぜ損失関数を設定するのか？（95ページ）」：この時点でこれが訊けるなら、質問力において魔界大冒険ののび太や数学ガールのユーリと張り合えますね。
微分の定義（97ページ）…今年のセンター試験…。

2017-01-15

keras-rl の example コードを実行するだけ

Keras

Keras を勉強します。
keras-rl でオリジナルの強化学習タスク・オリジナルのDQNモデルを学習したという記事が本日 Qiita に投稿されていましたが（参考記事）、まず keras-rl と gym がわからないので example コードを実行することにします。

参考記事
やること
手順
感想

参考記事

以下の記事を参考にさせていただきましたが、やったことは記事内容のトレースよりはるか低みです。
qiita.com

やること

強化学習で伝統的なポールバランシングタスクをエージェントに学習させます。
小学生のとき掃除の時間に、手のひらに箒をのせて倒れないようにバランスを取るのをよくやったと思います。
今回のタスクのポールの動く範囲は2次元平面内に制約されています。台車も直線上を動きます。
gym でのタスク設定は以下のページ参照。
OpenAI Gym CartPole-v0

その時間ステップにポールが直立していれば +1 の報酬がもらえます。
選択できる行動は台車に +1 の力を加えるか、-1 の力を加えるかのどちらかです。
ポールが15°以上傾くか、台車がスタート位置から所定の距離以上右か左へ外れてしまったらゲームオーバー（エピソード終了）です。

これを行動価値関数 $Q$ のパラメタライズされた関数で近似し最適パラメータを解くんですが、今回は関数というかディープネットにしてしまい、ディープネットの重みの最適化を図ります。

手順

keras はもう導入済みなので、参考記事通りに keras-rl と gym を導入します。
そして今回は以下のコードをそのまま実行するだけです。
https://github.com/matthiasplappert/keras-rl/blob/master/examples/dqn_cartpole.py

# -*- coding: utf-8 -*-
import numpy
import gym

from keras.models import Sequential
from keras.layers import Dense, Activation, Flatten
from keras.optimizers import Adam

from rl.agents.dqn import DQNAgent
from rl.policy import BoltzmannQPolicy
from rl.memory import SequentialMemory

if __name__ == "__main__":
  # 強化学習タスクの環境を構築する
  ENV_NAME = 'CartPole-v0'
  env = gym.make(ENV_NAME)
  numpy.random.seed(123)
  env.seed(123)
  nb_actions = env.action_space.n

  # DQNモデルを準備する
  model = Sequential()
  model.add(Flatten(input_shape=(1,) + env.observation_space.shape))
  model.add(Dense(16))
  model.add(Activation('relu'))
  model.add(Dense(16))
  model.add(Activation('relu'))
  model.add(Dense(16))
  model.add(Activation('relu'))
  model.add(Dense(nb_actions))
  model.add(Activation('linear'))
  print(model.summary())

  # DQNモデルを最適化する上での目的関数の設定
  memory = SequentialMemory(limit=50000, window_length=1)
  policy = BoltzmannQPolicy()
  dqn = DQNAgent(model=model, nb_actions=nb_actions, memory=memory,
                 nb_steps_warmup=10, target_model_update=1e-2, policy=policy)
  dqn.compile(Adam(lr=1e-3), metrics=['mae'])

  # トレーニング
  dqn.fit(env, nb_steps=50000, visualize=True, verbose=2)

  # トレーニングした重みの保存
  dqn.save_weights('dqn_{}_weights.h5f'.format(ENV_NAME), overwrite=True)

  # テスト
  dqn.test(env, nb_episodes=5, visualize=True)

print(model.summary()) で以下のようにモデルの姿を出力してくれます。パラメータ数などわかりやすいです。
当たり前ですが、各層で最適化すべきパラメータ数は、前の層のアウトプットの数 + 1(定数項) に、その層のアウトプットの数を乗じたものになっています。
最終的な出力2は、「+1 の力を入れることの価値」「-1の力を入れることの価値」になっているはずです。

[2017-01-15 23:06:20,720] Making new env: CartPole-v0
__________________________________________________________________________________________
Layer (type)                     Output Shape          Param #     Connected to            
==========================================================================================
flatten_1 (Flatten)              (None, 4)             0           flatten_input_1[0][0]  
__________________________________________________________________________________________
dense_1 (Dense)                  (None, 16)            80          flatten_1[0][0]
__________________________________________________________________________________________
activation_1 (Activation)        (None, 16)            0           dense_1[0][0]          
__________________________________________________________________________________________
dense_2 (Dense)                  (None, 16)            272         activation_1[0][0]     
__________________________________________________________________________________________
activation_2 (Activation)        (None, 16)            0           dense_2[0][0]          
__________________________________________________________________________________________
dense_3 (Dense)                  (None, 16)            272         activation_2[0][0]     
__________________________________________________________________________________________
activation_3 (Activation)        (None, 16)            0           dense_3[0][0]          
__________________________________________________________________________________________
dense_4 (Dense)                  (None, 2)             34          activation_3[0][0]     
__________________________________________________________________________________________
activation_4 (Activation)        (None, 2)             0           dense_4[0][0]          
==========================================================================================
Total params: 658
Trainable params: 658
Non-trainable params: 0
__________________________________________________________________________________________

そして訓練の結果を5エピソード分テストすると、こんなに長い時間ステップの間ポールを倒さず、部屋の中央からも離れずにいることができました。最初がどうだったのか並べないとこれが長いのか短いのかよくわからないですが、トレーニング中はなんかもっとよく倒れていました。

Testing for 5 episodes ...
Episode 1: reward: 21734.000, steps: 21734
Episode 2: reward: 7434.000, steps: 7434
Episode 3: reward: 5168.000, steps: 5168
Episode 4: reward: 13027.000, steps: 13027
Episode 5: reward: 22779.000, steps: 22779

感想

gym のサイトにあるように、実際にポールの動画が出てきて楽しい。

2017-01-13

数理論理学：ノート3

本読み数理論理学

読んでいる本（出典）：数理論理学 | 戸次大介 |本 | 通販 | Amazon

前回：ノート2 ／次回：ノート4
目次：数理論理学

第4章は一階命題論理の応用としての論理回路の話で、ノートは省略。
以下、第5章前半の自分の理解。第5章は一階述語論理。今回のノートは統語論まで。

前回までのあらすじ

「妥当な証明とは何か」を打ち立てるために、まず一階命題論理という体系を考えた。
- 個々の命題を論理式（原子命題を表す命題記号 or 論理式を真理関数に代入したもの）で表し、 $2$ 原子命題の数通りの解釈の上に個々の論理式の真偽 $\{1,0\}$ を定めた。
- ある解釈の下で、前提の命題たちを表す論理式列が全て $1$ で、帰結の命題を表す論理式が $0$ になる場合、その推論は妥当でないとした（どんな解釈の下でもそうならない場合、その推論は妥当であるとした）。

一階命題論理で表現できないこと

一階命題論理では個々の原子命題の中身には立ち入らず、各々の原子命題が真のパターンの解釈・偽のパターンの解釈を考える。
他方、我々は直観的には以下のように無数につくれる原子命題が全部真であることがわかる。
　　　 $P_1 \equiv$ 「西暦2019年は平成ではない」
　　　 $P_2 \equiv$ 「西暦2020年は平成ではない」
　　　 $P_3 \equiv$ 「西暦2021年は平成ではない」
　　　 $\cdots$
もし真ということにしておきたい論理式があれば真と仮定しておけばよいのだが、一階命題論理で「無数の論理式がすべて真」という知見は一気に表せない。と無数につなげた論理式を真と仮定したいところだが、無限の長さをもつ論理式は認められていない（25ページ）。
- 認められていないというか、論理式の定義が再帰的なので、無限の長さをもつ形式が論理式かどうか確かめようがない。
あるいは $P \equiv$ 「西暦2019年以降のすべての年は平成ではない」を真と仮定したところで、 $P, P_1, P_2, P_3, \cdots$ たちは互いに別々の赤の他人の原子命題なので、 $P_1, P_2, P_3, \cdots$ の真偽について何も示唆できていない。
このように、一階命題論理では「すべての $x$ について～」のような論理式から直観的に得られる知見を表現できていない。証明の妥当性を論じたいのに、数学の証明でよくつかう形式の直観を表現できていないのは具合が悪い。
これの解決に向けては、原子命題の中身に立ち入って分解するしかない。例えば $P_1$ は、「西暦2019年は平成ではない」のように名前 $a$ と述語 $F$ からなる $P_1=F(a)$ とする。さらに、 $\forall$ や $\exists$ といった量化子を導入し、「すべての $x$ について $F(x)$ 」「ある $x$ が存在して $F(x)$ 」のような論理式をそれぞれ $\forall x(F(x)), \; \exists x(F(x))$ と表すことにする。

一階述語論理の統語論

一階述語論理の述語は項という形式を $n$ 個取る。
以下の形式を満たさないものは一回述語論理の論理式ではない。
命題記号が基本述語になった点と、量化論理式が加わった点が一階命題論理と異なる。

一階述語論理における項 $\tau$	$a, \; x,$ 　名前は項、変項も項 $f(a_1, a_2, x_1, x_2, x_3), \; g(f(a_1, a_2, x_1, x_2, x_3), a_3, x_4)$ 　項を $n$ 項演算子に入れても項
一階述語論理における論理式	$\theta(\tau_1, \cdots, \tau_n),$ 　項を $n$ 項述語に入れたら論理式（基本述語） $\rho(\varphi_1, \cdots, \varphi_n),$ 　論理式を $n$ 項真理関数に入れても論理式（複合論理式） $\forall \xi \varphi, \; \exists \xi \varphi$ 　量化子 + 変項 + 論理式は論理式（量化論理式）

量化子により、一回命題論理ではそれ以上分析しようがなかった命題が、もっと細かい要素からかける。
- 例： 5は素数である（＝5は1ではない自然数であって、5を割り切れる自然数は1と5のみである）。
  $(5 \in \mathbb{N}) \land \lnot (5 = 1) \land \forall x \biggl( (x \in \mathbb{N}) \land \exists a \Bigl( (a \in \mathbb{N}) \land (x \times a = 5) \to (x = 1) \lor (x = 5) \Bigr) \biggr)$
量化論理式の部分論理式の集合には、束縛変項 $\xi$ に任意の項を代入したものが含まれるので（89ページ）、（任意の項が可算個あれば）部分論理式の集合の元の個数が可算個になりそう。

Q：記号集合 $\mathcal{A}=\{ (, \; ), \; ,, \; {\rm true}, \; {\rm false}, \; \lnot, \; \land, \; \lor, \; \to, \; \leftrightarrow, \; \forall, \; \exists, \; a_1, \; x_1, \; f_1, \; F_1, \; a_2, \; x_2, \; f_2, \; F_2, \; \cdots \}$ のもとでの一階述語論理の項と論理式全体に自然数のインデックスをふることはできるでしょうか。
A：できる。 $\mathcal{A}$ が可算集合でもOK。以下のように記号列 $s_1 s_2 \cdots s_n$ に自然数を対応させる写像がつくれる。
ただし ${\rm Pr}(n)$ は $n$ 番目の素数、 $i(s)$ は記号 $s$ の記号集合 $\mathcal{A}$ 内でのインデックスとする。
　　　 $g(s_1 s_2 \cdots s_n) = {\Pr}(1)^{i(s_1)} \times {\Pr}(2)^{i(s_2)} \times \cdots {\Pr}(n)^{i(s_n)}$ 　 $s_1 s_2 \cdots s_n$ のゲーデル数

練習問題5.15　一部略。

どの自然数にも、それより大きな自然数が存在する。
$\forall x \biggl( (x \in \mathbb{N}) \to \exists y \Bigl( (y \in \mathbb{N}) \land (x < y) \Bigr) \biggr)$
数列は発散する。
$\forall \varepsilon \biggl( (\varepsilon \in \mathbb{R}^+) \to \exists n_0 \Bigl( (n_0 \in \mathbb{N}) \land \forall n \bigl( (n_0 < n) \to (|\alpha - a_n| < \varepsilon) \bigr) \Bigr) \biggr)$
$\forall \varepsilon \biggl( (\varepsilon \in \mathbb{R}^+) \to \exists n_0 \Bigl( (n_0 \in \mathbb{N}) \land \forall n \bigl( (n_0 < n) \to (|\alpha - a_n| < \varepsilon) \bigr) \Bigr) \biggr)$
- 上記のどちらでもよい。緑色の部分は「数列 $(a_n)_{n \in \mathbb{N}}$ は $\alpha$ に収束する」。
  上の回答は「どの $\alpha$ にも収束しない」。下の解答は「ある $\alpha$ に収束するということはない」。

練習問題5.20　論理式から自由変項の集合と束縛変項の集合を抜き出す問題。一部略。

${\rm fv} \bigl( F(x, a, f(x)) \bigr) = {\rm fv} (x) \cup {\rm fv} (a) \cup {\rm fv} \bigl(f(x) \bigr) = \{ x \} \cup \{\} \cup {\rm fv} (x) = \{x\}$
${\rm bv} \bigl( F(x, a, f(x)) \bigr) = {\rm bv} (x) \cup {\rm bv} (a) \cup {\rm bv} \bigl(f(x) \bigr) = \{\} \cup \{\} \cup {\rm bv} (x) = \{\}$
${\rm fv} \bigl( \exists x \forall y F(y, x) \land \forall x \exists z F(z, y) \bigr) = {\rm fv} \bigl( \exists x \forall y F(y, x) \bigr) \cup {\rm fv} \bigl( \forall x \exists z F(z, y) \bigr)$
　　　 $= \Bigl( {\rm fv} \bigl( \forall y F(y, x) \bigr) - \{x\} \Bigr) \cup \Bigl( {\rm fv} \bigl( \exists z F(z, y) \bigr) - \{x\} \Bigr)$
　　　 $= \Bigl( \bigl( \{y, x\} - \{y\} \bigr) - \{x\} \Bigr) \cup \Bigl( \bigl( \{z, y\} - \{z\} \bigr) - \{x\} \Bigr) = \{\} \cup \{y\} = \{y\}$
${\rm bv} \bigl( \exists x \forall y F(y, x) \land \forall x \exists z F(z, y) \bigr) = {\rm bv} \bigl( \exists x \forall y F(y, x) \bigr) \cup {\rm bv} \bigl( \forall x \exists z F(z, y) \bigr)$
　　　 $= \Bigl( {\rm bv} \bigl( \forall y F(y, x) \bigr) \cup \{x\} \Bigr) \cup \Bigl( {\rm bv} \bigl( \exists z F(z, y) \bigr) \cup \{x\} \Bigr)$
　　　 $= \Bigl( \bigl( \{\} \cup \{y\} \bigr) \cup \{x\} \Bigr) \cup \Bigl( \bigl( \{\} \cup \{z\} \bigr) \cup \{x\} \Bigr) = \{x, y\} \cup \{x, z\} = \{x, y, z\}$

練習問題5.27　変項への代入の問題。これでいいのかな。

$(\forall x (F(f(x),y)))[y/x] = \forall x (F(f(x),y))$ 　 $x$ が束縛変項なので $x$ には代入できないパターン。
$(\forall y (F(f(x),y)))[z/x] = \forall y (F(f(z),y))$ 　 $y$ が束縛変項なので $x$ には $y$ が入っていない項は代入できる。
$(\forall x (F(f(y),z)))[y/x] = \forall x (F(f(y),z))$ 　 $x$ が束縛変項なので $x$ には代入できないパターン。
$(\forall y (F(f(y),z)))[y/x] = \forall y (F(f(y),z))$ 　 $x$ に代入しようとしても $x$ がない…。
$(\forall y (F(f(y),z)))[z/x] = \forall y (F(f(y),z))$ 　 $x$ に代入しようとしても $x$ がない…。
$(\forall y (F(f(x),y)))[y/x] = (\forall v (F(f(x),v)))[y/x] = \forall v (F(f(y),v))$ 　束縛変項を別の変項に回避するパターン。

練習問題5.30　項から部分項を抜き出す問題

${\rm Sub}\bigl( (1 + 2) \times ( x + (1 \times 2)) \bigr) = {\rm Sub}\bigl( 1 + 2 \bigr) \cup {\rm Sub}\bigl( x + (1 \times 2) \bigr) = \{1, 2, x\}$

練習問題5.32　面倒なので略。

練習問題5.36　面倒なので略。

練習問題5.39　面倒なので略。

練習問題5.40

任意の変項 $\xi,$ 項 $\tau, \, \sigma$ について以下が成り立つことを示せ。
${\rm fv}(\sigma [ \tau / \xi ])=\begin{cases} ({\rm fv}(\sigma) - \{ \xi \}) \cup {\rm fv}(\tau) & (\xi \in {\rm fv}(\sigma)) \\ {\rm fv}(\sigma) & (\xi \notin {\rm fv}(\sigma)) \end{cases}$

項 $\sigma$ の深さ $d$ に関する帰納法で証明する。

のとき：以下より、成り立つ。
- $\sigma$ が名前 $\alpha$ のとき： $\xi \notin {\rm fv}(\sigma) = \{\}$ で、 ${\rm fv}(\sigma [ \tau / \xi ])={\rm fv}(\alpha [ \tau / \xi ])={\rm fv}(\alpha)={\rm fv}(\sigma)$
- $\sigma$ が変項 $\xi$ のとき： $\xi \in {\rm fv}(\sigma) = \{\xi\}$ で、 ${\rm fv}(\sigma [ \tau / \xi ])={\rm fv}(\xi [ \tau / \xi ])={\rm fv}(\tau)=({\rm fv}(\sigma) - \{\xi\}) \cup {\rm fv}(\tau)$
- $\sigma$ が変項 $\zeta \neq \xi$ のとき： $\xi \notin {\rm fv}(\sigma) = \{\zeta\}$ で、 ${\rm fv}(\sigma [ \tau / \xi ])={\rm fv}(\zeta [ \tau / \xi ])={\rm fv}(\zeta)={\rm fv}(\sigma)$
$1 < d$ のとき：深さ $d$ 未満の項 $\sigma$ については問題の式が成り立つと仮定する。
深さ $d$ の項 $\sigma$ については、 $\sigma = o(\sigma_1, \cdots, \sigma_n)$ とすると、
　　　 ${\rm fv}(\sigma)={\rm fv}(o(\sigma_1, \cdots, \sigma_n))={\rm fv}(\sigma_1) \cup \cdots \cup {\rm fv}(\sigma_n)$
　　　 ${\rm fv}(\sigma [ \tau / \xi ])={\rm fv}(o(\sigma_1, \cdots, \sigma_n) [ \tau / \xi ])={\rm fv}(\sigma_1 [ \tau / \xi ]) \cup \cdots \cup {\rm fv}(\sigma_n [ \tau / \xi ])$
${\rm fv}(\sigma_1), \cdots , {\rm fv}(\sigma_n)$ のいずれにも $\xi$ が含まれていないなら、 $\xi \notin {\rm fv}(\sigma)$ で、
　　　 ${\rm fv}(\sigma [ \tau / \xi ])={\rm fv}(\sigma_1 [ \tau / \xi ]) \cup \cdots \cup {\rm fv}(\sigma_n [ \tau / \xi ])={\rm fv}(\sigma_1) \cup \cdots \cup {\rm fv}(\sigma_n)={\rm fv}(\sigma)$
${\rm fv}(\sigma_1), \cdots , {\rm fv}(\sigma_n)$ のいずれかに $\xi$ が含まれているなら（最初の $k$ 個としてもよい）、 $\xi \in {\rm fv}(\sigma)$ で、
　　　 ${\rm fv}(\sigma [ \tau / \xi ])=({\rm fv}(\sigma_1) - \{ \xi \}) \cup \cdots \cup ({\rm fv}(\sigma_k) - \{ \xi \}) \cup {\rm fv}(\sigma_{k+1}) \cup \cdots \cup {\rm fv}(\sigma_n) \cup {\rm fv}(\tau)$
　　　　　　　　 $\; =({\rm fv}(\sigma)-\{ \xi \}) \cup {\rm fv}(\tau)$

練習問題5.41　面倒なので略。

練習問題5.43　面倒なので略。