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

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 のサイトにあるように、実際にポールの動画が出てきて楽しい。

数理論理学: ノート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
  • もし真ということにしておきたい論理式があれば真と仮定しておけばよいのだが、一階命題論理で「無数の論理式がすべて真」という知見は一気に表せない。 P_1 \land P_2 \land P_3 \land \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)
  • 数列  (a_n)_{n \in \mathbb{N}} は発散する。
     \forall \alpha \Biggl( \lnot  \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) \Biggr)
     \lnot \exists \alpha \Biggl( \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) \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 に関する帰納法で証明する。

  •  d=1 のとき: 以下より、成り立つ。
    •  \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 面倒なので略。

Keras でロジスティック回帰するだけ

深層学習には Keras が便利という巷の評判に流されて Keras を勉強します。
でも冷静に考えると普段から別に深層学習などやっていなかったので、そういうのは今後やります。

参考文献

以下の記事を全面的に参考にさせていただきました。
aidiary.hatenablog.com

使用データ

手元にある都合上、以下の2章に出てくる10000人の身長・体重データをつかいます。データは GitHub にあります。

入門 機械学習入門 機械学習
Drew Conway John Myles White 萩原 正人

オライリージャパン 2012-12-22
売り上げランキング : 243617

Amazonで詳しく見る
by G-Tools
ML_for_Hackers/02-Exploration/data at master · johnmyleswhite/ML_for_Hackers · GitHub
上のデータをプロットすると以下のようになります。たぶんアメリカ人のデータです。データ上、前半5000レコードが男性、後半5000レコードが女性なので女性の点が上に重なってみえます。
f:id:cookie-box:20170111110830p:plain:w440

やること

上図の Height‐Weight 平面に直線を引いて男女を分離できるかというと完全にはできないですが、だいたい合っていればいいと思えばできるので、一番いい直線をロジスティック回帰で求めます。
要は、以下のピンク色の係数の最適化をします。

   f:id:cookie-box:20170111164918p:plain:w525

手順

データを R でもっていることが多い都合上、無駄に R を経由します。
まず R でデータを読み込んでダミー変数を付与します。ヤードポンド法も撲滅します。なお、結局正規化するので特に撲滅する意味はないです。

data.file <- file.path('data', '01_heights_weights_genders.csv')
heights.weights <- read.csv(data.file, header=TRUE, sep = ',')
heights.weights$Height <- 2.54 * heights.weights$Height              # インチ --> センチ
heights.weights$Weight <- 0.45359237 * heights.weights$Weight        # ポンド --> キログラム
heights.weights$Male <- ifelse(heights.weights$Gender=='Male', 1, 0) # 男性なら1、女性なら0
save(heights.weights, file='heights_weights_genders.RData')
  Gender   Height    Weight Male
1   Male 187.5714 109.72107    1
2   Male 174.7060  73.62279    1
3   Male 188.2397  96.49763    1

次に Python から読みこんで Keras にロジスティック回帰してもらいます。ほとんど参考記事通りのコードです。
参考記事の記述通り、データは正規化しないと全くトレーニングが進みませんでした。初期値を何とかすればいいのかもしれませんが。

# -*- coding: utf-8 -*-
from sklearn import preprocessing
from keras.models import Sequential
from keras.layers.core import Dense, Activation

import pyper
import pandas
import numpy

if __name__ == "__main__":
  # load data
  r = pyper.R(use_pandas='True')
  r("load(\"heights_weights_genders.RData\")")
  heights_weights = pandas.DataFrame(r.get("heights.weights"))
  heights_weights.columns = ['Gender', 'Height', 'Weight', 'Male']
  x = numpy.array(heights_weights.ix[:,('Height', 'Weight')])
  y = numpy.array(heights_weights.ix[:,'Male'])
  r = None

  # normalize data
  x = preprocessing.scale(x)
  r = pyper.R(use_pandas='True')
  r.assign("heights.weights.mod", x)
  r("save(heights.weights.mod, file=\"heights_weights_mod.RData\")")
  r = None

  # create model
  model = Sequential()
  model.add(Dense(1, input_shape=(2, )))
  model.add(Activation('sigmoid'))
  model.compile(optimizer='adam', loss='binary_crossentropy', metrics=['accuracy'])

  # train model
  model.fit(x, y, nb_epoch=1000, batch_size=100, verbose=1)

  # result
  result = model.layers[0].get_weights()
  w1 = result[0][0, 0]
  w2 = result[0][1, 0]
  b = result[1][0]
  print w1, w2, b
