Verification of a DPLL Transition System in Rocq

コンピュータが常に「真か偽か」という高額な賞金がかかったゲームをプレイしている、そんな世界を想像してみてください。このゲームでは、コンピュータには「もし砂糖を加えるなら、小麦粉も加えなければならない。しかし、もし小麦粉を加えるなら、塩を加えてはならない」といった、論理的な記述が複雑に絡み合った巨大な結び目のレシピが手渡されます。目標は、ルールを破ることなくそのレシピに従う方法を見つけることです。これが充足可能性（SAT）問題です。これは、何百万もの異なるパズルのピースを、あるピースは赤、あるピースは青であり、「赤の隣に青を置いてはいけない」という指示がある箱の中に、うまく収めようとする作業のデジタル版といえます。

なぜこれが重要なのでしょうか？ なぜなら、これは単なる論理パズルではなく、コンピューティングにおけるほぼすべての複雑な事象の背後にあるエンジンだからです。マイクロチップの設計から、数学的定理が正しいことを証明することに至るまで、コンピュータはこれらの巨大な論理の迷路を通り抜けるためにSATソルバーを使用します。しかし、ここに落とし穴があります。これらのソルバーは非常に複雑です。もしコードの中に小さなバグが隠れていれば、コンピュータは実際にはデタラメであるにもかかわらず、自信満々に「この証明は有効である」とあなたに告げてしまうかもしれません。だからこそ、数学者やコンピュータ科学者は**形式検証（formal verification）**に執着しているのです。これは、超厳格で壊れることのない安全網を構築することだと考えてください。コンピュータが正しく動くことを単に期待するのではなく、彼らは「証明助手（proof assistant）」と呼ばれる特別な種類の「数学的顕微鏡」を使用して、論理のあらゆるステップをチェックし、マシンが決して答えについて嘘をつかないようにするのです。

この論文の大冒険：信頼できる論理マシンの構築

この論文において、Julia DijkstraとBenedikt Ahrensは、これらの論理マシンを信頼できるものにするための大きな一歩を踏み出しました。彼らは単にプログラムを書いたのではありません。彼らは、Rocqというツールの中で、DPLL（Davis-Putnam-Logemann-Loveland）と呼ばれる有名な論理解決手法の数学的に証明された骨組みを構築したのです。

DPLL法を、単にスクリプトに従う硬直したロボットとしてではなく、「状態遷移（State Switching）」のゲームとして考えてみてください。探偵がミステリーを解こうとしている場面を想像してください。探偵は空のノート（手がかりなし）を持ってスタートします。彼らには、ノートを更新するためのルールがいくつかあります。

1. 「なるほど！」ルール（単一伝播 / Unit Propagate）： もし手がかりが「執事が犯人、あるいはメイドが犯人である」と言っており、探偵がすでに「メイドは無実である」と知っている場合、ノートは必ず「執事が犯人である」と更新されなければなりません。探偵には選択の余地はなく、論理がその動きを強制します。
2. 「純粋な推測」ルール（純粋リテラル / Pure Literal）： もし探偵が「庭師」に関する手がかりを見つけたものの、「庭師はやっていない」という手がかりを一度も見かけなかった場合、矛盾を恐れることなく、庭師が関与していると安全に推測できます。
3. 「枝分かれ」ルール（決定 / Decide）： もし探偵が行き詰まったら、ランダムな手がかり（例えば「執事が犯人である」）を選び、それを一つの決定として書き留めます。これは道の分かれ道です。
4. 「おっと、踏み間違い」ルール（バックトラック / Backtrack）： もし探偵が決定を下した後、後に矛盾（「執事は犯人ではない」という手がかり）を見つけた場合、その決定の後に起こったすべての出来事を消去し、決定を反転させ（今度は「執人は犯人ではない」とする）、やり直さなければなりません。
5. 「ゲームオーバー」ルール（失敗 / Fail）： もしすべてを消去し、最後の決定を反転させても、依然として矛盾に突き当たった場合、ゲームは終了です。そのミステリーは解決不可能です。

著者たちの主な成果は、このゲーム全体を取り上げ、Rocqの証明助手が読み取り、検証できる言語で書き記したことです。彼らは単に「これは正しそうだ」と言ったのではありません。彼らは以下の3つの巨大な事項を証明しました。

• 正当性（Correctness）： もしゲームが解決策とともに終了した場合、その解決策は間違いなく本物です。コンピュータがモデルを幻視することはありません。
• 完全性（Completeness）： もし解決策が存在する場合、ゲームは必ずそれを見つけ出します。コンピュータが途中で行き詰まったり、出すべき時に諦めたりすることはありません。
• 停止性（Termination）： ゲームが永遠に走り続けることはありません。解決策が見つかるか、あるいは「ゲームオーバー」になるかのどちらかであり、数学的に停止することが保証されています。

新しいひねりを加える：「純粋」ルール

この論文の面白い貢献の一つは、従来の理論のいくつかのバージョンでは欠落していた特定のルール、すなわち**純粋リテラル・ルール（Pure Literal Rule）**をゲームに追加したことです。探偵の比喩で言えば、これは探偵が「おや、庭師に対して否定的な証拠を一度も見かけていないので、庭師が犯人だと仮定しておこう」と気づく瞬間です。著者たちは、このルールを追加することで、安全性の保証を損なうことなくゲームを高速化できることを証明しました。このショートカットを用いても、論理が依然として隙のないものであることを彼らは示しました。

理論から現実の（しかし単純な）ロボットへ

理論においてゲームのルールが完璧に機能することを証明した後、著者たちは問いかけました。「実際にこのゲームをプレイするロボットを作れるだろうか？」 彼らは、次にどのルールを選ぶべきかという探偵への指示セットである**戦略（strategy）**を作成しました。彼らはこの戦略の具体的なバージョンをRocqの中に構築し、その後、抽出（extraction）と呼ばれる魔法のようなツールを使用して、彼らの数学的証明をOCamlで書かれた実際のコンピュータプログラムへと変換しました。

彼らはこの新しいロボットをいくつかの単純なパズルでテストしました。それは機能しました！ zebra.cnf という、155個の変数と**1,135個の節（clause）を持つパズルを含め、問題を正しく解決しました。しかし、著者たちはこのロボットの限界についても非常に正直です。それは、プロトタイプの模型車のようです。エンジンが機能していることは証明していますが、まだF1カーではありません。現実世界のレーシングカーが高速メモリを使用するのに対し、このロボットは手がかりを記憶するために単純なリストを使用しているため、動作が遅いのです。著者たちは、このバージョンが今日の企業で使用されている産業用レベルのソルバーに勝てる段階にはないことを認めていますが、これは検証済みのコア（verified core）**なのです。それは、将来のより速く、よりスマートなソルバーを構築するための、小さく、決して壊れない基礎です。

未来への意味

この論文は、世界最速のSATソルバーを作る問題を解決したと主張しているわけではありません。代わりに、彼らは最も安全な設計図を作ったと主張しています。Rocqで抽象的なルールを証明することで、彼らは「信頼できるコア」を作り上げました。将来の研究者は、この設計図を受け取り、現代的なソルバーの特徴――例えば「間違いから学ぶ（節学習）」や「複数のステップを一気に戻る（非逐次的バックトラック）」など――を、基礎となる論理が依然として健全であるという確信を持って追加することができます。

要するに、DijkstraとAhrensは単により良い車を作ったのではありません。彼らは決して衝突することのない車の設計図を作り、その車輪の背後にある論理が数学的に完璧であることを証明したのです。それは、将来のより大規模で、より複雑で、信頼できる論理マシンへの道を開く、検証された小さな一歩なのです。