最近、オセロのAIを作ろうと思ってOCamlでαβ法を実装したのですが、実装にバグがあって思ったように性能が出ませんでした。この不具合が厄介で、合法手がちゃんと返っているので実際に対戦させてみないと悪い手を打っている事に気付けないのです。

こんな時はやはりCoqで証明を付けるに限ります。

準備

αβ法はミニマックス法に枝刈りを実装したものです。αβ法の正当性としてはミニマックス法と同じ結果を返す事が期待されますから、まずはミニマックス法を実装する事になります。ミニマックス法を実装する際に評価値の最小値と最大値を求める操作が必要になりますから、ここでは畳み込みによる実装とそれについての性質の証明を書きます。

Require Import List Relations ZArith Omega Program.

Section Maximum.
  Variable A : Set.
  Variable max : A -> A -> A.
  Definition maximum x xs := fold_left max xs x.

  Hypothesis max_select : forall x y, max x y = x \/ max x y = y.

  Theorem maximum_select xs : forall x, In (maximum x xs) (x :: xs).
  Proof.
    induction xs as [ | x xs ]; simpl; intros x'.
    - eauto.
    - destruct (max_select x' x) as [ Heq | Heq ];
        rewrite Heq;
        [ destruct (IHxs x')
        | destruct (IHxs x) ];
        eauto.
  Qed.

  Variable le : relation A.
  Hypothesis le_refl : forall x, le x x.
  Hypothesis le_trans : forall x y z, le x y -> le y z -> le x z.
  Hypothesis max_join : forall x y, le x (max x y) /\ le y (max x y).

  Theorem maximum_join xs : forall x y, In y (x :: xs) -> le y (maximum x xs).
  Proof.
    induction xs as [ | x xs ]; simpl.
    - intros ? ? [ ? | [] ]; subst; eauto.
    - intros x' y [ ? | [ ? | ? ] ]; subst.
      + destruct (max_join y x).
        specialize (IHxs (max y x) _ (or_introl eq_refl)).
        eauto.
      + destruct (max_join x' y).
        specialize (IHxs (max x' y) _ (or_introl eq_refl)).
        eauto.
      + apply IHxs; simpl.
        eauto.
  Qed.

  Definition maximum_spec x xs := conj (maximum_select xs x) (maximum_join xs x).

  Definition maximum_concrete x xs :
    fold_left max xs x = maximum x xs := eq_refl.
End Maximum.

maximumがリスト中の最大値を求める関数で、maximumがきちんとリスト中の最大値を返している事の証明がmaximum_specです。帰納法を回す時に畳み込みを用いた表現に戻せると嬉しいのですが、実装を隠蔽する（真面目にモジュール使ったりしてないから見えてるけど）ためにmaximum_concreteを用意しています。

maximumは色々な型に用いられる汎用的な関数として定義されていますが、ここで最大値を求めたいのは盤面の評価値でしたね。後でネガマックス法に発展させる事とOmegaを使う事を考えて盤面の評価値は整数で表現するならば、最大の評価値と最小の評価値を求める関数は次のように定義されます。

Section ZMaximum.
  Local Open Scope Z_scope.

  Definition Zmaximum := maximum _ Z.max.
  Definition Zminimum := maximum _ Z.min.

  Corollary Zmaximum_spec : forall x xs,
    (In (Zmaximum x xs) (x :: xs)) /\
    (forall y, In y (x :: xs) -> y <= Zmaximum x xs).
  Proof.
    apply maximum_spec; try (intros; omega).
    - intros x y.
      destruct (Zmax_spec x y) as [[]|[]]; omega. 
    - intros x y.
      destruct (Zmax_spec x y) as [[]|[]]; omega.
  Qed.

  Corollary Zminimum_spec : forall x xs,
    In (Zminimum x xs) (x :: xs) /\
    (forall y, In y (x :: xs) -> y >= Zminimum x xs).
  Proof.
    apply maximum_spec; try (intros; omega).
    - intros x y.
      destruct (Zmin_spec x y) as [[]|[]]; omega. 
    - intros x y.
      destruct (Zmin_spec x y) as [[]|[]]; omega.
  Qed.

  Corollary neg_Zmaximum_distr x xs :
    - Zmaximum x xs = Zminimum (- x) (map Z.opp xs).
  Proof.
    destruct (Zmaximum_spec x xs) as [ HmaxIn Hmax ].
    destruct (Zminimum_spec (- x) (map Z.opp xs)) as [ HminIn Hmin ].

    assert (HmaxIn' : In (- Zmaximum x xs) (map Z.opp (x :: xs))).
    { apply in_map. eauto. }
    specialize (Hmin _ HmaxIn').

    assert (HminIn' : In (- Zminimum (- x) (map Z.opp xs)) (map Z.opp (map Z.opp (x :: xs)))).
    { apply in_map. eauto. }
    rewrite map_map in HminIn'.
    rewrite map_ext with (f := fun x => - - x) (g := id) in HminIn'
      by (unfold id; intros; omega).
    rewrite map_id in HminIn'.
    specialize (Hmax _ HminIn').

    omega.
  Qed.

  Corollary neg_Zminimum_distr x xs :
    - Zminimum x xs = Zmaximum (- x) (map Z.opp xs).
  Proof.
    replace (Zminimum x xs) with (Zminimum (- - x) (map Z.opp (map Z.opp xs))).
    - rewrite <- neg_Zmaximum_distr.
      omega.
    - f_equal.
      + omega.
      + rewrite <- map_id.
        repeat rewrite map_map.
        apply map_ext.
        intros.
        omega.
  Qed.

  Corollary Zmaximum_concrete : forall x xs,
    fold_left Z.max xs x = Zmaximum x xs.
  Proof. apply maximum_concrete. Qed.
End ZMaximum.

Zmaximumが評価値の最大値を求める関数で、Zminimumが評価値の最小値を求める関数です。これらが正しく最大値を返している事を表すのが系Zmaximum_specであったりZminimum_specであったりする訳です。また、ネガマックス法についての性質を証明する際に、符号を反転してから最大値を取ると符号を反転した最小値が取れる事を使いたくなるので証明しています。

ミニマックス法の実装

準備が整ったのでミニマックス法を実装しましょう。

まずは盤面と評価関数についての諸々の定義。

Section MinMax.
  Local Open Scope Z_scope.

  Variable board : Set.
  Variable succ : board -> list board.
  Variable eval : board -> Z.

boardは名前を見れば分かるように、盤面を表す型です。
succは与えられた盤面で一手打って遷移できる盤面のリストを返す関数。succ bが空リストを返した時がゲーム終了のつもり。
evalは名前の通り評価関数です。

これらを用いてWikipediaでも見ながらミニマックス法を実装するならこんな感じになるでしょう。

Fixpoint minimax b n :=
  match n with
  | O => eval b
  | S n =>
      match succ b with
      | [] => eval b
      | b :: bs =>
          Zmaximum 
            (minimax' b n)
            (map (fun b => minimax' b n) bs)
      end
  end
with minimax' b n :=
  match n with
  | O => eval b
  | S n =>
      match succ b with
      | [] => eval b
      | b :: bs =>
          Zminimum
            (minimax b n)
            (map (fun b => minimax b n) bs)
      end
  end.

minimaxが自分の手を考える関数で、minimax'が相手の手を考える関数。相手は自分にとって最悪の手を打ってくると考えて所定の数だけ手を読んでいますね。

ネガマックス法の実装・検証

ミニマックス法の実装を見ると、どうも重複したコードが多いように思えませんか。 minimaxは評価値が最大となるように手を選んでいるのに対し、minimax'は評価値が最小になるように手を選んでいる点を除けば両者はほぼ同じコードですよね。
符号を反転してから最大値を取れば最小値の符号を反転したものが得られる事を利用し、ミニマックス法における冗長なコードを排除する手法がネガマックス法です。コードにするとこんな感じでしょうか。

Fixpoint negmax (turn : bool) b n :=
  match n with
  | O =>
      if turn then eval b
      else - eval b
  | S n =>
      match succ b with
      | [] =>
          if turn then eval b
          else - eval b
      | b :: bs =>
          Zmaximum
            (- negmax (negb turn) b n)
            (map Z.opp (map (fun b => negmax (negb turn) b n) bs))
      end
  end.

注意すべき点は手番によって評価値の符号を変えなければならない点です。先ほどのようなミニマックス法と対応している事を示そうと思った場合、これを怠ると証明に行き詰ってしまいます。*1

新しい関数を実装した際にまずすべき事と言えば証明。ネガマックス法がちゃんとミニマックス法と対応している事を証明しましょう。

Theorem negmax_corresponds_minimax n : forall b turn,
  negmax turn b n = if turn then minimax b n else - minimax' b n.
Proof.
  induction n as [ | n ]; simpl.
  - intros ? []; reflexivity.
  - intros b0 [];
      destruct (succ b0); eauto.
    + rewrite map_map.
      f_equal; [ | apply map_ext; intros ? ];
        rewrite (IHn _); simpl;
        omega.
    + rewrite <- neg_Zminimum_distr.
      do 2 f_equal; [ | apply map_ext; intros ? ];
        rewrite (IHn _); simpl;
        omega.
Qed.

最大の評価値を求める操作についての性質はもう補題として立ててありますから、帰納法を回すだけですね。

αβ法の実装・検証

ミニマックス法（やネガマックス法）は考え得る手全てに対して先読みを行うわけですが、こちらがある程度以上良い手を選択しても、相手はその盤面に辿り付くような手を選択してくれない事が考えられます。それならば相手が選んでくれない事が分かった時点で探索を打ち切ってしまおうと言うのがαβ法です。

例によってWikipediaでも参考にしながら実装するならこんな感じでしょうか。

Definition Zmaximum_with_alpha {A} alphabeta alpha beta := (fix Zmaximum_with_alpha alpha (xs : list A) :=
  match xs with
  | nil => alpha
  | x :: xs =>
      let value := alphabeta alpha x in
      if Z_le_dec beta value then value
      else Zmaximum_with_alpha (Z.max alpha value) xs
  end) alpha.

Fixpoint alphabeta (turn : bool) alpha beta b n :=
  match n with
  | O => 
      if turn then eval b
      else - eval b
  | S n =>
      match succ b with
      | [] => 
          if turn then eval b
          else - eval b
      | bs =>
          Zmaximum_with_alpha
            (fun alpha b => - alphabeta (negb turn) (- beta) (- alpha) b n)
            alpha beta bs
      end
  end.

枝刈りをしなければならないのと、選択され得る最小の評価値alphaを引き回さなければならない都合上畳み込みで書けなくてつらい。再帰関数の中で匿名の再帰関数を使うと、内側の再帰関数についての性質が必要になった時のsubgoalがグロい事になるので名前をつけてやりましょう。

αβ法の正当性を証明するにあたって、まずは内側の再帰関数についての性質を示しましょう。これが前に述べた、帰納法の都合上maximumを畳み込みとして表したくなる場面ですね。

Lemma Zmaximum_with_alpha_spec_aux A minimax alphabeta beta xs :
  (forall alpha (x : A),
    alpha < beta ->
    minimax x <= alpha /\ alphabeta alpha x <= alpha \/
    alpha <= minimax x /\ minimax x = alphabeta alpha x /\ minimax x < beta \/
    beta <= minimax x /\ beta <= alphabeta alpha x) ->
  forall alpha,
  alpha < beta ->
  fold_left Z.max (map minimax xs) alpha = Zmaximum_with_alpha alphabeta alpha beta xs /\
  fold_left Z.max (map minimax xs) alpha < beta \/
  beta <= fold_left Z.max (map minimax xs) alpha /\ beta <= Zmaximum_with_alpha alphabeta alpha beta xs.
Proof.
  intros Halphabeta_spec.
  induction xs as [ | x xs ]; simpl; intros alpha ?.
  - omega.
  - destruct (Halphabeta_spec alpha x) as [ [ ] | [ [ ? [ Heq ] ] | [ ] ]]; eauto.
    + destruct (Z_le_dec beta (alphabeta alpha x)); [ omega | ].
      repeat rewrite Z.max_l by assumption.
      apply IHxs; assumption.
    + rewrite <- Heq.
      destruct (Z_le_dec beta (minimax x)); [ omega | ].
      rewrite Z.max_r by omega.
      apply IHxs; assumption.
    + right.
      destruct (Z_le_dec beta (alphabeta alpha x)); [ | omega ].
      rewrite Z.max_r by omega.
      split.
      * rewrite Zmaximum_concrete.
        specialize (proj2 (Zmaximum_spec (minimax x) (map minimax xs)) _ (or_introl eq_refl)).
        omega.
      * assumption.
Qed.

Corollary Zmaximum_with_alpha_spec A minimax alphabeta alpha beta xs :
  alpha < beta ->
  (forall alpha (x : A),
    alpha < beta ->
    minimax x <= alpha /\ alphabeta alpha x <= alpha \/
    alpha <= minimax x /\ minimax x = alphabeta alpha x /\ minimax x < beta \/
    beta <= minimax x /\ beta <= alphabeta alpha x) ->
  alpha <= Zmaximum alpha (map minimax xs) /\
  Zmaximum alpha (map minimax xs) = Zmaximum_with_alpha alphabeta alpha beta xs /\
  Zmaximum alpha (map minimax xs) < beta \/
  beta <= Zmaximum alpha (map minimax xs) /\ beta <= Zmaximum_with_alpha alphabeta alpha beta xs.
Proof.
  intros Halphabeta Halphabeta_spec.
  rewrite <- Zmaximum_concrete.
  destruct (Zmaximum_with_alpha_spec_aux _ _ _ _ xs Halphabeta_spec _ Halphabeta) as [ [ ] | [ ] ];
    [ left | right ];
    repeat split; eauto.
  rewrite Zmaximum_concrete.
  apply (proj2 (Zmaximum_spec _ _)). left.
  eauto.
Qed.

最後に、αβ法の正当性にあたる定理を証明します。
内側の再帰関数は現在の盤面から一手打って得られる盤面の評価値に、選択され得る最小の評価値alphaを加えてから最小値を取っているようなものですから、 alphaを含めずに最大値を取っていたミニマックス法との対応を証明する際には面倒な手順が必要になります。

  Theorem alphabeta_corresponds_negmax : forall n b beta turn alpha,
    alpha < beta ->
    negmax turn b n <= alpha /\ alphabeta turn alpha beta b n <= alpha \/
    alpha <= negmax turn b n /\ negmax turn b n = alphabeta turn alpha beta b n /\ negmax turn b n < beta \/
    beta <= negmax turn b n /\ beta <= alphabeta turn alpha beta b n.
  Proof.
    intros n.
    induction n as [ | n ]; simpl; intros b beta.
    - intros; omega.
    - destruct (succ b) as [ | b_ bs ]; intros turn alpha ?.
      + omega.
      + rewrite map_map.
        destruct (Z_lt_dec alpha (Zmaximum (- negmax (negb turn) b_ n)
          (map (fun b => - negmax (negb turn) b n) bs))) as [ | ].
        * right.
          replace (Zmaximum (- negmax (negb turn) b_ n) (map (fun x => - negmax (negb turn) x n) bs))
             with (Zmaximum alpha (map (fun x => - negmax (negb turn) x n) (b_ :: bs))).
          { apply (Zmaximum_with_alpha_spec _ _
              (fun alpha b => - alphabeta (negb turn) (- beta) (- alpha) b n) _ beta (b_ :: bs)); eauto.
            intros alpha0 b0 ?.
            destruct (IHn b0 (- alpha0) (negb turn) (- beta)) as [ [] | [ [ ? [] ] | [ ] ] ]; omega. }
          { destruct (Zmaximum_spec (- negmax (negb turn) b_ n) (map (fun b => - negmax (negb turn) b n) bs)) as [ HIn1 Hmax1 ].
            destruct (Zmaximum_spec alpha (map (fun b => - negmax (negb turn) b n) (b_ :: bs))) as [ [ | HIn2 ] Hmax2 ];
              specialize (Hmax2 _ (or_intror HIn1)).
            - omega.
            - specialize (Hmax1 _ HIn2).
              omega. }
        * left.
          assert (Zmaximum alpha (map (fun b => - negmax (negb turn) b n) (b_ :: bs)) = alpha).
          { destruct (Zmaximum_spec (- negmax (negb turn) b_ n) (map (fun b => - negmax (negb turn) b n) bs)) as [ HIn1 Hmax1 ].
            destruct (Zmaximum_spec alpha (map (fun b => - negmax (negb turn) b n) (b_ :: bs))) as [ [ | HIn2 ] Hmax2 ].
            - omega.
            - generalize (Hmax2 _ (or_intror HIn1)). intros.
              specialize (Hmax2 _ (or_introl eq_refl)).
              specialize (Hmax1 _ HIn2).
              omega. }
          destruct (Zmaximum_with_alpha_spec _
            (fun b => - negmax (negb turn) b n)
            (fun alpha b => - alphabeta (negb turn) (- beta) (- alpha) b n) alpha beta (b_ :: bs)) as [ [ ? [ ] ] | [ ] ]; simpl in *; try omega.
          intros alpha0 b0 ?.
          destruct (IHn b0 (- alpha0) (negb turn) (- beta)) as [ [] | [ [ ? [] ] | [ ] ] ]; omega.
  Qed.
End MinMax.

まとめ

αβ法がミニマックス法と対応した値を返している事が証明できました。これでビットボードまで実装したAIの性能が出なくてビットボードの実装をひたすらデバッグしたものの、バグっていたのはαβ法の実装で脱力する、なんて事も無くなる事でしょう。*2
今回書いたCoqによる証明はGitHubに上げてありますので、参照したい方はそちらをどうぞ。

余談ですが、αβ法の正当性を証明する時に帰納法が回るように一般化するのがめっちゃつらかったです。

*1:日本語版Wikipediaの疑似コードはこの点の記述が足りていないのではないか？英語版の方はちゃんと手番によって符号を変える点が表現されていた

*2:とてもつらい

fetburner.core

コアダンプ

αβ法に証明を付ける

準備

ミニマックス法の実装

ネガマックス法の実装・検証

αβ法の実装・検証

まとめ