競技プログラミングの問題を自動で解きたい

TL;DR

問い「競技プログラミングの問題は自動で解けるか？」
- 答え「ある程度は自動で解けるだろう。ただし問題の形式化を人間に任せる必要はある」
問い’「競技プログラミングの問題を自動で解くソルバは、具体的にはどのような形になるか？」
- 答え’「少なくとも初期のソルバは、最適化付きのトランスパイラと呼ばれるものになるだろう」

このような議論に従い、競技プログラミングの問題の実用的なソルバとして、Python から C++ への最適化付きトランスパイラを開発している。

TL;DR
目次
競技プログラミングの問題を解くとはどういうことか
競技プログラミングのソルバは形式化を人間に任せることになるだろう
競技プログラミングの問題を自動で解くことは不可能ではない
- 具体例 1
- 具体例 2
競技プログラミングのソルバは (初めは) トランスパイラの形がよいだろう
競技プログラミングのソルバは (近い将来においては) 定理自動証明機に近づいていくかもしれない
競技プログラミングのすべての問題が自動で解けるわけではない
競技プログラミングの自動化は競技プログラミングをより面白くするはずである
実現可能性を示すための実装例はすでに作った
実用レベルのものを目指して、いま頑張って実装をしているところである
競技プログラミングのソルバは遠い将来においては何になるだろうか？
競争相手を募集している
先行研究
言語実装 Advent Calendar 2020
注釈

競技プログラミングの問題を解くとはどういうことか

「競技プログラミングの問題を解く」と言っても、その範囲は意外に広い。まずこれを整理するところから初めよう。競プロの問題のページが開かれた直後の状態 (たとえば次のこのリンクをクリックした直後のような状態) から初めて、緑色の「AC」という表示を確認するまでの過程において、具体的にはどのようなステップがあるだろうか？もちろんこの過程には様々なものが含まれており (例: 「問題文中に埋め込まれている図を解釈する」「問題ページをスクロールする」「青い “提出” と書かれたボタンをクリックする」など) いくらでも細かく説明できてしまう。しかし、重要でないものを無視して抽象的な形で整理すると、通常の過程は次の 3 ステップにモデル化できるだろう¹²。

読解: 自然言語で与えられた問題を解釈し、数学的な問題として整理する
考察: 数学的な問題に対し、数学的な解法を考案する
実装: 数学的な解法を、計算機上の具体的な実装として記述する

(1.) は (人間にとっては) 自明なのであまりかえりみられることのないステップである。このステップでは、日本語や英語で書かれた問題を読み、数式などで表現された問題として整理し理解する³⁴。たとえば「熊の Limak が人間の高橋くんに合いに AtCoder 王国を訪れている。AtCoder 王国は $1$ から $N$ までの番号の付いた島と、それらの間にかかる $M$ 本の橋からなる。今 Limak は $s$ 番目の島にいて、高橋くんは $t$ 番目の島にいる。そして……」のような問題文を読んで理解し、不要な情報を捨象して「$N$ 頂点無向グラフ $G = (V, E)$ と $s, t \in V$ が与えられる。……」のような問題であることを確認する。

(2.) は競技プログラミングにおいて最も難しくかつ面白いとされる⁵ステップである。このステップでは、(1.) で理解した問題に対し、実行時間などの制限を満たす解法を考案する。たとえば、考察の結論として「まず重み付きグラフ $G = (V, E, w)$ とすべての頂点 $x \in V$ に対し $s \to x$ 最短路を $s$ からの Dijkstra 法で求め、次に重み付きグラフ $G’ = (V, E, w’)$ とすべての頂点 $x \in V$ に対し $t \to x$ 最短路を $t$ からの Dijkstra 法で求め、そして……」などのアルゴリズムが得られる。

(3.) はジャッジサーバによる自動採点のために必要なステップである。このステップでは、(2.) で得たがまだ頭の中にある抽象的なアルゴリズムを、計算機上の具体的なコードへ翻訳する。たとえば「$s \to t$ 最短路を Dijkstra 法で求めればよい」というときには、C++ なら priority_queue<pair<int64_t, int> > que; que.emplace(0, s); while (not que.empty()) ... から始まるようなコードが書かれるだろう。

そして、今回の話題は (2.) の「考察」のステップである。このステップは競技プログラミングという行為において中心となるステップであり、「問題を解く」と言うときも主にこのステップに注目している。つまり「競技プログラミングの問題を自動で解きたい」とは「考察を自動で行いたい」ということである。

競技プログラミングのソルバは形式化を人間に任せることになるだろう

競技プログラミングの問題を解くことを「読解」「考察」「実装」という 3 ステップに分けた上で主に「考察」を行いたいのだと言っても、残りのふたつのステップは容易に切り離せるものではない。問題は何らかの形で入力されねばならないし、解法は何らかの形で出力されねばならない。「読解」「実装」という残りのステップについても扱える必要がある。