Epoch 1/1000
10000/10000 [==============================] - 0s - loss: 0.7057 - acc: 0.5044      
Epoch 2/1000
10000/10000 [==============================] - 0s - loss: 0.6449 - acc: 0.6339     
Epoch 3/1000
10000/10000 [==============================] - 0s - loss: 0.5955 - acc: 0.7099     
... 
Epoch 999/1000
10000/10000 [==============================] - 0s - loss: 0.2091 - acc: 0.9194     
Epoch 1000/1000
10000/10000 [==============================] - 0s - loss: 0.2091 - acc: 0.9193     
 -1.89395 6.36942 0.0175593


上の実行結果では、最終的な正解率が 0.9194 とか 0.9193 になっていますが、そもそも上図のデータを直線で分離しようというのが雑な話なのでこれよりよくならないです。なお、R の glm でロジスティック回帰しても正解率は 0.9194 になります(以下;但し、シグモイド関数の出力が 0.5 未満を女性判定、0.5以上を男性判定とします)。
性別を正しく判定できなかった 806人の方には申し訳ありませんが、致し方ないです。

logit.model <- glm(Male ~ Weight + Height,
                   data = heights.weights,
                   family = binomial(link = 'logit'))
> logit.model
Coefficients:
(Intercept)       Weight       Height  
     0.6925       0.4373      -0.1939  
> length(which(floor(logit.model$fitted.values + 0.5) == heights.weights$Male))
[1] 9194

左が Keras の結果(但し、平均0、標準偏差1になるよう正規化済み)、右が R glm の結果です。

f:id:cookie-box:20170111175147p:plain:w380 f:id:cookie-box:20170111175202p:plain:w380

「これからの強化学習」勉強会#3(準備中)→ ノート3

読んでいる本(出典): これからの強化学習 | 牧野 貴樹, 澁谷 長史, 白川 真一 |本 | 通販 | Amazon

前回: 勉強会#2 / 次回: まだ
目次: これからの強化学習 / Sutton & Barto 強化学習(邦訳)の目次: 強化学習

「これからの強化学習」のエア勉強会3回目の準備中。
(スライドはできて)ないです。第2章の2.1節はページ数が多いし、後半は学習アルゴリズムのオムニバスなので、自分なりの講義にする余地がなくてスライドをつくれなさそう。

