KLabGames Tech Blog

KLabは、多くのスマートフォン向けゲームを開発・提供しています。 スマートフォン向けゲームの開発と運用は、Webソーシャルゲームと比べて格段に複雑で、またコンシューマゲーム開発とも異なったノウハウが求められる領域もあります。 このブログでは、KLabのゲーム開発・運用の中で培われた様々な技術や挑戦とそのノウハウについて、広く紹介していきます。

カテゴリ: その他

このエントリーは、KLab Advent Calendar 2017 の12/4の記事です。

今年のISUCONはKLabが作問するということで、ゲームが題材だと予想していた方も多かったと思います。 その期待(?)に応えるべく、本選ではCookie Clickerを元にしたゲームを出題しました。 これを複数人で協力プレイできるようにして、WebSocketを使っていて、クッキーではなく椅子を増やし、椅子の数が多倍長整数になる、というゲームでした。

この記事では @hasi_t がISUCON7本選の作問でやったことを書きます。

プロトタイプ作成

まずプロトタイプ作成を担当しました。 Cookie Clickerを元にする、という案が出ていたので、自分がやりたい要素を入れたプロトタイプを作りました。

一つ目の要素は未来計算と操作遅延です。 サーバが未来の値を計算できるようなデータを返し、クライアント側で各時点での値を計算するようにする、という設計です。 そして操作を遅延させることで可能な限り同時刻での見え方が同じになるようにしました。 このような設計によって通信頻度を下げる、というのは、 CEDEC 2015で発表したことの実践で(参考)、 それを実現するための技術や開発体制について普段の業務で日頃考えていたりするのですが、 その実態を見せる機会と考え、この要素を入れました。

二つ目の要素は多倍長計算です。 以前、 ICFPC 2016 というプログラミングコンテストに参加したときに多倍長有理数を使って、 こういう多倍長計算を使った問題を作りたいと思っていた、というのがあります。 あと、メモリを消費させて、ただキャッシュするだけでは駄目なようにしたい、というのも考えていました。

ちなみに、作問チームのうち3人 (@mecha_g3, @___Johniel, @hasi_t) はここ4年ほど、この3人だけではないですが、DiamondPrincessというチームでそのICFPCに参加しています。そして今年は2位でした!

プロトタイプの時点ではWebSocketではなく、普通のHTTP通信で、サーバはPHPで雑に書いた状態でした。 ver0とver1を作ったのですが、ver0の時点ではミリ秒単位ではなく秒単位だったりしました。 あと、命名が雑すぎて抽象的な一文字変数名だらけになっていたので、本実装時に名前の調整が結構大変でした。

本実装作成

WebSocketを使うことになり、初期実装は他の人に任せて、 ゲーム画面を作るためにJavaScriptコードをロジックとビューに分割したり、 いい感じのフォントを探したりしていました。

ベンチマーカのバリデーション作成

未来計算の設計時点で、ベンチマーカから見て検証可能にすることを考えていました。 誤差を許容するには、許容範囲やそれに合わせた計算など、考えることが多く、それを避けた結果、厳密な検証になりました。 そのため、値が1でもずれるとfailするという厳しいコンテストになりました。

負荷走行前の検証はaddIsu, buyItemに対するレスポンスが必ず存在するので良かったのですが、 負荷走行後の検証はタイムアウトなどでレスポンスが無い場合を考える必要があり、 上限と下限を考えて検証する必要があってちょっと大変でした。

エラーメッセージを参加者にとってわかりやすくする、という作業をするのがぎりぎりになってしまい、 初期実装作成者には苦労をかけてしまいました。

ベンチマーカのチューニング

当然といえば当然ですが、初期実装そのままで検証していたら、 負荷走行後の検証の実行時間が長すぎる問題が発生し、高速化をしました。

やったこととしては、指数表記変換関数の高速化、item価格と生産速度のキャッシュ、1000回ループの回避、指数表記変換関数内の10のn乗のキャッシュ、addingの累積和を使う、などです。

実装は以下の通りです。指数表記変換関数(big2exp)はutil.goにあります。

とりあえず、Go言語のbig.Intは、つらい、という感想でした。

マスタデータ調整

いい感じのマスタデータにしないと多倍長使う意味が無い、と思っていたので、 1分間のベンチマークで10の10万乗ぐらいまで到達できるようにマスタデータを調整しました。 調子に乗って1個目の購入価格が10の10万乗ぐらいあるアイテムを作ったら、 初期実装の時点でそこが重すぎて、リハーサルやってみたけどまともにチューニングできない、 みたいなことも起きたりして申し訳ない感じだったりしました。

ちなみに、Excelで値を調整して、Pythonスクリプトで雑なシミュレーションをする、ということをしていました。 もちろん、値を直接扱えないので、対数をとって計算していました。

おわりに

参加者の皆様、運営の皆様、お疲れ様でした! いろいろご迷惑おかけしましたが、出題することができて嬉しく思っています。 ありがとうございました!

(本稿はKLab Advent Calendar 2017 の3日目の記事になります)

昨今、電子工作やマイコンプログラミングへのハードルが急激に下がっているという印象があります。皆さんの身の周りでもArduinoやRaspberry Piに秋葉原で買ったセンサーを繋いで遊んでいる人がいるのではないでしょうか?

私の所属しているKLab株式会社にも「Make部」という部活があり、毎年Maker Faire Tokyoで各個人が作品を展示したり社内勉強会を開いたりして、業務と無関係に電子工作を楽しんでいたりします。

ふつうのLinuxマシンでもセンサー類を扱いたい

とはいえ、ArduinoもRaspberry Piも普段使っているLinuxマシンやmacOSマシンとは随分異なる環境です。ふつうのLinuxマシンにセンサーを接続して、気軽に扱えないものでしょうか?

Raspberry Piでセンサー類を簡単に扱えるのは、GPIOインターフェースが存在するためです。GPIOピンと各種センサー類やサーボモータなどを接続することで、Linux+電子工作の組み合わせが簡単に実現できるよ、というのがRaspberry Piの強みだと言えるでしょう。

Raspberry PiのGPIOピン

一方で、多くのLinuxマシンにはGPIOインターフェースが存在しません。たとえばUSB to I2C変換モジュールを使えばLinuxマシンでも電子工作的な遊びはできますが、追加の出費が必要ならRaspberry Piを買った方がマシだよ、となってしまいそうです。