機械にとって最も難しいのは「読解」である。自然言語の理解という非常に高度な処理が必要になる。競技プログラミングの問題文を以降のステップに支障がでないように読み取るには、表面的に単語を追うだけではおそらく足りず、文章全体の意味を正しく把握する必要があるだろう。競技プログラミングの問題文以外は理解できなくてよいのだとしても、これはかなり困難である。そしてこの「読解」は今回やりたいことではない。諦めてしまうべきである。

「実装」もそのままの形では機械では扱えない。「数学的な解法を、計算機上の具体的な実装として記述する」と言うときの「数学的な解法」などは、(通常の人間による競技プログラミングにおいては) 人間の頭の中のみ存在するものだからである。人間の頭の中にしかないものは機械には扱えない。「数学的な解法」でなくて「数学的な問題」の場合も同様である。

一方で、機械で扱える形に形式化したものが入力であれば「実装」も機械に可能である。このことはコンパイラを思い出せば分かる。F# や Haskell のような高級言語のソースコードを仮想機械の中間言語や実際の機械語に変換する操作はまさに「実装」であろう。

よって、ソルバを用いて競技プログラミングの問題を解くとすると、その過程は以下のような 4 ステップに整理されるだろう。この形であれば可能性はある。

読解: (人間が) 自然言語で与えられた問題を解釈し、数学的な問題として整理する
翻訳: (人間が) 数学的な問題を、機械上に形式化された問題として入力する
考察’: (ソルバが) 記述された形式化された問題に対し、機械的に解法を計算する
実装’: (ソルバが) 計算された解法を、具体的な実装として出力する

(1.) と (2.) は合わせて「形式化」をしている。これらのステップはどちらも人間にとっては簡単である。「読解」のステップが簡単であるのは認めてよいだろう。「翻訳」のステップも人間にとっては簡単だとしてよい。ただ読んだままを書けばよいためである。まったく理解できない難しい数式であってもそれを LaTeX で打ち込むだけならそれほど難しくないことがたいていだろうが、これと同じようなものである。

競技プログラミングのソルバが (1.) と (2.) のステップによる「形式化」を人間に任せてしまったとして、そのような条件で残りのステップだけを処理した場合も「競技プログラミングの問題を自動で解けた」と言ってよいだろうか？これは「自動で解けた」と言ってしまってよいだろう。なぜなら、「形式化」は (機械にとっては難しいとはいえ) 人間にとっては簡単であるし、通常は重要視されるステップではないからである。困難でも重要でもないステップを省略しても、困難で重要な (3.) の「考察’」のステップをうまく扱うのなら「問題を自動で解く」と言ってよいだろう。様々なことを自動でしてくれるソフトウェアであってもデータの打ち込みは人間の担当であることは多く、今回もそうだったというだけである。

競技プログラミングの問題を自動で解くことは不可能ではない

形式化を人間に任せてしまえば、競技プログラミングの問題を自動で解くことは不可能ではない。なぜなら、我々は (少なくとも私は) 通常の競技プログラミングの問題を (人間の手で) 解く過程において、すでに「機械的に行えるような考察」を多数しているためである。そのようなものを人間の手で行なうのでなく機械に行わせれば、これは競技プログラミングの問題を自動で解くことにほかならない。

具体例を見ていくのが早いだろう。

具体例 1

例として、問題 AtCoder Beginner Contest 100: D - Patisserie ABC を考えてみよう。整理すると次のような問題である。

長さ $N$ の整数列 $x = (x_0, x_1, \dots, x _ {N - 1})$ と $y = (y_0, y_1, \dots, y _ {N - 1})$ と $z = (z_0, z_1, \dots, z _ {N - 1})$ および自然数 $M \le N$ が与えられる。集合 $X \subseteq N = \lbrace 0, 1, \dots, N - 1 \rbrace$ に対し
\[f(X) = \left\vert\sum _ {i \in X} x_i\right\vert + \left\vert\sum _ {i \in X} y_i\right\vert + \left\vert\sum _ {i \in X} z_i\right\vert\]
と定義する。このとき
\[\max \Bigl\lbrace f(X) \Bigm\vert X \subseteq N \land \lvert X \rvert = M \Bigr\rbrace\]
を求めよ。

この問題は機械的に解ける。求めたい値 $y = \max \Bigl\lbrace f(X) \Bigm\vert \ldots \Bigr\rbrace$ はある整数 $a, b$ に対し $\max \Bigl\lbrace \vert a\vert + b \Bigm\vert \ldots \Bigr\rbrace$ の形の式で書かれている。 $\vert a\vert = \max \lbrace a, -a \rbrace$ という等式を使えば、この形の式は