以下、2.1節(72~111ページ)の読書メモ。

  • 2.1節: 「パラメタライズされたモデルでおいた価値関数はちゃんと収束するのか」が中心的話題。
    まず、パラメタライズされたモデルといっても色んなモデルが仮定できるけど、状態と行動が離散的で、実質的に \pi 固定した動的プログラミング(方策反復)と変わらないモデルを考える(各状態の  \hat{V}^{\pi} (s_i) がそのままパラメータになっている)。これは当然収束する(だって方策反復DPだから)。
    テキストでは、収束するかちゃんと確かめなければならない理由を、教師あり学習と違って固定された教師信号との誤差の最小化になっていない、と。強化学習には正解がないので最初からパラメータの到達すべき場所はわからない。前ステップの推定モデルで測った価値より今ステップの推定モデルで測った価値が現実をよく表すように動かすしかない(その測った価値すらモデル依存)。と考えると、本当にちゃんとどこかにたどり着くのかは確かに不安だと思う。
    そして、もっと違うモデルにした場合でも同じパラメータ更新式を使用することに決め打つと(なんで同じパラメータ更新式をつかい回しすことに決め打ったのかちょっとよくわからない)、「方策オンかつ線型モデル」でない限り収束が保証されない。線型かつ方策オフのとき収束が保証されない理由はもうちょっとかいてあるけど、非線形のときはよくわかりません。
    TD(λ) 法の場合は λ=1(要はモンテカルロ法)の場合はモデルにかかわらず収束する。
    Sarsa や Q学習は、\pi 固定のときと同じ感じで、方策オンかつ線型の限られた場合でのみ収束する。
    最初に決め打ったパラメータ更新式ではなくて、実際に何らかの目的関数を最適化する学習アルゴリズムも色々ある。色々あるけど、ひっくるめてセミパラメトリック推定として理解できると。
    • 教師あり学習で2乗誤差の勾配方向に適切な距離だけパラメータ更新していけばモデルはちゃんと改善する(74ページ)って進研ゼミじゃなくて青い本のオンライン機械学習でやった。でも強化学習では近づくべき正解もわからなければ、得られるデータも自分の行動に依存するので同じ議論ができないと。
    • マルコフ連鎖が規約ならば唯一の定常分布をもつ(75ページ)って伊庭先生のMCMCの本でやった。
    • 「状態価値関数(中略)に収束する。これは、ベルマンオペレータが一様ノルムに対して縮小写像となることから示すことができる(76ページ)」: このくだりは、Sutton でいうと「系列  \{V_k\} が極限  k \to \infty V^\pi に収束することが一般的に示される(96ページ)」に相当する。
    • 78ページ (2.1.24) 式で言いたいのは、「最良な行動をとったときの報酬の最大値の期待値(最左辺 & 中辺)」と「最良な行動をとったときの期待値の最大値(最右辺)」は等しくないと。
      • 転職に悩めるエージェント(勉強会#1のスライド10ページ)が「不満」な状態にあるとき、「転職」することが最良な行動だとして、前者は A-c だけど、後者は \beta (A-c) + (1-\beta)(B-c) だから等しくない(転職に悩めるエージェント問題は状態遷移のみが確率的で、報酬は与えられた状態-行動-状態組について決定的としていたが、一般にはさらに報酬も確率的)。
    • 78ページ (2.1.27) は Sarsa の更新式そのもの、(2.1.28) はQ学習の更新式そのもの。
      • ただし、86ページの書き方だと、毎ステップ \pi を改善しないなら Sarsa ではない? この本での Sarsa の初出箇所(33ページ~)では、\pi を更新しようとしなかろうとこの更新式で \pi の下での価値関数を改善するのが Sarsa のようには読めた。
    • 「一般に、ある行動方策に従って得られる状態行動系列は、状態遷移確率のもつマルコフ性を有するため、集合 \mathcal{S} から一様ランダムに選択して得られる状態とは大きく異なる(79ページ)」: だからこそ、Sutton の 135ページ~の方策オフ型モンテカルロのような、目的の行動方策の下での確率測度への変換を行う手法があると思うんだけど、こちらの本ではそのような手法の紹介はこれより後。
    • 81ページ (2.1.29) の線形モデルのイメージ: これって、 \hat{V}^{\pi} (s_i) をそのまま  \theta_i に書き換えただけ。「この更新則が、式 (2.1.29) の関数近似器を用いるとき、テーブル表現した価値関数のTD学習に一致することを確かめてみよう(82ページ)」というのも、書き換えただけなので当然。
      • \theta=(盤面1の価値. 盤面2の価値, 盤面3の価値,  \cdots)
        \phi (盤面1)=(1, 0, 0, \cdots)
        \phi (盤面2)=(0, 1, 0, \cdots)
    • TD(λ) 法の前方観測と後方観測って何だったっけ。

数理論理学: ノート2

読んでいる本(出典): 数理論理学 | 戸次 大介 |本 | 通販 | Amazon

前回: ノート1 / 次回: ノート3
目次: 数理論理学

以下、第3章の自分の理解。第3章は一階命題論理。

一階命題論理の統語論

  • 一階命題論理では、命題(≡ 真偽を問うことのできる形式)を下のような論理式にかきあらわす。
    この形式を満たさないものは論理式ではない。
    一階命題論理に
    おける論理式
     P, \; Q, \; R,  命題記号は論理式
     \top , \; \perp , \; \lnot(P) , \; \land(P, Q) , \; \to \! \! (P, Q),  n項真理関数に論理式を代入した形式も論理式
     \lnot(\top) , \; \lor(\land(P, Q), R) , \; \leftrightarrow \! \! (\lnot(\top), \lor(\land(P, Q), R))  なので、これらも論理式
    ちなみに、上の例の最後の論理式の部分論理式の集合は以下。
     {\rm SubF}\bigl( \leftrightarrow \! \! (\lnot(\top), \lor(\land(P, Q), R)) \bigr) = \{ \leftrightarrow \! \! (\lnot(\top), \lor(\land(P, Q), R)) \} \cup {\rm SubF}\bigl( \lnot(\top) \bigr) \cup {\rm SubF}\bigl( \lor(\land(P, Q), R)) \bigr)
      = \{ \leftrightarrow \! \! (\lnot(\top), \lor(\land(P, Q), R)), \; \lnot(\top), \; \lor(\land(P, Q), R)) \} \cup {\rm SubF}\bigl( \top \bigr) \cup {\rm SubF}\bigl( \land(P, Q) \bigr) \cup {\rm SubF}\bigl( R \bigr)
      = \{ \leftrightarrow \! \! (\lnot(\top), \lor(\land(P, Q), R)), \; \lnot(\top), \; \lor(\land(P, Q), R)), \; \top, \; \land(P, Q), \; R \} \cup {\rm SubF}\bigl( P \bigr) \cup {\rm SubF}\bigl( Q \bigr)
      = \{ \leftrightarrow \! \! (\lnot(\top), \lor(\land(P, Q), R)), \; \lnot(\top), \; \lor(\land(P, Q), R)), \; \top, \; \land(P, Q), \; R, \; P, \; Q \}