本稿では、DigiTempを使ってLinuxマシンで比較的安価に温度センサーを扱う方法を紹介します。DigiTempはLinuxのシリアル通信インターフェース経由で1-Wire接続のセンサーを扱うOSSで、多くのLinuxディストリビューションで標準パッケージとして採用されています。

ソフトウェアのインストール

まずはソフトウェアのインストールをしましょう。大抵の環境でDigiTempはコマンド一発で入るはずです。

Debian系なら apt でインストールできます。

$ sudo apt install digitemp

RedHat系は yum でインストールできます。

$ sudo yum install digitemp

macOSでも遊べます。Homebrewからインストールしましょう。

$ brew install digitemp

後述するようにシリアル通信ドライバも必要です。こちらは利用するシリアル変換ICに応じて適切なドライバをインストールしてください。

ハードウェアの準備

当然ですが、ソフトウェアだけで外気温の測定はできません。DigiTempの利用には下記のような準備が必要です。

USB to シリアル変換モジュール

USBからシリアル通信(UART)への変換モジュールです。Arduinoで遊んだことがあれば必ず1個は持っているのではないでしょうか。変換ICとしてはFTDI社のFT232RLなどが有名ですが、他にもSilicon Labs社CP2102やProlific社 PL2303を採用した変換モジュールも容易に入手できます。

ちなみに私はCP2102ベースの変換モジュールを利用しています。これはeBayで1.15ドルでした。

CP2102 USB to シリアル変換モジュール

FTDI製ICを使っているモジュールであればドライバは標準でインストールされていることが多いかもしれません。それ以外の場合は手動でドライバをインストールする必要があるはずです。

温度センサ DS18B20

DS18B20はMaxim Integrated Products社製の温度センサです。秋月で買うと1個250円ですが、eBayなどを探せばもっと安いものも見つかります。

DS18B20

このセンサーは1-WireというMaxim独自のプロトコルで動作します。このプロトコルがUART経由で扱う上でのキモです。1-Wireはデータレートが低速かつ通信線1本で動作するので、UARTからでもドライブできるのです。他のプロトコルのセンサーであれば何らかのICが必須になるでしょう。

UARTとDS18B20の接続用ボード

UARTとDS18B20を直結しても動くことは動くらしいのですが、逆流防止などの用心のため、簡単な回路を工作してみました。

UART to DS18B20 接続用ボード

これはdword1511/onewire-over-uartで紹介されている下記の回路図を元に作成したものです。

回路図

材料は下記の通りです。

  • ユニバーサル基板
  • L型ピンソケット(1×6、メス)
  • 5.1kΩ 抵抗
  • スイッチングダイオード 1N4148
  • ポリウレタン銅線(配線用)

動かしてみる

これらを組み合わせると次のような見た目になります。思ったより場所を取る感じの仕上がりになってしまいました。

完成図

これをLinuxマシンのUSBに接続して、先ほどインストールしたDigiTempを起動すると温度が取れます。

コマンドの使い方として、まずは-wオプションを指定して1-Wireデバイスのスキャンを行う必要があります。-sオプションはシリアルポートの指定です。

$ /usr/bin/digitemp_DS9097 -s/dev/ttyUSB0 -w
DigiTemp v3.7.1 Copyright 1996-2015 by Brian C. Lane
GNU General Public License v2.0 - http://www.digitemp.com
Turning off all DS2409 Couplers
.
Devices on the Main LAN
28FF933161150389 : DS18B20 Temperature Sensor

これで接続されているセンサーの情報が$HOME/.digitemprcに記録され、次回以降の起動でこの情報を参照するようになります。

$ /usr/bin/digitemp_DS9097 -a -d 2 -n 5
DigiTemp v3.7.1 Copyright 1996-2015 by Brian C. Lane
GNU General Public License v2.0 - http://www.digitemp.com
Dec 02 21:21:27 Sensor 0 C: 21.50 F: 70.70
Dec 02 21:21:29 Sensor 0 C: 21.56 F: 70.81
Dec 02 21:21:31 Sensor 0 C: 21.50 F: 70.70
Dec 02 21:21:33 Sensor 0 C: 21.50 F: 70.70
Dec 02 21:21:35 Sensor 0 C: 21.44 F: 70.59

上記は2秒間隔でセンサーの値を5回取得する指定です。摂氏と華氏で温度が取れているのがわかります。

ちなみに、筆者はこれを家のLinuxルータに刺した上で取得した値をMackerelに書き出しています。

温度変化グラフ

上記のグラフが作りたいだけならRaspberry Piで温度センサーを扱った方が楽なのでは?と思われるかもしれません。理屈で言えばそうかもしれませんが、個人的にRaspberry Piは長期間電源を入れっぱなしにする気が起きないので、ふつうのLinuxマシンで運用できることに価値があるように感じています。同じ感覚の方が他にいらっしゃるかはわかりませんが…。

まとめ

  • DigiTempというLinux/macOS上で温度センサーDS18B20を扱うOSSを紹介しました
    • シリアル通信(UART)経由で1-Wireセンサーをドライブできます
    • 多くのLinuxディストリビューションで標準パッケージ採用されています
  • Raspberry Piで同じことをするより適用範囲が広かったり長期運用しやすかったりするかもしれません

@hnw

こんにちは、@trigottです。この記事では、社内で行っている Agda ハンズオンの紹介をします。

はじめに

Agda とは、依存型の使える関数型プログラミング言語、あるいは定理証明支援系です。Coq などとは違いタクティックは使わず証明項を直接記述するスタイルですが、Emacs 上で対話的に証明を進めるためのインタフェースが用意されているため、効率的に証明を進めることができます。Agda で n * 2n + n が等しいことを証明する動画を撮影してみました。雰囲気がつかめれば幸いです。

KLab では月に1回 ALM(All Layers Meeting)という社内勉強会を開催しています。学生のころから Agda が好きで触っていたこともあって、Agda に関する発表をしたところ、先輩からハンズオンを開いてほしいということを言われました。ハンズオンとかやったことないし、Agda も人に教えられるほどではないし・・・と最初は不安だったのですが、まあ全3回くらいでやってみよう、という軽い気持ちで開催することにしました。社内から参加者を募り、集まるか不安でしたが5人の方が参加してくれることになりました。この勉強会は昨年の10月から始まり、現在も継続中です。