\[\begin{array}{rcl} y & = & \max \Bigl\lbrace \vert a\vert + b \Bigm\vert \ldots \Bigr\rbrace \cr & = & \max \Bigl\lbrace \max \lbrace a, -a \rbrace + b \Bigm\vert \ldots \Bigr\rbrace \cr & = & \max \Bigl\lbrace \max \bigl\lbrace a + b \Bigm\vert \ldots \bigr\rbrace, \max \bigl\lbrace a + b \Bigm\vert \ldots \bigr\rbrace \Bigr\rbrace \end{array}\]

と変形できる。

この変形を可能な限り繰り返すと、求める式は

\[y = \max \left\lbrace\begin{matrix} \max \bigl\lbrace + \sum _ {i \in X} x_i + \sum _ {i \in X} y_i + \sum _ {i \in X} z_i \bigm\vert \ldots X \ldots \bigr\rbrace, \\ \max \bigl\lbrace + \sum _ {i \in X} x_i + \sum _ {i \in X} y_i - \sum _ {i \in X} z_i \bigm\vert \ldots X \ldots \bigr\rbrace, \\ \max \bigl\lbrace + \sum _ {i \in X} x_i - \sum _ {i \in X} y_i + \sum _ {i \in X} z_i \bigm\vert \ldots X \ldots \bigr\rbrace, \\ \max \bigl\lbrace + \sum _ {i \in X} x_i - \sum _ {i \in X} y_i - \sum _ {i \in X} z_i \bigm\vert \ldots X \ldots \bigr\rbrace, \\ \max \bigl\lbrace - \sum _ {i \in X} x_i + \sum _ {i \in X} y_i + \sum _ {i \in X} z_i \bigm\vert \ldots X \ldots \bigr\rbrace, \\ \max \bigl\lbrace - \sum _ {i \in X} x_i + \sum _ {i \in X} y_i - \sum _ {i \in X} z_i \bigm\vert \ldots X \ldots \bigr\rbrace, \\ \max \bigl\lbrace - \sum _ {i \in X} x_i - \sum _ {i \in X} y_i + \sum _ {i \in X} z_i \bigm\vert \ldots X \ldots \bigr\rbrace, \\ \max \bigl\lbrace - \sum _ {i \in X} x_i - \sum _ {i \in X} y_i - \sum _ {i \in X} z_i \bigm\vert \ldots X \ldots \bigr\rbrace \\ \end{matrix}\right\rbrace\]

となる。符号の正負を適当に処理すれば、あとは

\[\max \Bigl\lbrace \sum _ {i \in X} x_i + \sum _ {i \in X} y_i + \sum _ {i \in X} z_i \Bigm\vert \ldots X \ldots \Bigr\rbrace\]

を計算できればよいこととなる。次は数列 $a, b$ に対して $\sum _ {i \in X} a_i + \sum _ {i \in X} b_i = \sum _ {i \in X} (a_i + b_i)$ であることを使う。数列 $w_i$ を $w_i = x_i + y_i + z_i$ とおけば

\[\max \Bigl\lbrace \sum _ {i \in X} w_i \Bigm\vert \ldots X \ldots \Bigr\rbrace\]

を計算すればよいことになる。つまり $N$ 個の整数から $M \le N$ 個選んだときの総和の最大値を求めればよく、これはソートして上から $M$ 個を足すだけである。よってこの問題は $O(N \log N)$ で解ける。

ここまでの変形は主にいくつかの等式を用いた置き換えであった。つまり、以下のような (主に⁶) 5 つの規則を目標の式に機械的に適用していけば、今回の問題は機械的に解ける。

$\vert a\vert$ を見つければ $\max \lbrace a, -a \rbrace$ で置き換える
$\max \Bigl\lbrace \max \lbrace a, a’ \rbrace + b \Bigm\vert \ldots \Bigr\rbrace$ を見つければ $\max \Bigl\lbrace \max \bigl\lbrace a + b \Bigm\vert \ldots \bigr\rbrace, \max \bigl\lbrace a’ + b \Bigm\vert \ldots \bigr\rbrace \Bigr\rbrace$ で置き換える
$- \sum _ {i \in X} a_i$ を見つければ $\sum _ {i \in X} (- a_i)$ で置き換える
$\sum _ {i \in X} a_i + \sum _ {i \in X} b_i$ を見つければ $\sum _ {i \in X} (a_i + b_i)$ で置き換える
$\max \Bigl\lbrace \sum _ {i \in X} w_i \Bigm\vert \ldots X \ldots \Bigr\rbrace$ の計算方法を埋め込んでおく

規則を用いた置き換えは自動でできる。規則を事前に十分なだけ用意しておく必要もあるが、これは可能である。今回の例のように実際に使われる規則は $\vert a\vert = \max \lbrace a, -a \rbrace$ や $- \sum _ {i \in X} a_i = \sum _ {i \in X} (- a_i)$ のような一般性のある等式であり、個数はそう多くない。よってこの例は、競技プログラミングの問題を自動で解けることの例になっている。