一階命題論理の意味論

  • 上で命題をあらわす論理式に形式的定義を与えたので、次に、論理式の真偽を考える。ここで「真偽を問う」というのは、「集合  D_t \equiv \{1,0\} の要素へ対応させる」ということとする。この  D_t領域という。ここでの領域には「真(1)」と「偽(0)」のみがあり、「ちょっと真」とかはない。
  • それで論理式の真偽を考えると、「n は偶数である」「今年は2月29日がある」「丸の内線の線路は地下にある」「コイルはでんきタイプ単色である」など、真か偽かは状況によることに気付く。このようなあらゆる状況を明示的に取り扱うことはできない気がする。
  • 逆に、「論理式の集合  \rightarrow D_t」という写像の1つ1つが「このような状況」を表しているといえる。
    • 例えば、以下の原子命題を考える。
            Pコイルはでんき単 \equiv「コイルはでんきタイプ単色である」
      このとき、 \{Pコイルはでんき単\} \to D_t なる写像全体は以下の2つ。これらがそれぞれ状況に相当する。
      写像1写像2
       Pコイルはでんき単  \mapsto \; 1 Pコイルはでんき単  \mapsto \; 0
      • 写像1は感覚的には、コイルがでんき単色だった "第1世代" という状況に相当する。
      • 写像2は感覚的には、はがねタイプが追加された "第2世代以降" という状況に相当する。
    • ここに原子命題をもう1つ付け加える。
            Pコイルはでんき単 \equiv「コイルはでんきタイプ単色である」
            Pピッピはノーマル \equiv「ピッピはノーマルタイプである」
       \{Pコイルはでんき単, \; Pピッピはノーマル\} \to D_t なる写像全体は以下の4つになる。
      写像3写像4写像5写像6
       Pコイルはでんき単  \mapsto \; 1
       Pピッピはノーマル  \mapsto \; 1
       Pコイルはでんき単  \mapsto \; 1
       Pピッピはノーマル  \mapsto \; 0
       Pコイルはでんき単  \mapsto \; 0
       Pピッピはノーマル  \mapsto \; 1
       Pコイルはでんき単  \mapsto \; 0
       Pピッピはノーマル  \mapsto \; 0
      • 写像3は感覚的には、"第1世代" という状況に相当する。
      • 写像4のような世代は実際なかったが、とりあえず状況としては定義できる。
      • 写像5は感覚的には、"第2~5世代" という状況に相当する。
      • 写像6は感覚的には、フェアリータイプ追加後の "第6世代" という状況に相当する。
  • この「 I: 論理式の集合  \rightarrow D_t」であるような写像  I解釈という。解釈という言葉へのイメージは、「地球は動いている」は、「天動説」という解釈の下では偽で、「地動説」という解釈の下では真みたいな。
  • 解釈をつかうと、「 Pコイルはでんき単 は真か?」という問いへの答えは「 I(Pコイルはでんき単)=1 であるような解釈 I の下では真である」になるけど、これ自体は「真のときは真です」と言っているだけなので何もうれしくない。
    ただ、論理式が原子命題ではない場合、例えば「 Pコイルはでんき単 \lor Pピッピはノーマル は真か?」という問いには、部分論理式に含まれる原子命題の真偽で場合分けすればよく、「写像3, 写像4, 写像5で表される解釈の下では真で、写像6で表される解釈の下では偽です」となる。これは「真のときは真です」以上のことを言っている。真偽を考えるべき論理式は無数に存在するが、考えなければならない状況の数は  2原子命題の数 だけでよい。
  • 解釈 I によらず真な論理式(恒真式)もある。よく知られているものは例えば以下。
    •  \varphi \land \psi \leftrightarrow \psi \land \varphi 交換律
    •  \varphi \lor \psi \leftrightarrow \psi \lor \varphi 交換律
    •  \varphi \to \psi \leftrightarrow \lnot \psi \to \lnot \varphi 対偶律
    •  \varphi \land \lnot \varphi 排中律

