ref: http://icfpc2013.cloudapp.net/
最近やる気がなくてちゃんと参加できてなかった ICFPc ですが、今年は久々にフル参加しました。
チームメイトは例によって @hirekoke さんですが、途中で飽きられてしまったので事実上のぼっちでした。
問題
こんな感じ。
- サーバに「隠された関数」がある。
- サーバに整数を送ると、返り値を教えてくれる。
- この情報を頼りに、隠された関数の実装を推測する。
- 1 つ当てるごとに 1 点。たくさん当てた者の勝ち。
まあ、地味ですね。古代の石版とか宇宙人救済みたいなこじ付け設定はなし。もう少し言うと、
自分の解答
大まかに、全列挙ソルバ、ちょっと賢い列挙ソルバ、bonus 用ソルバ、敗戦処理ソルバの 4 つを作りました。
全列挙ソルバ
ブルートフォースです。
- テストベンチ (引数とそれに対する返り値の組) をサーバから取得する。
- 指定されたサイズで、指定されたプリミティブをすべて使う関数を列挙する。
- 列挙したものの中からテストベンチを満たす関数を探す。
- 見つかったらサーバに投げてみる。当たれば終わり。外れたらテストベンチを拡充して 3 へ。
ライトニングはこれで戦ってました。でもサイズ 11 くらいで限界。
なお、初期テストベンチは、ビットが 1 つだけ立ってるような人為的な整数 128 個と、乱数 128 個にしました。後で乱数の数は 16 個くらいに減らしたけど、基本的には最後までこのまま。
ちょっと賢い列挙ソルバ
2 日目に作ったもの。
単純な全列挙だと冗長な関数がたくさん列挙されます。具体的には以下のような部分式を持つもの。
- (and x (and y z)) と (and y (and z x)) とかは 1 つあれば十分。
- (and 0 x) は明らかに不要。
こういうのの列挙を抑制するようにしたものです。具体的には以下の 3 つ。
- and や or を内部的に n 引数として扱い、部分式をソートしたもののみ列挙する。(式には適当な全順序を定義しておく)
- 簡単な記号実行をおこない、確定的に 0 や 1 になるものや、常に片方に分岐する if などを弾く。
- 上の記号実行で弾けない冗長パターンは個別に弾く。
記号実行は、式ごとに、その値の各ビットが確定しているか、確定しているならどんな値か、を判定するもの。0 という式は全ビット 0 で確定、x は全ビット未確定、(shr1 x) は MSB のみ 0 で確定、その他は未確定、みたいな感じで。具体的には式 1 つあたり 64 bit 整数 2 つの組で表してます (ビットの確定情報のマスクと、確定しているビットの値) 。頭の中では valgrind の未初期化変数の検知でした。
これだけだと (if0 x 1 x) が非ゼロと判定できないとか弱点はあるのですが、その辺は精度と実行効率と実装効率のトレードオフということで妥協しました。
(not (not x)) とか、(shr1 (not 1)) は (shr1 (not 0)) と同じだよねーとかは、この記号実行で弾けないので、手動で条件を追加していきました。3 日目前半はこの条件探しばかりやってましたが、効果があったのかはよくわかりません。
ちなみに、確定値を返すことが分かった式で、同じ値を返すより小さな式があるものは列挙しない、というのも実装してみたんですが、なぜかあまり枝刈り効果がなく、列挙の時間が 1.5 倍くらい遅くなったのでやめました。今から思えば、これはもっと調べてみればよかったかも？ 他のチームはこの辺真面目にやってる感じ？
あと、列挙をちゃんとメモ化するようにしたのでまあまあ速くなった。それでも、サイズ 15 が解けるかどうかという程度。
bonus 用ソルバ
bonus は全体構造が (if0 (add (...) 1) (...) (...)) という形 (ただし (...) はサイズ 5 以上の式？) だと分かっている問題です。
- ちょっと賢い列挙ソルバの要領で (...) に入る関数候補を列挙しておく。
- テストベンチを取得。
- テストベンチ (引数 i と返り値 o の組) すべてに対して、f(i) = o または g(i) = o となるような関数の組 f と g を、関数候補の中から探す。
- 見つかったら、それを then 節と else 節にあてはめてみて、さらに条件部分に合う式を探す。
- すべてそろったらトライ。ダメならテストベンチを拡充してやり直し。
探索範囲は結構広いのですが、解がいっぱいあるのか、大抵はすぐ解が見つかるので、第一弾の bonus はすべてゲットできました (バグと操作ミスで 2 問落としたのは除外) 。でも第二弾の bonus は規模がでかすぎて全然だめだった。
敗戦処理ソルバ
決定的に解けない問題を適当に解こうとしてみるソルバ。
といってもやってることは単純で、「ちょっと賢い列挙ソルバ」の列挙処理を一定回数で打ち切り、列挙しきれたものの中から解を探すだけ。見つからなかったらその問題は捨てる。
打ち切り回数は当然大きいほどよく当たりますが、その分遅くなるので、残り時間を見て調整しつつ走らせてました。
3 日目の夕方時点で決定的に解けない問題が 1200 問程度あることに絶望しつつ、「10 問に 1 問くらい当たればいいや」くらいの気持ちで作りましたが、それよりは結構当たりました。
この大会の本質は「如何に正解を見つけるか」ではなく「如何に高確率で正解を作るか」なんですよね。わかってはいたものの、有限個しかトライできないとなると慎重なアプローチを選んでしまう貧乏性。
ソース
実際には試行錯誤しながらいじったので全列挙ソルバは残ってないですが、他のソルバは 1 ファイルに詰め込んでます。
ref: https://gist.github.com/mame/08b38f75b7c7d88a8a7c
「3 日間だけわかればいい」という大変投げやりな姿勢で書いたので、読めたものではありません。所望のモードで動かすのにプログラム終端のコードをコメントアウトしたり適当に値を設定したりしないといけなくて、すでに自分でも動かし方を覚えてません。テスト環境とかバージョン管理とか実行方法の整理とか適当なのは当然自分の首を締めるんですが、環境整備をする余力がなかった。
記録
以下、3 日間でやったことを時系列順で。読み飛ばしてください。
1 日め
13:00 参戦。大会は朝 9 時からですが、会社を午後半休にしたので。
昼ご飯を食べつつ問題文をざっと読む。通信部を適当に作って、問題リストを取得した。
問題の感覚をつかむべく、全列挙のソルバを書く。トレーニングで問題なさそうだったので、17:00 ごろからサイズ 8 くらいまでの回収を始める。
わりと安定して回収できるようになったのを見て、走らせつつ tfold に対応。これはすぐにできてサイズ 11 くらいまでを回収。
この辺で Unable to decide equality (サーバのソルバのタイムアウト) に出会い、ちょっとやる気減退する。ここからしばらく迷走。
- 主催者に抗議のメールを送る (笑)
- 今頑張るところじゃないと知りつつ、送信を別スレッドにしたり、定数オーダの最適化をしたり。
- みるからに GC のせいで遅そうだったので、世代別 GC の入った開発版の Ruby を試して倍速になって喜んだり。
- z3 を調べてみたり、boolector にエンコードしようとして失敗したり。
- 全列挙の方法を変えてみたり (関数の木構造を先に列挙し、後からノードにプリミティブをはめていく) 。効果はまったくなかった。
初期テストベンチをフェッチしてから列挙するのだとタイムアウトが怖いので、フェッチ前に列挙と分類を行っておき、フェッチしたら該当分類だけを引っ張ってくるようにした。前処理はうまくすれば問題間で使いまわせるけど、列挙部分は見直す予感がしたのでやらなかった。
これで安心してぶん回しつつ寝る。
2 日め
起きたらメモリ不足で落ちていた。
fold に対応し、サイズ 13 くらいまでの回収を始める。この辺でライトニング終了。
また迷走。式を PostgreSQL 上でエンコードしてみるなど。(検索してくるのが早くなるかと思ったけど、登録が遅すぎてどうしようもなかった)
サイズ 14 のやつ 1 問に 6 時間かかるとか、手詰まり感。
bonus が公開されたので bonus 用ソルバを作り始めるけど、現在の全列挙の遅さではどうしようもないので、先にこちらに取り組むべきと判断。
ここらで頑張って、ちょっと賢い列挙ソルバを作った。この方法を初日に思いついてればなあ。(いつものこと)
なお、この時点で simple 版、tfold 版、fold 版が完全に独立したファイルになっていた (共通部分はコピペ) 。動いたコードを拡張するとエンバグしそうで怖かったので。でも管理がきつくなったので共通化。
これが終わって、走らせながら寝ようとしたところでバグで 1 問落とし、デバッグしてたら夜が明けた。
3 日め
昼前に起きる。速くなった列挙を元に、bonus 用のソルバを作って走らせる。
あとは、列挙のルーチンに不要な式の列挙を抑制する細かい最適化を加えていた。けど決定的に解けるのは 15 から 16 になった程度で、どの程度効果があったのかは不明。他の方式のソルバを考えた方がよかったなあ。
夕方ごろにギブアップし、low hanging fruit (大きいサイズだけれど、実はずっと小さい等価な関数が存在する問題) を狙った敗戦処理ソルバを作る。本当は日が変わるまで頑張るつもりだったけれど疲れたので。しかし後から考えると、解いてない問題が 1000 問程度残ってたので、夜から解き始めていたのでは間に合わなかった。危ないところだった。
結局夜になっても実行が終わらず、打ち切り回数を適当に小さくして平均時間を見積もり、2 台 2 並列 (計 4 並列) で走らせながら寝た。(それ以上走らせるとメモリ不足になるので)
朝起きたら一部のプロセスだけ終了していたので、適当に手動でタスクを再分配し、なんとか終了 1 時間前に全問消化。おわり。
感想
大変面白かったです。個人的にはここ数年で最高の出来。
「隠された関数を当てろ」というネタ自体は、誰でも考えたことのあるものだと思いますが、それを ICFPc クオリティに仕上げたのはさすが MSR 。
「こんなのできるかー」と頭を抱えるのが、翌日には当たり前にできるようになってて、別の問題に頭を抱えている、というのを繰り返すカタルシスの連鎖。を演出する絶妙な難易度設定でした。
多くを語らない地味な運営もわりと好みです。事前に「プログラム合成がテーマ」という予告があるとか、easychair を大会参加者管理に使うとか、問題文が味気ないとか、とっつき悪そうな雰囲気全開でしたが、今ではむしろクールに感じる。ランキングがないのも個人的には歓迎 (見るとやる気減退するので) 。逆に、終盤にスコアの情報が公開されたのは少し残念。あと touchdevelop.com の Flat UI は微妙すぎ。
問題で唯一どうかなーと思うのは、1820 個の独立した問題なので、計算パワーが有効過ぎることですかね。そりゃ速い計算機を持ってる人が有利なのは当然なのですが、amazon EC2 をずんどこずんどこ投入するのは、何かちがうような気が……。まあ、時代なのかな。とりあえずぼくは自分と @hirekoke さんのラップトップ 2 台だけで戦ったことを誇りに思うことにします。*4
それはおいといて自分の戦略を振り返ると、やはり決定的な解法にこだわりすぎですね。せめて 3 日目を正解率の改良にあてていれば……。とはいえ問題の本質を見誤るのはいつものことだし、決定的な解法でためた最適化は敗戦処理ソルバでも少しは活かされたと思うんでよしとします。むしろ最近の大会では健闘した方じゃないかと。
そんなことより IOCCC 2013 が開催中なことに今頃気がついた。10 月頭までだそうな。何か考えないと。