具体例 2

別の種類の例として、直接コードを弄るものも見てみよう。以下のコードを考えてみよう (ところで、REP (i, n) と REP3 (i, l, r) はそれぞれ Python の for i in range(n): と for i in range(l, r): のようなものである。展開するとむしろ読みにくいと思われるのでそのままにしてある)。これが具体的にどのような問題⁷に対する解法コードなのかを知る必要はない。このコードの意図や正確な意味について理解していなくても、この関数 solve の時間計算量が $O(n^3)$ であることは明らかに分かるだろう。

#define REP(i, n) for (int i = 0; (i) < (int)(n); ++ (i))
#define REP3(i, m, n) for (int i = (m); (i) < (int)(n); ++ (i))

double solve(int n, const vector<int64_t>& a) {
    vector<vector<double> > dp(n, vector<double>(n + 1));
    REP3 (len, 2, n + 1) {
        REP (l, n - len + 1) {
            int r = len + l;
            REP3 (m, l, r - 1) {
                dp[l][r] += dp[l][m + 1] + dp[m + 1][r];
            }
            dp[l][r] /= r - l - 1;
            REP3 (i, l, r) {
                dp[l][r] += a[i];
            }
        }
    }
    return dp[0][n];
}

そして、すこし競技プログラミングに慣れている人であれば、この関数 solve の時間計算量が $O(n^2)$ に落とせることも同時に分かるだろう。REP3 (i, l, r) { dp[l][r] += a[i]; } という形で a[l] + a[l + 1] + ... + a[r - 1] を計算している部分は、累積和 sum を用意しておいて sum[r] - sum[l] とすればよい。(dp[l][l + 1] + dp[l][l + 2] + ... + dp[l][r]) + (dp[l + 1][r] + dp[l + 2][r] + ... + dp[r][r]) を計算している部分は、ふたつの累積和 dp_sum_l dp_sum_r を動的に更新しながら用いればよい。よって以下のようになる。

#define REP(i, n) for (int i = 0; (i) < (int)(n); ++ (i))
#define REP3(i, m, n) for (int i = (m); (i) < (int)(n); ++ (i))

double solve(int n, const vector<int64_t>& a) {
    vector<int64_t> sum(n + 1);
    partial_sum(a.begin(), a.end(), sum.begin() + 1);

    vector<vector<double> > dp(n, vector<double>(n + 1));
    vector<vector<double> > dp_sum_r(n, vector<double>(n + 2));
    vector<vector<double> > dp_sum_l(n + 1, vector<double>(n + 1));
    REP3 (len, 2, n + 1) {
        REP (l, n - len + 1) {
            int r = len + l;
            dp[l][r] += dp_sum_r[l][r] - dp_sum_r[l][l + 1];
            dp[l][r] += dp_sum_l[l + 1][r] - dp_sum_l[r][r];
            dp[l][r] /= r - l - 1;
            dp[l][r] += sum[r] - sum[l];
            dp_sum_r[l][r + 1] = dp_sum_r[l][r] + dp[l][r];
            dp_sum_l[l][r] = dp_sum_l[l + 1][r] + dp[l][r];
        }
    }
    return dp[0][n];
}

変換前のコードはほとんど愚直解のようなものであり、ソルバへの入力だと思ってよい。このようなコードの変形は (多少複雑ではあるかもしれないが) 自動で可能である⁸。この問題の想定解は $O(N^2)$ であり、変換後のコードは AC が得られた⁹。つまり、この例は競技プログラミングの問題を自動で解けることの例になっている。

競技プログラミングのソルバは (初めは) トランスパイラの形がよいだろう

さて、問題を自動で解くことが不可能ではないことが分かった。可能性についての話題ではなく、より具体的なソルバについての話題へ移ろう。

ソルバの入力は「形式化された問題」だろうと言ったが、では「形式化された問題」というのは具体的に何にするとよいだろうか？ $(\text{入力となる変数}, \text{出力となる変数}, \text{それらが満たすべき制約})$ という $3$ つ組だろうか？計算可能な関数のグラフだと考えるべきだろうか？これはおそらく何でもよい。問題を表現できてさえいれば、入力の選択によって問題が解けたり解けなかったりするといったことはあまりないだろう。好きなものを使えばよい。

しかしソルバへの入力形式はソルバ自体の実装のしやすさを大きく左右する。どのような入力にするのはもっとも楽だろうか？何度かプロトタイプを実装した経験から、私は「実行可能なプログラム」を「形式化された問題」の代わりに使うのがよいと考えている。「実行可能なプログラム」をソルバの入力とすれば、競技プログラミングの過程は以下の 3 ステップに具体化される。

