17:55 13/08/12
ICFPコンテストでした
ICFP プログラミングコンテスト が終わりました。 今年は @nya3jp @phoenixstarhiro @dmikurube @kinaba の 4 人チームで参戦していました。 C++ で計算バックエンド、 Python でサーバーとのやりとりと計算モジュールをつないで答えを送りまくる最上位のロジックとフロントエンド、 という構成でした。
簡単なまとめ
今年の問題は、 『サーバーに1400個くらいプログラムが置いてあります。 プログラムは 64bit 整数を 1 個受け取って、 何か計算して 64bit 整数を 1 個返す関数です。 サーバーは、プログラムの番号と引数を指定すると実行して結果を返してくれます。 どういうプログラムが置いてあるのか、できるだけ沢山当ててみなさい！』 という問題。 当てた個数が多ければ多いほど好スコアです。
プログラム中に使われている演算子の種類や、プログラムのサイズがヒントとして与えられているので、 それを手がかりに当てて行くことになります。また、「これでしょ？」とサーバーに回答を送りつけると、 合っていたらスコアになるし、間違っていても、（サーバーの努力が及ぶ範囲で）反例、つまり、 サーバーにあるプログラムと送りつけたプログラムの結果が違うような入力整数を返してくれるので、 それをヒントにさらに推測を進められるのがポイントです。
感想としては、かなり面白かったです。 プログラムを書いたらあとは完全にプログラム任せ、になるゲームの AI とかの作成大会よりも、 その場で人間もモジュールとして込みの態勢で問題を解きに行く体勢になるようなコンテストの方が好き、 というのもありますが。難易度も72時間にピッタリの絶妙な調整だったと思います。
主催 Microsoft だったので答え合わせや反例生成は Z3 で実装しているのだと思うのですけど、 こういうゲーム仕立てでこういうテクノロジーを見せてくれるのも格好いいなあと思う。
（チームの人が）やったこと
ソースコードは github.com/NekoSamaDuce/icfpc2013 にあります。 solver/ と frontend/ に問題解きルーチンがあって、 書かれた時期や用途は、以下の絵のような流れになっています。 （括弧内は途中で破棄されたプロジェクト）。
・ 開始直後： 問題読み合わせ。用意されている問題のメタデータをざっと眺めてみる。
・ とりあえず、サイズ 3 のプログラムとかほとんど一つに決まるし、 サイズ小さいのはあり得るプログラムを 全列挙 (genall) して全部サーバーに送りつければどれかは当たるはず。 これが最大サイズまでスケールしないのはわかりきっているけど、 問題に慣れるためと、 どうせ何をやるにもプログラムを表現するデータ構造の定義とかは書くはめになるので、 無駄にはならないはず、と実装開始。
・ 完成。確実に問題無さそうなサイズ 3, 4 までおそるおそる送ってみる。正解。 「回答開始から 5 分以内に正解を出さないとその問題は 0 点に確定されてしまう」 というシステムだったので、少なくとも序盤はかなり安全側に倒して絶対の自信を持ててから行くようにしました。 結果、サイズ 5 以降は（ほぼ間違いなく解けていそうなケースでも）念のために翌日送りになりました。
・ さて、単純全列挙の次のステップをどうするか会議。 1. 全生成したプログラムを予め分類 (cluster) しておく。 具体的には256のランダムな入力を与えたときの出力256個をキーにして引けるようにしておく。 すると、サーバーに全部投げつけるのではなく、256入力の結果をサーバーに聞いてみて、 一致したクラスタの要素プログラムだけ送ればよくなる。 2. 生成したプログラムを正規化 (simplify) して、 すでに生成したものと同じだったら忘れるようにして、生成されるプログラム数自体を減らす。 たとえば (plus x 0) を x に置き換えちゃうとかそういうルールは無限に思いつくのでどんどん足していく。 3. 反例フィルタ。間違いの時にサーバが返してきた入出力ペアを使って手持ちの候補を実行 (eval) してみて、間違っている物はもう送らない、とすることで送る候補を減らす。
・ 全部実装。2 日目は、この 3 つを統合したフロントエンドで、 小さい方の問題から順にゆっくり解いていっていました。 「simplify の追加規則はどんどん思いつくのでそれを実装する。 とりあえず全探索系で潰せる範囲 (size=15 くらい？) まではこの流れで潰す」 「勢いでコード書きまくってしまって怖い状況なのでテスト整備しまくる」 「そんな作業を各自しながら、最大サイズ 30 向けの抜本的な別解法を考え始める」 というのが 2 日目の状況。 最終的には結局、 この全探索ラインで十分な速度で解けるのはサイズ12、tfoldなら15まで、 13、16も必要なら待てる程度の速度では動く、くらいになりました。
・ 3 日目前半の主要タスクは、 1. 昨晩追加されたサイズ小さい方(19～25)の"ボーナス"問題に特化したソルバー。 2. 全探索の及ばないサイズに突撃する用の新ルーチン。 少数の入力値に対する計算結果の値だけを見た式の同一視。
・ ボーナス問題は (if0 (and A 1) B C) の形を必ずしているようなので、
サイズ 8 までの A, B, C の候補を作成済みの全列挙ルーチンで全列挙
→ 同じく作成済みの、サーバにまず256個のランダム入力値を投げて結果をもらう処理
→ 正しい A, B, C は、「(and A 1) が 0 であるような入力で B がサーバの答えとすべて
合っていて、そうでないような入力で C がサーバの答えと合っている」ような組。
そういう組を探索して反例フィルタつきで片っ端から投げる。
さて、ここまでのソルバーは全て、 「256個の入出力を一回サーバから貰う」 「解の候補集合を作る」 「（反例フィルタで候補集合を削りながら）順に投げつける」 という構造をしていました。 つまり、まず答えを確実に含むような（巨大な）プログラム集合を列挙して、 あとはそれをひたすら削っていく、と。 これだと対象が巨大だとそのようなプログラム集合を構成することができなくて破綻するので、 方向をスイッチ。
・ 「3個の入出力をサーバから貰う」 「他の入力のことは全く知らないがその3個についてだけは正しいプログラムを作る」 「サーバーに送ってみる」 「合ってたら良し、間違ってたら反例を加えた4個で同じ事を繰り返す」
・ 「その3個についてだけは正しいプログラムを作る」 というのは、プログラムの全生成を下から動的計画法で組み上げて行くときに、 "その3個の入力については同じ値になる" ような式が既に作ってあれば、 本質的には違う式であっても捨てる、という形で全生成を実装しています。 これで意外と当たるし、意外とサイズの爆発を押さえられるという。
・ この全体の Counter-example guided refinement っぽいループを回すドライバと、 メインの式の値だけをキーにしたDPの計算モジュールが終了13時間前くらいに一応の完成、投入。 fold の部分式はメインの入力 x だけでなく変数 y, z も含んでいて"値"に潰せなくて困るので、 このソルバーは fold なし のケースだけを対象にしています。
・ 割とよく動いているのだけど、trainデータでの挙動を見ていると、 浅い位置に複雑な if 分岐があるプログラムを合成するのが苦手っぽい動きをしている。 → 「時間がかかっている場合は、プログラムのルートを必ず if にして、 合成が難しくなった入力値を then と else の別ブランチに分けるような条件部をまず自動生成」 というヒューリスティックスを投入。強制ifモード。
・ これでかなり解けるようになったので、バックグラウンドで回しておいて、さて、残りは fold 入りのケース。
・ fold のbodyや途中式などというものを考えるから難しいのであって、 "fold λyz.(or y z)" や "fold λyz.(or z (shr1 y))" のような挙動をする組み込み演算子が無限にある言語なのだ、 と思えば問題は消える！ という方針で頑張ることに。 重み5のfold-orや重み6のfold-or-shr1という演算子がある、という扱いにして上記のアルゴリズムを走らせる。
・ fold の中として面白い式に特化した式全列挙ルーチン、 それを使ってfoldに対応した新バージョンの合成型ソルバを実装。 fold 全列挙を毎回起動されるたびにやるのは時間の無駄なので、 常駐して標準入出力をパイプしてドライバとやりとりするように変更。 終了5時間前、実戦投入。この時点で600個くらい手つかずのfold問題が残っています。 そもそもfoldなしの方も100問くらい残っている…。
・ 残り時間とサーバのrate limitを見ながら、ソルバを 3 ～ 4 並列起動する体勢に以降。 解けるケースは大抵すぐに解けるので、解けない場合は5分と言わず1分で打ち切り、などなどを導入。
・ けっこうな数 fail してしまったけど終了20分前に通常問題は完走。
強制ifモードの代わりに強制ボーナスifモード （(if0 (and 1 X) ...)で分岐する）
を足した non-fold ルーチンを時間いっぱい走らせて、終了！
