Lean4 でゲーム理論
MixedMatched/formalizing-game-theory というリポジトリでゲーム理論を Lean4 で形式化している人がいて、自分がやりたかったことはこうやればいいのか、と勉強になった。読んだ内容をメモとしてまとめておく、ファイルはこれ: https://github.com/MixedMatched/formalizing-game-theory/blob/0b35fc377f76a5b143bd3f2e6fd36027cdf1ee43/FormalizingGameTheory/Basic.lean
また、囚人のジレンマで両者黙秘はナッシュ均衡にならないことを示せたのでそれも書いておく。
用語はわかっていないため、wiki を参照しながら読んだ。
定義
効用 (Utility)
実数を val として持つ
戦略 (Strategy)
純粋戦略 (pure) と混合戦略 (mixed) を持つ帰納型で、戦略の集合として型を引数に取る
戦略の型を取るためゲームごとに自由に戦略を与えることができる、戦略と戦略の型は違うので注意。
例としてスタグハントゲームの戦略が与えられている
inductive StagHuntStrategies
| stag
| hare
もう一つの例としてはナッシュの要求ゲーム、実数の値を持つ、持てる値として 0 < で < 1 の条件がついている。
structure NashDemandStrategies := (demand : Real) (above_0: demand > 0) (below_1: demand < 1)
(構造体を値とその証明を持つものとして使うのが勉強になった)
プロファイル (Profile)
ゲーム理論では効用、戦略などの「一覧」をプロファイルと呼ぶ？
- 戦略プロファイル: プレイヤーごとに異なる戦略を取れるような型になっている
- 効用プロファイル:
- (L: List Type) という戦略型のリストをパラメータとしてとっている
- (utilities: List Utility) というフィールドも持ち、L と utitilies の長さが一致する
効用関数 (UtilityFunction)
効用関数は戦略プロファイルを受け取って、効用プロファイルを返す関数。
ゲーム (Game)
効用関数とプレイヤー数を受け取り、ゲームが定義できる、プレイヤーは少なくとも一人いるという条件がある
ナッシュ均衡 (NashEquilibrium)
ナッシュ均衡は戦略プロファイルから Prop への関数として与えられていて、そのプロファイルがナッシュ均衡であることを示す。
内容としては任意のプレイヤーの戦略を任意に変更した場合、そのプレイヤーの効用が低下することを、旧戦略プロファイルを一部書き換えて新戦略プロファイルを作り、新旧効用プロファイルのそのプレイヤーの値を比較することで示している。
具体例を眺める
混乱してきたので、具体例を見てみる。
- 囚人のジレンマの戦略は自白と黙秘の2つで、これは帰納型で定義されている。
- PL という変数を定義している、これはプレイヤーごとの戦略の型のリスト。
- 今回は同じだが、先行後攻で異なる戦略を取ることが可能
- 効用関数を定義している、中でやっていることは、
- 純粋/混合戦略の場合わけ
- 次にマッチしたプロファイルの要素を既知の値として扱っていいことを示す (これいる？)
- 最後にその組み合わせに応じて効用を返す
裏切り合いの原因
囚人のジレンマのよく知られている話として、両者が黙秘することは (パレート最適だが) ナッシュ均衡ではない、というものがある。
このことが案外簡単に示せたのでここに書いておく (リポジトリにも証明があったが途中だった)
theorem MyNotNashEquilibriumSilent : ¬ NashEquilibrium PL 2 PrisonersDilemmaGame PrisonersDilemmaSilentProfile := fun h_nash => let h_64: 6 ≤ 4 := h_nash (Fin.ofNat 0) (Strategy.pure ⟨PrisonersDilemmaStrategies.confess⟩) let nh_64: ¬ (6 ≤ 4) := not_le_of_gt ( (@Real.ratCast_lt 4 6).mpr ( by exact rfl ) ) absurd h_64 nh_64
両者黙秘でナッシュ均衡が成り立っていると仮定すると False になることを示せばいい。 プレイヤー0が自白すれば 6 、黙秘すれば 4 ということがわかっていて、ナッシュ均衡は任意のプレイヤーと戦略を取るので、 プレイヤー0と自白をわたすと 6 ≤ 4 が得られる。 そんなことはないということを愚直に示した。