読解: (人間が) 自然言語で与えられた問題を解釈し、数学的な問題として整理する
実装”: (人間が) 数学的な問題を、計算機上にその愚直解として実装する
考察”: (ソルバが) 記述された実装に対し、計算量的な最適化を行う

このとき (3.) の「考察”」のステップは、入力も出力も共にプログラミング言語である。入力されたコードと同じ計算をするより高速なコードを出力する。これは「最適化」である。つまり「実行可能なプログラム」をソルバの入力とすれば、「競技プログラミングの問題を自動で解くソルバ」は「最適化を伴なうトランスパイラ」となる。

「競技プログラミングの問題を自動で解くソルバ」を「最適化を伴なうトランスパイラ」と言い換えられた。これは大きな進歩である。「なにやらよく分からないすごそうなもの」ではなく「いつもの」を書けばよいことになった。「人工知能」と比べれば「コンパイラ」はたいへんに開発しやすい。既存の技術や資料をたくさん利用できる。また、入力と出力のギャップが小さいことも利点である。入力をそのまま出力するだけのプログラムでさえ、いまや「自明なソルバ」だと主張できる。

ところで、「形式化された問題」として「実行可能なプログラム」使うことのギャップは大きい。答えを先に聞くとギャップは感じず自然に聞こえるかもしれない。しかし思い出してほしいのは、「問題」と「プログラム」はまったく異なるものだということである。プログラムは実行できるが、問題は実行できない。プログラムは漸近的計算量を持つが、問題は漸近的計算量を持たない。少なくとも私はいくつかのプロトタイプを作るまでこのギャップを乗り越えられなかった。

競技プログラミングのソルバは (近い将来においては) 定理自動証明機に近づいていくかもしれない

より多くの競技プログラミングの問題を解きたいと思えば、より高度な考察が必要である。たとえば「この述語 $p$ は単調性を持つのでこの部分は二分探索でよい」だとか「この関数 $f$ は Monge 性を持つので探索範囲を絞れる」などを自動で判断して最適化してほしいと思うと、それには「述語 $p$ が単調性を持つこと」「関数 $f$ が Monge 性を持つこと」などを自動で証明できる必要がある。つまり、与えられた条件下で何らかの命題を自動で証明する必要がでてくる。するとソルバは「定理自動証明機」と呼ばれるものに近づいていくだろう¹⁰。

この変化と同時に、ソルバの入出力も変化していくだろう。すでに説明したように、おそらく始めに実装されるソルバの入力は「実行可能なプログラム」だろう。通常のプログラミング言語のソースコードを入力とし、計算量的な最適化がなされた機械語やその他の言語のソースコードを出力とするというものである。しかしある時点で「形式化された問題」を入力とするものに戻るだろう。形式化された問題 (つまり、条件の集合のような、必ずしも実行可能とは限らないもの) を入力とし、解法となるアルゴリズムやソースコードを出力とする方が、より柔軟で使いやすいソルバになるだろうからである。

競技プログラミングのすべての問題が自動で解けるわけではない

言うまでもないことだろうが、競技プログラミングのすべての問題が自動で解けるわけではないことを注意しておく。期待しすぎるべきではない。機械的な解法と相性の良い問題は解けるだろうが、相性の悪い問題は解けない。少なくともしばらくの間は、再翻訳がおもしろおかしいものだった時代の機械翻訳と同程度の有用性がせいぜいのはずである。

相性の悪い問題にはたとえば以下のようなものがある。

愚直解の実装が難しい問題
「直感」や「ひらめき」を必要とする問題
問題そのものが複雑な問題

(1.) は、たとえば幾何の問題である。ソルバの担当範囲以外の部分が難しい。そのような場合は人間が頑張るしかない。考察要素がある問題であってもその考察要素が「愚直に実装するとたいへんだが、うまく工夫すると実装量を減らすことができる」という形であれば、やはりソルバは無力である。 (2.) は、たとえば貪欲法が想定解の問題である。ソルバの担当範囲が難しい。実装にもよるだろうが、基本的にソルバは 1 歩ずつ考察を詰めていけば解けるような問題しか解けないだろう。「証明はできないけどなんとなく正しそう」のような判断は機械とは相性が悪そうである。「突然ですが、ここで $x = f(y, g(y, z))$ とおきます。すると……」のような発見的解法も機械とは相性が悪そうである。手法によっては扱えるかもしれないが、少なくとも、先程の節で述べたような形の機械的解法で解くことはできない。 (3.) は、たとえばゲームの問題がそうだろう。交互ゲームで「先手が必勝である」ことを表現しようと思うだけで、量化子の繰り返しや再帰関数のような扱いにくいものが出てきてしまう。きれいな式で表現できないような問題と機械の相性は悪いだろう。