ハンズオンということで、一人で進められるような資料を作成しました。具体的には、資料は Agda のプログラムとして実行可能なファイルで、コメントとして説明を記載し、さらに演習として、埋めるべき箇所を指定したプログラムを所々に配置しています(Software Foundations の真似をしました)。演習の問題は以下のように作成しました。

-- ==================================================================
-- Exercise: (2 star) app-assoc
-- _++_ の結合法則を証明してください。_++_ は右結合なので、xs ++ ys ++ zs
-- は xs ++ (ys ++ zs) と解釈されます。
-- ==================================================================

app-assoc : ∀ {A : Set} (xs ys zs : List A)
            → xs ++ ys ++ zs ≡ (xs ++ ys) ++ zs
app-assoc = ?

2 star は問題の難易度を示しています。特に基準を設けず難易度付をしてしまったせいで、あてになりません。コメントに問題の解説を書いています。問題の本文は実際の Agda のプログラムです。基本的にどれも証明すべき命題=プログラムの型だけを記述し、値は ? だけの未完成なものになっています。Agda ではプログラムの代わりに ? を書くことができ、プログラムとしては不完全ですがコンパイルを通すことができます。なので、まだ解けていない問題がある状態でプログラムをコンパイルしてもエラーにはなりません。また、Emacs でファイルをロードすると埋めるべき ? の一覧が表示されるので、現在の進捗が分かります。

資料は https://github.com/krtx/agda-handson にあります。最初は全3回くらいで終わる予定でしたが、資料を作成しているうちに内容が膨らみ、気づいたらDay1からDay6までの全6部構成になっていました。以下、各ファイルについて解説と作成時の苦労について書きます。

Day1

一番最初に作ったので、一番気合が入っていて、一番長いです。真偽値と自然数を題材にして Agda での基本的な定理証明の仕方を解説しています。≡などの文字の入力の仕方や、Emacs でのコマンドを使った対話的な証明のやり方などです(そう、このハンズオンは Emacs が前提です)。Day1 の最後は、自然数の大小関係を定める2つのデータ型が互いに等価であることを証明する問題になっています。Day1 と言いつつ、1日ではまったく終わりませんでした。

Day2

等しいことの証明をする際によく使われる Rewrite パターンと equational reasoning combinator というものについて(あとおまけで自動で証明してくれる SemiringSolver について)解説しています。Day2 の演習の最後は (a + b) * (c + d)(a * c + b * c) + (a * d + b * d) が等しいことを証明する問題です。Rewrite パターンか equational reasoning combinator を使ってこの問題が証明できれば、初等的なものに限れば等しいことの証明は大体できるのではないでしょうか。

Day3

新しい構造としてリストの解説を、またリストに関する証明を題材として With abstraction の解説をしています。真偽値→自然数→リストという順番でデータ構造を紹介するのは、構造が徐々に複雑になっていくという点で自然に難易度を上げることができているのではないかと思います。rev-involutiverev-injective は Software Foundations のものを真似しています。with abstraction が説明できたので with abstraction を使うことで実現できる inspect パターンというものも説明しようと思ったのですが、例が思い浮かばず断念しました。

Day4

レコード型及び依存型を伴うレコード型について解説しています。レコード型の例として二次元平面上の点を定義し、それを使ったマンハッタン距離に関する性質の証明を演習としています。マンハッタン距離が三角不等式を満たすことの証明はやってみると意外と面倒なのですが、面白かったのでそのまま演習に残しています。ただレコード型の理解に貢献する問題ではないので、余力がある人向けとなっています。この辺から例を考えるのがかなりしんどくなっています。

Day5

偽及び Absurd パターンの解説をしています。偽についての説明は、自分の力量不足で怪しいかもしれません。演習には古典論理にまつわる命題をいくつか与えており、そのために必要なので「かつ」と「または」についても解説しています。

Day6

最後は新しいことはなしで、これまでの知識を使って正しいソートアルゴリズムを定義するという演習です。どこまでヒントを出すかは悩みましたが、ソート済みであることなどの定義はすべて与えて、ソートするプログラムだけを書いてもらう形にしました。insert-sort は単にソートするだけでなく、命題を見ると結果のリストがソート済みであることも要求しています。想定解法では、ソートをしつつ証明も同時に行うようにしています。このように、証明とプログラムが一緒になった証明のスタイルを intrinsic な証明と呼び、一方プログラムを単体で書き、それに対する証明を別で与えるスタイルを extrinsic な証明と呼びます。Agda では intrinsic な証明が多いようなので、insert-sort の型もそれを推奨するように作ってみました(ただ説明がないので、ちょっと中途半端...)。

やってみての感想

実際にハンズオンをしていく中で出てきた感想です。

refl が分からん

Day1 である2つの項が等しいとはどういうことか、またそれはどのようにして証明できるか、について説明したのですが、これが分からないという意見が非常に多かったです。Agda では等しいという関係 _≡_ は以下のように定義できます。

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {x} → x ≡ x

以下のような点から、_≡_ を理解するのは非常に難しかったようです。

  • 関係をデータ型として定義するというのは、普通のプログラミングでは出てこない考え方であること
  • _≡_ という型自体が値を受け取っていること(依存型)
  • refl の引数が implicit になっていること
  • Agda が値を比較する際には正規形に計算してから比較するため、プログラムの字面とは違う値が比較されていること

等しいというのはとても馴染み深い関係のように思えるにもかかわらず、初心者にとっては超えるべきハードルがいくつもあります。自分でも説明に窮する場面が何度もあり、まだまだ十分に理解できていないなと感じました。もう少し簡単な関係から始めるべきだったかもしれません。

Agda がどこまで計算してくれるのか分からん

Day1 では足し算を以下のように定義しています。

_+_ : ℕ → ℕ → ℕ
zero    + m = m
(suc n) + m = suc (n + m)

このため、以下の命題中に現れる (suc x) + y という項は suc (x + y) に計算されます。

prop : ∀ x y → (suc x) + y ≡ suc (x + y)
prop = refl

refl は対応する命題の左辺と右辺が同一の項であることを要求します。(suc x) + y という項と suc (x + y) という項は構文解析をした時点では違う形ですが、Agda によって (suc x) + ysuc (x + y) に計算されるため、refl を使うことができるようになります。このように、Agda が自動で計算を行うということを知っていないと、なぜ証明が通るのかが理解できません。また、足し算の定義を覚えていないと、どこまで計算が進むかも分かりません。自分もこの辺りの理解が甘く、テキストには解説を書けていませんでした。