じゃあ一階命題論理において妥当な推論とは何か

  • 妥当な推論とは何かとは意味論的推論に基づくことにしていたのだが、意味論的推論を一階命題論理の言葉に書き直すとこうなる: \Gamma , \, \Delta を論理式列として(ただし |\Delta| は高々1)、以下を満たすとき「\Gamma\Delta を意味論的に含意する」といい、 \Gamma \models \Delta とかく。
    • 以下のような解釈  I が存在しない。
      •  \Gamma に含まれるすべての論理式  \varphi について I(\varphi)=1 である。
      •  \Delta に含まれるすべての論理式  \psi について I(\psi)=0 である。
  • 例えば、 P \to Q, \, Q \to R \, \Rightarrow \, P \to R は妥当な推論である。つまり、 P \to Q, \, Q \to R \, \models \, P \to R が成立する。これは、以下の真偽値表で確認できる。
    • まず、登場する原子命題が  P, Q, R の3つなので、2^3=8 つの解釈を考えればよい(下表の各行)。
    • それぞれの解釈の下での  P \to Q, \; Q \to R, \; P \to R の真偽値を書き入れる。
    •  P \to Q, \, Q \to R \, \models \, P \to R であるためには、 I(P \to Q), \; I(Q \to R)1 であって、I(P \to R)0 であるような解釈 I が存在してはならないが、 I(P \to Q), \; I(Q \to R)1 であるような行を薄い青で塗ると、それらの行ではすべて I(P \to R)1 なので、  P \to Q, \, Q \to R \, \models \, P \to R は成立する。

P Q R P \to Q Q \to R P \to R
1 1 1 1 1 1 1 1 1 1 1 1
1 1 0 1 1 1 1 0 0 1 0 0
1 0 1 1 0 0 0 1 1 1 1 1
1 0 0 1 0 0 0 1 0 1 0 0
0 1 1 0 1 1 1 1 1 0 1 1
0 1 0 0 1 1 1 0 0 0 1 0
0 0 1 0 1 0 0 1 1 0 1 1
0 0 0 0 1 0 0 1 0 0 1 0

  •  \quad \models \varphi は論理式 \varphi が恒真であることを意味する(I(\varphi)=0 となる解釈 I が存在しないということだから)。
  •  \Gamma \models \quad は論理式列 \Gamma が矛盾していることを意味する(\Gamma に含まれるすべての \varphi を同時に I(\varphi)=1 とする解釈 I が存在しないということだから)。
  • \varphi \models \psi かつ \psi \models \varphi のとき、\varphi\psi は意味論的に同値であるといい、\varphi = \! \! \! | | \! \! \! = \psi とかく。
  • 真偽値表をかけばどんな推論も妥当かどうか手続き的に確かめられるが、以下のような定理(教科書には他にも色々示されている)を活用するともっと楽になる。「推論が意味論的に妥当かどうか」を、「論理式が恒真かどうか」という確認に落とし込むとよい。
    • \varphi \models \psi \; \Longleftrightarrow \; \models \varphi \to \psi
    • \varphi = \! \! \! | | \! \! \! = \psi \; \Longleftrightarrow \; \models \varphi \leftrightarrow \psi
    • ある論理式と、その論理式の部分論理式を意味論的同値な論理式に置き換えた論理式は、意味論的同値。 置き換え
    •  \Gamma \models \varphi, \; \; \Delta, \varphi, \Delta' \models \psi \; \Longrightarrow \; \Delta, \Gamma, \Delta' \models \psi カット
    •  \varphi, \Gamma \models \perp \; \Longleftrightarrow \; \Gamma \models \lnot \varphi 背理法