ソルバを活用するにはそれなりの能力が要求される。愚直解を素早く書けることは大前提である。そして、ある問題がソルバで解けるか解けないかを判断する能力が必要である。そのような能力がなければ「時間をかけて愚直解を書いたのに解法は発見されなかった」という事態に終わることがたいていだろう。また、そのような能力を持つ人は、ソルバなしでも問題を解けるだろう。

競技プログラミングの自動化は競技プログラミングをより面白くするはずである

競技プログラミングの自動化の技術が発達すると、競技プログラミングの面白さは失われるだろうか？そんなことはないだろう。競技プログラミングはむしろより面白くなると予想している。理由はいくつかあるが、重要なのは以下の 2 点であろう。

すべての問題が機械的に解けるわけではないので、機械的には解けない問題が出題されるようになる
機械的に解けてしまうようなつまらない部分を機械に任せることで、人間はより面白い部分に注目できる

(1.) は OEIS を思い出せば理解できるだろう。出題者は出題前にソルバに入力してみて解けるかどうか確認するだけでよい。

(2.) についても同様のものはたくさん存在している。たとえば Dinic 法は、それをブラックボックスとして使えば「問題を最大流問題の形に帰着させればあとは適当に解いておいてくれるすごいソルバ」だと理解できる。top tree や wavelet matrix のような高度なアルゴリズムやデータ構造など、「ライブラリ」はたいていそのような性質を持つ。 AC Library は「中身のアルゴリズムについて理解していなくても貼れば convolution や floor_sum を計算してくれるすごいソルバ」である。あるいは Wolfram|Alpha を思い出してもよい。これらによって競技プログラミングがつまらなくなったということはない。むしろ出題される問題の幅が広がって面白くなったとさえ言えるだろう。

よって、競技プログラミングのソルバは「ある程度まで人間が考察した後、残りの自明な部分を機械に押しつける」ような使われ方をすることになるだろう。たとえば C++ のソースコードを機械語のバイナリに変換する操作を機械 (GCC や Clang) にやってもらうのと同様である。

実現可能性を示すための実装例はすでに作った

その実現可能性を示すための実装例もすでに存在している。去年 (2019 年) の夏頃に私が簡易なものを実装しておいた (kmyk/Jikka (v3.1.0), その時書かれた解説 PDF) 。このプログラムは、ML 風の言語で表現された競プロの問題を入力とし C++ のコードを出力する。

例題として問題 AtCoder Beginner Contest 134: C - Exception Handling を使おう。まず問題文をそのまま翻訳してできる愚直解のような ML 風のコードを書く。これは与えられた $N, A$ に対し長さ $N$ の数列 $f$ (つまり $\lbrace 0, 1, \dots, N - 1 \rbrace$ から $\mathbb{Z}$ への関数 $f : \lbrace 0, 1, \dots, N - 1 \rbrace \to \mathbb{Z}$) を返す $O(N^2)$ のコードである¹¹。

let given N : [2, 200001) in
let given A : N -> 200001 in

let f (i : N) = max N (fun j -> if j = i then 0 else A j) in
f

この ML のコードを入力すると以下のような C++ のコードを出力される。これは $O(N)$ である。これを人間が手で main 関数を付け加えて¹² AtCoder に提出して AC した結果は https://atcoder.jp/contests/abc134/submissions/6526623 にある。

vector<int64_t> solve(int64_t N, const vector<int64_t> & A) {
    vector<int64_t> t1(N + 1);
    t1[0] = INT64_MIN;
    for (int i1 = 0; i1 < N + 1 - 1; ++ i1) {
        t1[i1 + 1] = ((0 <= i1) ? max<int64_t>(t1[i1], A[i1]) : INT64_MIN);
    }
    auto & g1 = t1;
    vector<int64_t> t2(N + 1);
    t2[0] = INT64_MIN;
    for (int i2 = 0; i2 < N + 1 - 1; ++ i2) {
        t2[i2 + 1] = ((((N - i2) - 1) < N) ? max<int64_t>(t2[i2], A[((N - i2) - 1)]) : INT64_MIN);
    }
    auto & g2 = t2;
    vector<int64_t> t3(N);
    for (int i3 = 0; i3 < N; ++ i3) {
        t3[i3] = max<int64_t>(max<int64_t>(max<int64_t>(INT64_MIN, g1[i3]), g2[(((N - (i3 + 1)) - 1) + 1)]), 0);
    }
    auto & f = t3;
    return f;
}

実用レベルのものを目指して、いま頑張って実装をしているところである

コンテストの本番で使えるような実用的なソルバを目指して実装作業中である¹³。作業レポジトリは kmyk/Jikka にある。ただし、書き直し始めたばかりであり、現在 (2020 年 12 月時点) はまだ実用に耐えるものではない¹⁴。先日やっと入力から出力までが繋がったばかりである。