名前が読めない

Agda の標準ライブラリを見ていると、n ≤ m → n ≤ suc m という命題に n≤m⇒n≤sm という名前をつけるなど、空白だけ詰めた名前を採用していることが多いです。Agda では : など一部の例外を除いて基本的に空白で区切られるため、n≤m⇒n≤sm のような名前でもひと続きの識別子として認識されます。このハンズオンでも同様の命名法を採用したのですが、やはり n≤m⇒n≤sm はひと続きの名前としては認識しづらいとのことでした。

rewrite はロードが必要

rewrite は 文脈中のある項を別の項で置き換えるパターンです。以下の例のように使います。

posulate
  A : Set
  a : A
  b : A
  eq : a ≡ b

lem : suc a ≡ suc b
lem rewrite eq = {! ここの命題は suc b = suc b となる !}

ただし、rewrite を書いただけでは反映されません。rewrite を書いてからロードして初めて文脈に反映されます。テキストのなかでも注意がなかったため、ここで戸惑う参加者の方が多かったです。

reasoning combinator はよしなに推論してくれない

Day2 ではある2つの項が等しいという命題について、rewrite と reasoning combinator それぞれを使った証明法を解説しています。上述の例と同じ命題を reasoning combinator を使って証明すると以下のようになります。

lem′ : suc a ≡ suc b
lem′ = begin
  suc a
    ≡⟨ cong suc eq ⟩
  suc b
    ∎

rewrite の場合は eq だけを指定すればよかったのですが、reasoning combinator を使う場合は suc がついていることを明示してあげる必要があります。

reasoning combinator は対象となる項を書く必要があり、また完全な証明を与えなければならないため、冗長な記述になります。ですが、冗長になっている分、説明が多いためこちらのほうが分かりやすくなっています。実際参加者の間では rewrite による証明よりも reasoning combinator を使ったほうがわかりやすいと評判でした。

標準ライブラリに何があるか把握するのが難しそう

演習を進めていく上で補題が必要になったとき、それが標準ライブラリにあるかどうかが分からない、という声がありました(このハンズオンでは標準ライブラリの解説は対象外にしていたのでそのあたりの話は特にテキストには書きませんでした)。これは実際もっともで、自分もいまだにどのように探せばいいのか分かりません。補題を探すときはファイルを標準ライブラリから直接目で見ることが多いし、モジュールの構成も完全には頭に入っていません。どうすればいいんでしょうか。

1週間空くと何をやっていたか忘れる

普通のプログラミングではないし、週に1時間しかやっていないため、どうしても前回やっていたことを忘れてしまうという声が多かったです(1時間の最初は前回やっていたことを思い出すところから始まる)。しょうがないところもあるとは思いますが、この問題に対しては対策を思いつきませんでした...。

おわりに

初めにも書いたとおり、当初は3回完結の想定(本気で3回でソートまでできると思っていた)だったし、やる内容からしても(そして最初の依頼に沿う形としても)ハンズオン形式が相応しいと考えて、ハンズオン用の資料を作成しました。ところが、蓋を空けてみるともう半年以上も続いています。ハンズオンという自分で進める形式の勉強会が長期に渡ると、参加者の間で進度に差が出てしまうという問題が発生します。途中から参加者が少ない場合は開催を中止するようにして、なるべく差が出ないよう配慮をしました。

ハンズオンをやることになったときに思ったことの1つとして、Agda が非常に入門難易度の高い言語であり苦労した経験から、自分が教えることでその障壁を少しでも和らげることができたらいいな、ということがありました。同じ証明支援系である Coq などと比較すると、決定版と言えるような教科書はなく(教科書は最近出版された1冊だけあり、入門にはよさそう)、日本語の情報もそこまで多くはありません。一体、世間の人はどのようにして Agda を学んでいるのでしょうか? 標準ライブラリを使いこなしている人間がどれだけいるのか、気になります。

(本稿はKLab Advent Calendar 2016 の9日目の記事になります)

こんにちは, @mecha_g3 です.

ISUCON6 の優勝賞金で新型の MacBookPro を購入しました. キーボードの打ち心地にどうも慣れられなかったり, USB-C の周辺機器がたくさん増えたりしていますが, 概ね満足しています.

格ゲーの攻略記事のようなタイトルですが, この1ヶ月ほど CODE VS for STUDENT というプログラミングコンテストに注力していたので, 今日はそれについて書きたいと思います.

CODE VS とは

CODE VS とは, お題となるゲームの, 最強のAIを開発するプログラミングコンテストです.

CODE VS for STUDENT 公式サイト https://student.codevs.jp

主催はチームラボさんとキャリフルさんで, KLabはスポンサーをさせて頂いてます.

決勝イベントが明日 12/10(土) に行われます. 決勝イベントでは, 予選で勝ち上がった学生 16 名 (Normalコース, Hardコース各8名) が対戦します.

また, 僕は学生を除いたランキングで 1 位だったので, エキシビジョンマッチに招待していただきました. 優勝した学生のAIと, 僕のAIが対戦します.

生放送もされるようなので, 是非観てください!

この記事の後半は, コンテストに参加していない方は興味がない内容になっているかもしれないので, 最初に宣伝しておきます.

ゲームのルール

今回のゲームは, CODEVS 2.0 のリメイク版で, 対戦形式の落ちものパズルです.

ルールの詳細は以下の PDF に記されています. https://student.codevs.jp/assets/files/rule.pdf

ゲームイメージ

ゲームのリプレイ動画を撮影しました. 動画を見ると, ルールのイメージを掴みやすいです.

ブロック

1~9 の数字が書かれた 1x1 のブロックです.

パック

3x3 の領域にブロックが 3~4 個入っています. ゲーム開始時に全300ターン分のパックが与えられます.

フィールド

幅10, 高さ16 のフィールドで, ここにパックを投下していきます.

消滅と連鎖

フィールド上で 縦, 横, 斜めのブロックの数字の和が 10 になった所が消えます. 消えたブロックの上にブロックが積まれていた場合, 上のブロックが落下します. ブロックが消えた事により上のブロックが落下し, 落下したブロックが消える. という動作を繰り返し, 連鎖が発生します.

得点

連鎖を行うと、以下の得点計算式に従って得点を得ることができます.