ここまで来て気付くこと

  • n項真理関数を色々考えていたけど、冷静に考えると任意の真偽値の出力って  \lnot, \; \land, \; \lor だけでできるのでは。
    • 真偽値表で1になる行を全部抜いてきて、(P \land Q \land R) \lor (P \land \lnot Q \land R) \lor \cdots のようにつないでいけばよい。 選言標準形
    • 逆に、真偽値表で0になる行を抜いてきて、(P \land Q \land \lnot R) \land (P \land \lnot Q \land \lnot R) \land \cdots のようにつないでいって最後に全体に \lnot してもよい。 連言標準形
  • もっというと、ドゥ・モルガンの法則をつかうと  \land \lor に換えたり、その逆ができるので、 \{\lnot, \; \land, \; \lor\} から  \land \lor のどちらか一方をリストラしてもあらゆる真偽値の出力がつくれる。 表現的適格性
    •  \{ \lnot, \; \land \}  \{ \lnot, \; \lor \} という組でなくてもよい。例えば  \{\lnot, \; \to\} でもOK。
  • さらにいうと、NAND または NOR は単独で表現的に適格になれる。



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

  • まず、(論理式全体の集合)=(命題記号の集合)  \oplus (複合論理式の集合)。
  • 仮定より、解釈  I_1 I_2 で、任意の命題記号について、I_1 ( 命題記号 )=I_2 ( 命題記号 )
  • 複合論理式は、手元に命題記号たちだけがある状態からはじめて、n項真理関数を有限回つかえばつくれる。
    以下を帰納法で示せばよい。
    • I_1 ( n項真理関数を1回つかった論理式 )=I_2 ( n項真理関数を1回つかった論理式 )
    • I_1 ( n項真理関数を2回つかった論理式 )=I_2 ( n項真理関数を2回つかった論理式 )
    • \cdots

練習問題3.28 面倒なので略。
練習問題3.31

  • 2^{2^0}=2 より、0項真理関数は2個ある。だから、 \top, \; \perp で全部。

練習問題3.35

  • 2^{2^1}=4 より、1項真理関数は4個ある。だから、 \lnot の他に3個ある(練習問題3.36)。

練習問題3.36

  • どんな値を取っても1を返す関数。
  • どんな値を取っても0を返す関数。
  • 「取った値に何もせずそのまま返す」という関数。

練習問題3.39

練習問題3.40

  •  n 項真理関数は 22^n 乗個ある。

練習問題3.42 面倒なので略。
練習問題3.44 真偽値表で38~39ページの恒真式が恒真式であることを確認せよという問題。ドゥ・モルガンの法則だけ。
\varphi \psi \lnot ( \varphi \land \psi ) \leftrightarrow \lnot \varphi \lor \lnot \psi
1 1 0 1 1 1 1 0 1 0 0 1
1 0 1 1 0 0 1 0 1 1 1 0
0 1 1 0 0 1 1 1 0 1 0 1
0 0 1 0 0 0 1 1 0 1 1 0
\varphi \psi \lnot ( \varphi \lor \psi ) \leftrightarrow \lnot \varphi \land \lnot \psi
1 1 0 1 1 1 1 0 1 0 0 1
1 0 0 1 1 0 1 0 1 0 1 0
0 1 0 0 1 1 1 1 0 0 0 1
0 0 1 0 0 0 1 1 0 1 1 0
練習問題3.45 面倒なので略。
練習問題3.47 面倒なので略。
練習問題3.52

  •  \quad \models \varphi」がいえるなら、左側にどんな論理式列を書いたっていい。
  •  \Gamma \models \quad」がいえるなら、右側にどんな論理式を書いたっていい。

練習問題3.53

  •  \quad \models \quad」は「解釈 I が存在しない」を意味するが、たとえその言語に原子命題が1つもなくとも I は存在するので、「 \quad \models \quad」は成立しない。

練習問題3.54

  •  \varphi_1, \, \cdots, \, \varphi_n \models \quad」は「I(\varphi_1)=1 かつ \cdots かつ I(\varphi_n)=1 である I が存在しない」を意味する。
    •  \varphi_1, \, \cdots, \, \varphi_n がすべて矛盾式(恒偽式)であれば「 \varphi_1, \, \cdots, \, \varphi_n \models \quad」である。
    • ただ、すべて矛盾式でなくとも、 \varphi_1, \, \cdots, \, \varphi_n に1つでも矛盾式が含まれれば「 \varphi_1, \, \cdots, \, \varphi_n \models \quad」である。
    • もっというと、個々の論理式は矛盾式でなくとも、 \varphi_1, \, \cdots, \, \varphi_n に含まれる2つ以上の論理式の組をすべて真にする解釈がなければ、「 \varphi_1, \, \cdots, \, \varphi_n \models \quad」である。
      • 例えば、 P \lnot P それぞれを真にする解釈はあるが、これらを同時に真にする解釈はない。