Python から C++ へ、動くものが書けました pic.twitter.com/AXDxgwSCty
— kimiyuki@うさぎ🐇 (@kimiyuki_u) December 3, 2020

このソルバは Python から C++ へのトランスパイラとなっている。ただし入力の Python はかなり制限されたサブセットとなっており、通常の Python と一定の互換性を持つような静的型付き純粋関数型言語として解釈される。内部的には GHC Core (Haskell の処理系である GHC の内部言語) を参考にした内部言語に変換し、その上で rewrite rules のような最適化を行う。

競技プログラミングのソルバは遠い将来においては何になるだろうか？

競技プログラミングのソルバはトランスパイラから始まり、まずは定理自動証明機に向けて進んでいくだろうと議論した。ではその先のソルバはどのようなものになるだろうか？究極的なことを言えば「強い人工知能」だとか「シンギュラリティ」のような威勢のよい (そしてありふれた) 話になってしまうが、もっと面白い展望はあるだろうか？余談として、このような話題についても言及しておこう。

実現可能性を気にせず夢のようなことを語ってよいとすれば、競技プログラミングのソルバはいつか「新しい種類のプログラミング言語のコンパイラ」になると考えている。ただしそのプログラミング言語のソースコードは我々の知る「プログラム」ではない。「競技プログラミングのソルバはトランスパイラから始まるだろう」という議論において、ソルバの入力は、実行できない「問題」から実行できる「プログラム」へとギャップを越えたと話した。次はこのギャップを逆向きに越える。するとコンパイラは「実行の概念を持たない仕様のようなもの」を入力として「実行可能なプログラム」を出力するものになる。夢のような話だが、この予想はまったく荒唐無稽というほどではない。たとえば関係データベース管理システム (RDBMS) は SQL のクエリを入力とし、クエリを解析して最適な実行計画を自動で判断して処理を実行する。これは今回の予想のものとかなり近い。

競争相手を募集している

競技プログラミングの問題を解くソルバを作ることは可能である。上記の説明を読めば、競技プログラミングとコンパイラ開発の両方に詳しい人間であれば、ソルバの実現が可能であることに同意してくれるだろうと思っている。

競技プログラミングのソルバの開発に複数の人間が挑戦することは、挑戦者全体の開発速度を上昇させるだろう。私は数理論理学や分析哲学などに近い位置にいるため、どうしても発想が古典的な記号処理の方向に寄る。異なる分野の人、たとえば機械学習に親しい人であればなにか違う発想がでるかもしれない。問題と解法のデータベースを作って統計的な手法で解法を生成してもよいだろう。あるいは解法データベース上の精度のよい検索だけでも有用かもしれない。あるいは自動化のレベルを落として人間の手を借り、たとえば Akinator や Coq のように対話的に問題を解くこともできるだろう。様々な発想によるソルバが実装され試されれば、より優れたソルバに辿り着きやすくなる。

ということで、興味があればぜひソルバ開発に挑戦してみてほしい¹⁵。将来的には競技プログラミングのソルバを投稿して競うメタなオンラインジャッジの運営も検討している。

先行研究

一般のものであれば、以下のものが近いだろう。

競技プログラミングでの利用を意図したものに限れば、以下のような事例がある。