score = ∑ floor(1.3 ^ i) * floor(Ei / 2)
i: 連鎖数
Ei: 消滅カウント(合計が 10 になったブロックの数)

連鎖数に応じて指数的にスコアが上昇するので, 連鎖数が一番大事です. 連鎖の最後 (連鎖尾) の消滅カウントでスコアが数倍変わってくるので, 消滅カウントも無視できない存在です.

お邪魔ブロック

得られた得点に応じて, 相手にお邪魔ストックが加算されます. お邪魔ストックがある場合, パックの空いている領域にお邪魔ブロック (消すことができないブロック) が挿入されます.

自分にお邪魔ストックがある場合に得点を得た場合, お邪魔ストックが消費 (相殺) されます.

勝敗判定

パックがフィールドの外に溢れたり, 思考の制限時間を過ぎると敗北になります. 思考時間は 1 手最大 20 秒, 1 ゲームの持ち時間は 180 秒です.

基本的な考察

AIのプログラムは, 標準入力でゲームの情報を取得し, 各ターンにおいてパックを何回転させてどこに投下するかを標準出力に出力します.

全ターンのパックは事前に分かるので, 落下と連鎖のシミュレーションを行い, 大連鎖を作ることを目標に探索するプログラムを作る事になります.

長いターン使って大連鎖を作ろうとしていると, 相手が先に連鎖を発火し, 邪魔ブロックが降って来て大連鎖を発火できずに負けてしまいます.

逆に, 短いターンで連鎖を作っていると低いスコアになってしまい, 相手に邪魔ブロックが大して降らないため, 相手は連鎖を伸ばすことができてしまいます.

そこそこ短いターンで出来るだけ大きな連鎖を作る探索が, このゲームで一番大事なポイントです.

ここからは, 僕がこの探索部分をどう改良していったかについて掘り下げていきます.

アプローチ

落とし方は 1ターンあたり 48 通りあるので, 4 ターン先(48^4 = 5308416) まで調べるのに数秒かかりそうです.

実際には有効な落とし方はもう少し少ないですが, 全探索だと 5, 6 ターンが限界だと思います.

相手のフィールドを埋め尽くす程の邪魔ブロックを降らせるためには, 16 ~ 20 連鎖程度必要で, そこから考えると 20 ターン程度必要です.

このような探索の問題では, 評価関数を作り, 各深さ毎に評価値の高い上位 K個 を残すことを繰り返すビームサーチという手法がよく使われます. (K をビーム幅と呼びます)

もちろん厳密な解は得られませんが, 適切な評価関数が設定できれば, 短い時間でそこそこ良い解を得ることができます.

僕は最初ビームサーチで実装していましたが, 今回の問題では時間制限がシビアだったので, 時間調整のしやすいビームサーチの亜種である chokudaiサーチを採用しました.

ベンチマーク

探索の改良を試したり, 評価関数を調整した結果, それが良くなったか悪くなったかを比較できるようにする必要があります.

今回僕は, 公式クライアントから 300 ゲームの入力ファイルを抽出し, 各入力で 20 ターン先まで探索し, できた連鎖のスコアの平均値を見て調整しました.

1 回 15 秒かけて探索するので 1 時間半かかってしまいますが, Google Compute Engine で 16 コアのマシンを借りて並列で走らせる事で 5 分程で計測することができるようになりました.

GCE 上に Jenkins をインストールしたプリエンプティブインスタンスを用意し, ベンチマークをかけたい時だけ立ち上げて実行, 終わったら個人的に使っている slack に結果を通知し, インスタンスを停止する. という運用で使っていました. 今回 CODE VS のために使った金額は 400 円程度でした.

slackへの通知イメージ

評価関数

「連鎖数が大きくなるようにしたい」というのはどういう評価関数にしたら良いのか悩みどころですが, 評価関数の中で実際に連鎖を起こしてみて何連鎖したのかを見るのが簡単です.

各列に対して 1-9 のブロックを落とすシミュレーションをしてみると, 何連鎖する盤面なのかを正確に見積もることができます.

ただ, 1 状態を評価するのに 90 回もシミュレーションをするのはとても無駄が多く遅いので, ある程度サボらないといけません.

僕の場合は, フィールドを広く使って, 左端から右端(あるいは右端から左端) に向かって連鎖を伝搬させていくような積み上げ方を見つけて欲しかったので, 発火点を左端か右端に固定しました.

最初の評価関数は

200 * 左端の列に 4 を落としたときに発生するスコア + 連鎖前のブロック数

でした. すごく雑ですが, わりと強くて最初の 1 週間程度 1 位を維持していました.

ここから, ベンチマークの結果を見ながら評価関数を調整していきました.

最終的には

ランダム(0.0 ~ 1.0)
+ 100000 * 連鎖数
+ 1000 * 連鎖前のブロック数
+ 10 * 連鎖尾の消滅カウント
- 100 * 連鎖あたりの平均消滅ブロック数
- 1 * 連鎖後に残っているブロック数

としました.

お邪魔ブロックが混入してきた場合は発火に使うブロックを 1-9 で試すようにしましたが, 他は同じです.

各パラメータの重みは比較の優先度を決めているだけです.

ランダム

連鎖数が増えるまでの盤面は優劣をうまく付けれないので, 同じスコアが並びやすいです.

同じスコアが並んだ場合, 特定の順序 (探索キューに入れた順など) で偏りが出てしまうので, これを分散させる目的で入れています.

連鎖数

発火目標ターンのパックをフィールドの端に落とした際に発生する連鎖数です.

この方法で評価した場合, 発火点は固定なので, 連鎖尾を伸ばしていくような探索になります.

スコアをそのまま評価関数にしてしまうと, 連鎖数を伸ばすよりも同時消し数を増やしてしまうほうが良いと評価してしまうことになるので, 最終的に連鎖が伸びにくくなってしまいます.

連鎖前のブロック数

フィールド中に存在する, お邪魔ブロックを除いた 1-9 のブロックの数です.

連鎖を積み上げていく途中で, 無駄に消してしまうとそれだけでもったいないので, ブロック数が多い方が良い状態としました.

連鎖尾の消滅カウント

連鎖尾も一応評価したいのですが, それよりも連鎖数を伸ばして欲しいので評価値としてはかなり優先度を低くしてあります. 気持ちです.

連鎖あたりの平均消滅ブロック数