練習問題3.58 面倒なので略。
練習問題3.59 最初のだけ上のノート内で解いた。
練習問題3.63 面倒なので略。
練習問題3.64 面倒なので略。
練習問題3.66 面倒なので略。
練習問題3.67

  • 1)   (\lnot P \to P) \leftrightarrow P は恒真式。
  • 2)  左側が恒偽式なので、右側は何でもいい。
  • 3)   \lnot P \leftrightarrow (P \to \perp) は恒真式。
  • 4)   (P \to Q) \to (\lnot P \to \lnot Q) は恒真式ではないので意味論的妥当性は成立していない。

練習問題3.71 面倒なので略。
練習問題3.73 面倒なので略。

  • 1)  対偶律 + 二重否定律
  • 2)  分配律 + ドゥ・モルガンの法則
  • 3)  同一律 + ドゥ・モルガンの法則 + 二重否定律

練習問題3.80 面倒なので略。
練習問題3.84 何この問題。
身内の犯行であるならば、貞夫か光枝が犯人である。  P \to Q \lor R
貞夫が犯人ならば、犯人は財産目当てではない。  Q \to \lnot S
犯人が財産目当てならば、光枝は犯人ではない。  S \to \lnot R
したがって、身内の犯行であるならば、犯人は財産目当てではない。  P \to \lnot S
妥当性を示すべき推論: P \to Q \lor R, \; \; Q \to \lnot S, \: \: S \to \lnot R \; \; \models \; \; P \to \lnot S
以下に略解を記す。
1) Q \to \lnot S , \; \; R \to \lnot S \; \; \models \; \; Q \lor R \to \lnot S (構成的両刃論法)
2) Q \to \lnot S , \; \; S \to \lnot R \; \; \models \; \; Q \lor R \to \lnot S (1) の前提の一部を対偶律で置き換え)
3) P \to Q \lor R , \; \; Q \lor R \to \lnot S \; \; \models \; \; P \to \lnot S (推移律)
4) P \to Q \lor R , \; \; Q \to \lnot S , \; \; S \to \lnot R \; \; \models \; \; P \to \lnot S (2) と 3) をカット)
練習問題3.87
1)  \models \; \; \varphi \to \psi \; \; \; \Longleftrightarrow \; \; \; \varphi \; \; \models \; \; \psi (定理 3.60)
2)  \models \; \; \psi  \models \varphi と 1) をカット)
練習問題3.89 面倒なので略。
練習問題3.91
背理法以前にこの推論は妥当でない。出題ミス?
練習問題3.94
左側は0になっている行がないので連言標準形の手続きを進めることができないし、右側は1になっている行がないので選言標準形の手続きを進めることができないよね。
練習問題3.95 面倒なので略。
練習問題3.101 面倒なので略。
練習問題3.103 n項真理関数を別のn項真理関数で表現。

  • 1)   \varphi \to \psi \; = \! \! \! | | \! \! \! = \; \lnot(\varphi \land \lnot \psi)
  • 2)   \varphi \to \psi \; = \! \! \! | | \! \! \! = \; \lnot \varphi \lor \psi
  • 3)   \varphi \lor \psi \; = \! \! \! | | \! \! \! = \; (\varphi \to \psi) \to \psi
  • 4)   \varphi \land \psi \; = \! \! \! | | \! \! \! = \; ((\varphi \to \psi) \to \psi) \leftrightarrow (\varphi \leftrightarrow \psi)
  • 5)   \land \to のみでは表現できないことを示すのはすぐできなさそうなのでパス。

練習問題3.106 面倒なので略。
練習問題3.107
一項真理関数は原子命題を1つとって「そのまま返す」「裏返して返す」「1にして返す」「0にして返す」しかできない。
2つ目以降の原子命題を全く考慮できない。


所感

  • 以下の記事を書くときにペアノの公理の5番目ってなんでこんな浮いているんだろうと思ったけど、自然数の定義に自然数をつかってはいけないのでそんな感じにせざるをえない。たぶん。
  • それで、一階命題論理では集合の概念をつかっているけど、本来集合の概念自体が論理体系を整えた上にあるのに大丈夫?というのが心配になるけど、それについては集合の概念を回避できる意味論もあるらしい(35ページ注釈9)。
  • 意味論的同値の記号  = \! \! \! | | \! \! \! = ってこうですか。わかりません。
    = \! \! \! | | \! \! \! =