個別の問題のソルバとしては wata による「Σ電卓」が知られている (wata-orz/SigmaCalculator, Σ電卓 - てきとーな日記) (2009 年)。
実装には至っておらず構想のみであるが、一般の問題の解法の自動生成についての試みが kinaba によってなされている (SRM 531 Div2 250 - cafelier@SRM - TopCoder部など) (2012 年)。
AtCoder Regular Contest のある A 問題の解法の完全自動生成が mkotha によって行われたことがある (https://twitter.com/atcoder/status/538665089931296768, https://atcoder.jp/contests/arc030/submissions/286413) (2014 年)。
最適化などは含まれていないが、競技プログラミングでの利用を意図して作られた言語としては laycurse による cLay がある (cLay概要（version 20201123-1） - ゲームにっき（仮）別館（仮）) (2107 年から)。

一般の競技プログラミングの問題を解くソルバを目指しているものとしては、ある程度の形になっているものは見つけられていない。

言語実装 Advent Calendar 2020

この記事は言語実装 Advent Calendar 2020 の 9 日目の記事です。前回は cympfh さんの「設定ファイル言語 cumin を自作している」で、次回は Drumato さんの「Guide to Rustc Developmentを読んでRustcのアーキテクチャを解説します」です。

注釈

この 3 ステップへの分類は妥当だろうか？これが妥当であることを言うには (a.) 「これら 3 ステップがすべて異なる」, (b.) 「これら 3 ステップのうちに削除してしまえるようなものがない」, (c.) 「これら 3 ステップにさらに追加すべきであるような 4 個目のステップはない」, (d.) 「これら 3 ステップの順序は正しい」の 4 点をそれぞれ確認すればよい。(a.) と (b.) は明らかだろう。(c.) はすこし怪しい。たとえば「デバッグ」などはここに含めてもよいかもしれない。しかし今回はそのような「ミスをする」という「人間の競技プログラマに特有の性質」は無視することにすれば (c.) は大きく間違っていないだろう。同様に「誤読」「勘違い」「バグ」のようなミスによる手戻りがないと仮定すれば、(d.) の順序も正しい。よってこの 3 ステップへの分類は妥当である。 ↩
これはひとつのモデル化でしかない。すべての人間がすべての問題を常にこのように解いているという主張ではない。たとえば「数学的な問題」などと言っても、述語論理の論理式として書き下せるレベルまで落とし込む人もいれば、小学校の算数の文章題のレベルまでしか整理しない人もいるだろう。「考察」の途中である程度解けそうだと思えばその時点で「実装」も初め、両者を同時に進める人もいるだろう。問題文中に長大な表が含まれているなどすれば問題の全体を同時に認識することが難しく、このとき「読解」というステップは曖昧になるだろう。 ↩
その問題がどのようなストーリーを持つかの情報は忘れてしまってよい。「りんごが 2 個とみかんが 3 個あります。くだものはぜんぶで何個ありますか？」というストーリーに対する “2 + 3” という式であっても「うさぎが 2 羽いました。いつのまにか 3 羽増えました。いま何羽いますか？」というストーリーに対する “2 + 3” という式であっても、これら “2 + 3” はまったく同様に計算できるからである。このような普遍性は数学の特徴のひとつである。今回のモデル化における「数学的な問題として整理する」とは、「数式で書く」というより、このように「普遍的で明確な形にする」という性質が強い。 ↩
モデル化の上ではストーリーを持つかの情報はまったく捨てられてしまいそれ以降まったく利用されないが、これは実際とは異なるかもしれない。適切なストーリーは直観的な理解を助けるためである。そのような例としてはウェイソン選択課題が有名である。 ↩
このことは、他のステップに比重を置いた問題があまり歓迎されないことから言える。考察の部分が難しい問題は「良問」とされるが、読解の部分が難しい問題は「Readforces」「エスパー問」「注意力コンテスト」などと批判される。実装の部分が難しい問題も「重実装」として避けられがちであるし、「競プロは自動採点機能付き数学コンテストである。実装パートは蛇足」のような主張がされることもしばしばある。 ↩
この 5 つの他に、結合律や対称律なども必要である。 ↩
Merge Cards, Kick Start 2020 Round G - Google’s Coding Competitions ↩
そして、人間の手ではやりたくない。時間がかかるしすぐ間違える。 ↩
実際には、ここからもうすこし定数倍の最適化をしてから提出して AC した。たとえばキャッシュ効率のために dp_sum_l の添字ふたつを入れ替えるなどである。もちろんこのような定数倍の最適化も機械的に可能だろう。 ↩
ちなみに、以前はいきなりそのようなものを作ろうとして泥沼にはまった。依存型は難しい。一般的な数学の証明を扱いたいのではなく最適化に必要ないくつかの性質を見抜きたいだけなので、まずはできるだけ個別的な証明方法を考えるのがよいだろう。 ↩
このときの言語には表示的意味論は与えられていたが、操作的意味論が与えられていなかった。「プログラム」というより「問題」を入力としていたので、実行や計算の概念は曖昧であった。ゆえに漸近的計算量の概念も曖昧である。しかしここではそれは無視しておく。計算方法を自然に補ってやれば $O(N^2)$ になることは明らかだろう。 ↩
ちなみに、問題文を解析して main 関数を (入出力を含めて) 実装してくれるツール online-judge-tools/template-generator もすでに作ってある。このツールの実装も内部はほとんどコンパイラなものになっている。 ↩
去年の夏から開発が止まっていたのは、正直に言うと「実装が面倒なのでさぼっていた」である。しかし最近は私の実装力が落ちてきてもう手でコードを書くのがしんどく、しかたがないので自動化のためのプログラムを実装している。 ↩
まあ書けば書けると思うのでもうすこし待っていてほしい。 ↩
競技プログラミングには詳しいがコンパイラ開発にはあまり詳しくない人に向けて: このようなソルバの開発に挑戦したいと思うと、構文解析が最初の壁となる。しかしソルバの目的を考えると構文解析は非本質的な前処理でしかない。言語機能を大きく制限するだとか、構文解析は他のツールに任せてしまい、入力も出力も構文木にしてしまうなどがおすすめである。たとえば Python 標準ライブラリ ast モジュール (ast — 抽象構文木 — Python 3 ドキュメント) には Python のソースコードを構文解析する機能がある。 ↩