連鎖で消えたブロック数 / (連鎖数+1) で計算しています.

限られた数のブロックで大きな連鎖を作って欲しいので, 同時消しが多いのは無駄です. 連鎖あたりの平均消滅ブロック数が少ないほうが良い状態としました.

連鎖後に残っているブロック数

8 や 9 といった大きい数字のブロックは 1 や 2 が来ないと消えません. 一方 1 や 2 は他の数字のブロックとも消えます. 連鎖が終わった後で 8 や 9 が残りやすく, これが実質的にお邪魔ブロックになって次回連鎖のスコアが下がってしまう現象が見られたのでこれを入れました.

高速化

速い方がたくさんの盤面を探索できるので, 制限時間内に良い連鎖を見つけやすいです.

テストの作成

シミュレータのテストがあると安心してリファクタリングや高速化に着手できます.

今回のルールでは, CODEVS のクライアントのリバースエンジニアリングは禁止されていませんでした.

クライアントの jar をライブラリとしてインポートした Java プロジェクトを作る一般的なテクを用いて, ログファイルから入出力を抽出するプログラムを作りました.

オンライン対戦のログファイルを大量に用意し, そこから入出力を作ってテストケースとしました.

評価用の落とし方の固定

ある程度探索が進むと, 発火に使うパックの落とし方はほぼ決まってしまうので, 評価関数の中で色々な落とし方を試して評価するのは無駄が多いです. なので, 4 連鎖以上が発生した場合は, 次から評価関数内での連鎖数の評価に使うパックを固定するようにしました.

精度は落ちますが, かなり無駄が省けるのでスコアは上がりました.

同一盤面の除去

高速化とは少し違う話ですが, 一般的に探索の途中で同じ盤面を 2 回探索しないようにするのは多くの場合必須な処理です. これを同一盤面の除去と呼んでいます.

今回はゲームの性質上, 完全におなじフィールドは現れにくいので効果は薄いですが, 探索中のフィールドをビジュアライズしてみると, 少なからず現れていたので除去を行いました.

フィールドのハッシュ値を計算し, 探索済のハッシュ値を保持しておきます. 同じハッシュ値のフィールドが現れた場合, 処理をスキップします.

探索のキューに入れるタイミングではなく, キューから取り出すタイミングで判定することでほとんどコストをかけずに除去することができます.

同一盤面を除去することで, 多少ですが無駄な探索を減らす事ができました.

落下処理の高速化

予選の対戦サーバは Xeon E5-2670 v2 だったのですが, 決勝参加者向けに提供された環境は Xeon E5-2666 v3 でした. (おそらく c4.large)

調べた所 v3 では Haswell 世代の命令が使えます.

Haswell から使える命令に PEXT (Parallel bits extract) という命令があります. これは値 val と ビットマスク mask を入力し, val のビット列の中から mask 指定したビットを抽出し, それを下位ビットに寄せたビット列を作る命令です.

さて, ブロックの数字は 0~11 (お邪魔ブロックは11で表される) なので 4bit あれば表現でき, フィールドは幅10 高さ16なので, 64bit 整数 10 個で表現することができます.

このようにフィールドを表現すると, PEXT を消去が行われた列に対して使うだけで落下処理が実装できます.

// erased_y_mask := 消えたブロックの位置が 1111 となるようなビットマスク
// m_[x] := 1列を表す uint64_t 型の変数
m_[x] = _pext_u64(m_[x], ~erased_y_mask);

落下処理のために生まれたかのような命令ですね.

消去処理の高速化

消去処理では, フィールド中にある隣接したブロックの数字の和が 10 になる場所を探さなければなりません.

和が 10 になるかどうかの計算は, しゃくとり法というテクニックを使うことで, 各列に対して 1 度走査するだけで行うことができます.

あるブロックが落下した結果, そのブロックに隣接したブロックの数字の和が 10 になることで消去が発生するので, 落下が発生していない領域は調べる必要がありません.

落下が発生した行, 列と, それに対応する斜めの行を記録しておき, 消去が発生しえない範囲に対しては消去判定を行わないようにしました.

もう少し具体的に説明すると, あるブロックが落下し (x, y) で止まったとしたとき, 以下のビットマスクをつくります.

x_mask |= 1 << x
y_mask |= 1 << y
z_mask |= 1 << (x + y)
w_mask |= 1 << (9 - x + y)

x_mask, y_mask はそれぞれ縦消し, 横消しが発生する可能性のある列を表します. z_mask, w_mask はそれぞれ左上から右下, 左下から右上に向かっての斜め消しが発生する可能性のある列を表します.

ビットが立っている縦, 横, 斜めだけを調べ, さらに横と斜めは x_mask によって調べる範囲を絞ることができます.

これらの評価関数の調整や高速化により, 20 ターン発火での平均得点は 400 点程度から 730 点程度まで上がりました.

また, 20 ターン発火では火力不足で負けてしまう事があったので, 最終的には 22 ターン発火にしました. 22 ターンでは平均 1070 点程になりました.

今夜勝ちたい実装

エキシビジョンマッチ向けに実装した勝ちたいだけのちょっとズルい実装です.

ルール的に禁止していないことを確認した上で実装しています.

相手の思考時間を使う

ゲーム開始直後の 1 ターン目で 22 ターン先まで探索して落とし方をキューに入れておき, その後は邪魔ブロックが降ってこない限り, キュー入れた落とし方を再生するような実装になっています.

相手が 1 ターンあたり 1 秒つかって探索してくるタイプの場合, 20 秒程 CPU が暇することになります.

なので, キューの内容を再生中も裏で探索を継続しておき, よりよい連鎖が見つかったら途中で乗り換えるという実装をしました.

相手に合わせて発火ターン数を調整する

十分にダメージが与えられる量のお邪魔ブロックを送ることができるなら, 先に発火したほうが勝ちやすいルールになっているように思います. なので, 対戦時のログをファイルに記録しておき, 以下のルールに従って初回攻撃のターンを調整する機能を実装しました.

前回の対戦で勝利した場合

  • 前回の初回攻撃のターンを使用する

前回の対戦で敗北した場合

  • 相手の方が先に初回攻撃を行っていたら, 相手の初回攻撃ターンでこちらも初回攻撃を行う
  • 自分の方が先に初回攻撃を行っていたら, 初回攻撃ターンを +1

ボツネタ

考えたけど上手く行かなかった事, 実装できなかったことなどです.

発火点を成長させる

連鎖を組んでいく際に, 発火点を成長させるのと, 連鎖尾を成長させるのでどちらが強いのでしょうか.

当たり前のことですが, 上から落下させたブロックは, 下から上に積み上がっていきます.

発火点を固定し, 連鎖尾を成長させる場合, 発火点は必然的にフィールドの下の方になってしまいます. フィールドの下の方でブロックを消すと, 上に乗っているたくさんのブロックが落下し, 多くのブロックがズレることになります. たくさんのブロックズレるということは, たくさんのブロックが消える可能性があるわけですが, 連鎖数を稼ぎたいので, 同時消しではなく 2, 3 個ずつ消えて欲しいです. 一度ズレたけど消えなかったブロックは, 今後同様のズレの状態になったとしても消えません.

この消えないズレの組み合わせが徐々に連鎖の成長を制限するため, 連鎖尾を成長させる方針はある程度で頭打ちになります.

発火点を成長させていくと, 発火点が上になるためこの制限を受けづらくなり, フィールド全体を使って連鎖を作ることができます.

ズレの理論に関しては, CODE VS 2.0 の colun さんの説明がわかりやすいです.

また, 連鎖尾の同時消しはスコアにそこそこ大きな影響を与えます. 発火点を伸ばす場合, 連鎖尾の同時消しを作った後に発火点を伸ばすことができるので, 高いスコアを取りやすいと考えられます.

つまり, 発火点を成長させる方針は, 以下のようなメリットがあります.

  • フィールド全体を使って大連鎖を作ることができる
  • 連鎖尾の同時消しを作ることができる

一方で, 連鎖尾を伸ばす連鎖は, 以下のようなメリットがあります.

  • 少ないブロックで柔軟な連鎖を組みやすい
  • 発火点を固定することで評価が高速にできる
  • 邪魔ブロックが降ってきても発火点さえ潰れなければ連鎖は残る

CODE VS 2.0 予選では発火点を成長させる連鎖が強かったのですが, 今回の CODEVS for STUDENT では, スコアに対して相手に送る邪魔ブロックの数が多く, 素早く連鎖を作ることが大事だったため, 連鎖尾を伸ばす方針にしました.

マルチスレッド化

CPU を使い切るために, 探索をマルチスレッドで動かす実装を行いました.

できるだけロック時間が減るように探索の仕方を工夫し, 手元の PC では 2 スレッドにした際に約 2 倍探索できるようになりました.

しかし, 決勝の環境はハイパースレッディングの 2CPU だったので, 1 スレッドと比べて 1.2 倍程度にしかなりませんでした.

プログラムが複雑になってしまったのと, 探索順序が実行するたびに微妙に変わってしまい, 他のチューニングがやりにくくなってしまったので破棄しました.

ベクトル演算による高速化

連鎖のシミュレーションのうち, 一番ボトルネックになるのは, 加算や減算をたくさんして部分和が 10 になるところを探す消去判定です.

加算や減算をたくさんするので, ベクトル演算を使いまとめて演算を行うことで高速化できるはずだと考えて, 3 日ほど AVX2 の関数の使い方を覚えベクトル演算版のシミュレータを書きました.

消去判定のしゃくとり法において, 10 を超えた部分に関して戻って減算をする部分でどうしても演算回数を減らすことができず, 影響範囲のあるところだけ調べるナイーブなしゃくとり法に比べ, 1/3 程度の速度しか出せませんでした.

もっとベクトル演算に慣れて, ベクトル演算しやすいアルゴリズムを思いついたら速くなるかもしれませんが, 今回はあきらめました.

評価関数の自動調整

各評価パラメータの重みが, 比較優先度を決めているだけになってしまいました.

ブロックの位置関係など, もう少しパラメータを増やし, 重みを機械学習的な手法での自動調整に挑戦してみたかったです.

僕が今夜勝ちたいだけの実装をしている間に, 決勝に出場する piroz さんはこの自動調整に挑戦していたらしく, とても尊敬しています.

結果的にうまく調整できなかったようですが, コンテストを通しての成長という観点で僕は完全に負けています.

pirozさんの記事

ソースコード

エキシビジョン提出時のソースコードを公開します.

後に気づいたバグがそのままだったり, 人に読ませるつもりのない思考ログやコミットログが残っていますが, コンテスト参加時のリポジトリをそのまま公開します.

https://bitbucket.org/mecha_g3/codevsfs/src

まとめ

明日は CODEVS for STUDENT の決勝イベントが行われます. エキシビジョンマッチで僕の今夜勝ちたいAIが優勝者と対戦します.

生放送是非観てください!

2017年は機械学習勉強するぞ!!!!


@mecha_g3

(本稿はKLab Advent Calendar 2016 の4日目の記事になります)

Travis CIはよく知られたCIサービスの一つです。読者の方々の中にも、個人的なプロジェクトのCIに利用している人は多いのではないでしょうか。一方で、設定ファイル .travis.yml 中に秘密情報を暗号化して記述できることはあまり知られていないかもしれません。

YAML中での暗号化のやり方はTravis CIのドキュメント「Encryption keys」にも書いてあるのですが、 travis encrypt コマンドによりAPIトークンなどの秘密情報を暗号化して .travis.yml 中に記述するような仕組みになっています。この情報はTravis CI側で復号されてCIプロセス中で利用することができます。

今回指摘する内容は、この暗号の強度が多くのプロジェクトにおいて不足しているのではないかという点です。というのも、2015年4月以前に作られたTravis CIプロジェクトではRSA 1024bit鍵による暗号化が利用されているのです。

本稿ではTravis CIの暗号化の仕組みを簡単に説明した上で、どういうときに危険性があるかの詳細と鍵ペア再生成の方法を紹介します。

travisコマンドの概要

まずは travis コマンドを用いた暗号化について簡単に紹介します。 travis コマンドというのは gem install travis でインストールされるRuby製のコマンドで、内部的にTravis CIのAPIを叩いて色々とよしなにやってくれる便利コマンドです。

そのサブコマンドの一つが travis encrypt で、これを使えば任意の文字列を暗号化して .travis.yml 中に記述することができます。たとえば、Travis CI連携しているGitHubプロジェクト直下のディレクトリで下記コマンドを実行してみましょう。

$ travis encrypt 'FOO=secret_information'
Please add the following to your .travis.yml file:

  secure: "BEC97APcjoBsKRRGS4DCcQoLCviHTzK88JxfEq0wDfJ4+kfuLktyXEbHbG6Ct9cP+KLnwxIDBamf0pgOS7iQGLLb5Irn00fn4JEBeHd6kyTXQbyuPSe/NffVceg5vq8RWPT8nlWzVHD3wtjJFWz/Ocm6q5RkqvOtLszwM1Nc0Ig="

上記コマンドで出力された行を .travis.yml 中に書けば FOO=secret_information と書いたのと同じ意味になります。この仕組みにより、APIトークンやメールアドレスなどをYAML中に記述して外部サービスとの連携に使うことができます。

travisコマンドによる暗号化の中身

さて、この暗号化はどのような仕組みなのでしょうか? travis コマンドの中身を見ると、その正体がRSAを利用した公開鍵暗号であるとわかります。具体的には、travis encrypt コマンドが公開鍵で暗号化を行い、暗号文を受け取ったTravis CIが秘密鍵で復号するような仕組みになっています。

この暗号化に用いられるRSA鍵ペアの生成はTravis CI内部で暗黙に行われており、秘密鍵はTravis CIだけが持っています。つまり、公開鍵で暗号化した文字列は暗号化した本人でさえ復号できず、Travis CIだけが復号できるというわけです。

言い換えると、この暗号化を信用するためのポイントは2点だと言えます。

  1. Travis CIが秘密鍵や復号済みデータを流出させるようなことが無い
  2. 公開鍵への攻撃により秘密鍵を求められるようなことが無い

これさえ守られていれば、暗号化された情報は安全だと言えるでしょう。逆に上記のうちどちらかの問題が発生するようだと、秘密情報を .travis.yml に平文で書いたのと同じということになりかねません。本当に大丈夫なのでしょうか?

実は2012年に少数のプロジェクトで1の問題が発生したことがあるようですが、今後は安全だと仮定するしかないでしょう。今回は2の問題について議論していきます。

公開鍵への攻撃の可能性

今回指摘したいのは、RSA公開鍵への攻撃の可能性についてです。

まずはTravis CIの公開鍵にアクセスしてみましょう。リポジトリに紐付く公開鍵は下記のようにAPI経由で取得できます(参照:「Travis CI - API Reference - Repository Keys」)。URL中の hnw/php-build というのがユーザー名/リポジトリ名になっています。

$ curl -s https://api.travis-ci.org/repos/hnw/php-build/key | jq -r '.key'
-----BEGIN RSA PUBLIC KEY-----
MIGfMA0GCSqGSIb3DQEBAQUAA4GNADCBiQKBgQDOQb++oR7aBL6TfjSZbo/ssNrE
sV9FJmOn5TZktfAgLFv7T5c93Iot1k6ha7OO0FaZyf67bR+5Nou4Vd4SaiFpvb38
NMj4Pz9Smdwi3pWisqcgZaQOOpe9IB0nTAGhzZp8+2EPC1syRUi30FXOD03xnL0q
X8rhgIkuD6415tGP3QIDAQAB
-----END RSA PUBLIC KEY-----
$

ところで、この公開鍵は短そうに見えますよね。実はこれが1024bit鍵です。RSA 1024bit鍵の素因数分解は現代のスパコンでもかなり手強い計算ではありますが、コンピュータの性能向上により5年後なり10年後なりには現実的に攻撃可能になると考えられています。「暗号の2010年問題」の頃に2048bit以上の鍵への移行が叫ばれたことを考えても、1024bit鍵の寿命が近いのは間違いないと言えるでしょう。

ちなみに、鍵ペアが1024bitになっているのは一定以上古いプロジェクトだけです。最近のプロジェクトでは4096bit鍵が利用されていますので、今後プロジェクトを作る分にはこの問題はありません。正確な時期はわかりませんが、2015年4月頃に4096bit鍵に切り替わったように推測しています。

ご自分のプロジェクトの鍵ペアの鍵長を確認したい場合、上のようにAPIから公開鍵を確認すればわかります。公開鍵がASCIIで210文字くらいだったら1024bit鍵、730文字くらいだったら4096bit鍵ということになります。わざわざ鍵を確認しなくても、 travis encrypt の結果の長さも鍵長と同じサイズになるので、そこからも判断できます。

鍵の中身を正確に把握したい場合は openssl asn1parsedumpasn1 などを試してみてください。

鍵ペアを再生成する手順

もしかすると短い鍵ペアを使っているプロジェクトが見つかったかもしれませんね。もしそうだとしても、鍵ペアを再生成するAPIが提供されていますので安心してください。ちなみに、現時点ではAPIを直接叩く以外の方法は提供されていません。

鍵ペアの再生成APIを利用するにはAPIトークンが必要です。これは travis login コマンドでログインした後で travis token コマンドを実行することで取得できます。このAPIトークンを下記のように Authorization: ヘッダから送信すればAPIの認証が成功します。ただし、下記の hnw/php-timecop はユーザー名およびプロジェクト名です。

$ curl -d '' -H 'Authorization: token abcdefghijkl1234567890' -s https://api.travis-ci.org/repos/hnw/php-timecop/key

API呼び出しに成功すると新たな鍵ペアが生成されます。失敗した場合はおそらくトークンの指定が間違っています(ヘッダ中の token は消してはいけません)。元の鍵ペアが1024bitだった場合でも再生成すれば4096bit鍵になりますので、あと20年くらいは安心だといえそうです。

もちろん、鍵ペアを再生成した場合は改めて秘密情報の暗号化を行う必要があります。また、古い暗号文を遠い将来第三者が解読する可能性まで考えれば、暗号化対象のパスワード変更やAPIトークン再発行なども合わせて行うのが良いでしょう。

まとめ

  • Travis CIのtravis encryptによる暗号化にはRSAが使われている
  • そのRSA鍵の鍵長が1024bitのことがあるので要確認
  • 1024bitでは暗号強度の観点から中長期的に不安
  • 2015年4月頃までにTravis CI上に作られたプロジェクトが該当
  • API経由で鍵ペアの再生成ができる
  • 再生成すると4096bit鍵になる

本題とはズレますが、RSAを署名ではなく暗号化に使っている事例は比較的珍しい気がするので、その観点でも面白い話題といえるかもしれません。


@hnw

↑このページのトップヘ