From Dag-Like Proofs to Boolean Circuits in Lean

あなたは、あらゆるピースが論理的な議論である、巨大で複雑なパズルを解こうとしているところだと想像してください。コンピュータサイエンスや数学の世界では、これは「形式検証（formal verification）」と呼ばれます。これは、コンピュータプログラムや数学的定理が、隠れたバグや論理的な穴のない、完全に正しいものであることを証明するプロセスです。これを行うために、数学者は「自然演繹（Natural Deduction）」を用います。これは、家族の系図のようなものに見える、ステップバイステップの証明構築法です。あらゆる結論は、前のステップから枝分かれし、巨大で広大な論理の木を作り上げます。

しかし、これらの証明が大きくなるにつれ、木は巨大で乱雑になります。同じ場所から何度も同じ枝が生えているような、多くの重複が含まれるのです。これでは、証明のチェックが遅く、困難になります。これを解決するために、研究者は「水平圧縮（horizontal compression）」という手法を用います。この巨大な木を取り、同一の枝が単一の共有パスへと統合されるように押しつぶす様子を想像してください。その結果、それはもはや「木」ではなく、「DAG型導出構造（DLDS）」となります。これは、パスが交差し、合流することができるマップであり、膨大なスペースを節約できます。しかし、ここが厄藉な点です。マップが小さくなったからといって、それが読みやすいとは限りません。圧縮されたマップが依然として有効な証明であるかどうかをチェックすることは、絡み合った地下鉄の路線図の中で、迷うことなく単一のルートを辿ろうとするようなものです。

ここで、論文内の物語が登場します。著者であるLorenzo SaraivaとEdward Hermann Haeuslerは、大胆な問いを投げかけます。「この複雑で圧縮された証明のマップを、さらに単純で機械的なものに変えることはできるだろうか？」彼らは、これらの複雑な論理構造を「ブール回路（Boolean circuits）」へと翻訳する方法を提案しています。ブール回路を、シリコンの破片としてではなく、スイッチとワイヤーで作られた巨大で硬直したグリッドとして考えてください。証明のパスを辿る代わりに、あなたはスイッチの一組を操作し（これはパスの割り当てを表します）、ライトの様子を見守るだけです。もし、最後にライトが正しいパターンで点灯すれば、その証明は有効です。そうでなければ、無効です。

この論文は、「純粋含意最小論理（purely implicational minimal logic）」と呼ばれる特定の論理における、あらゆる圧縮された証明に対して、この回路を構築する方法を提示しています。彼らは、特定のスイッチ操作（「パス割り当て」）に対して、その回路が論理規則に従っているかどうかを正しく計算できることを示しました。彼らは単に推測したわけではありません。彼らは「Lean」という強力なコンピュータツールを使用して、彼らの回路構築が完璧に機能することを、形式的にマシンチェックされた証明として書き上げました。これは、ロボットが自分自身の設計図をダブルチェックするロボットを作るようなものです。彼らは、すべてのパスを瞬時にチェックすること（それは非常に困難です）は解決していませんが、彼らの回路が、提示されたあらゆる単一のパスに対して信頼できる、一様な検証手段であることを証明しました。これは、証明のチェックという乱雑な作業を、クリーンで電気的な「オンとオフのゲーム」へと変え、将来的に量子コンピュータのような新しい超高速技術を用いて証明を検証できる道を開くものです。

主な発見：論理を「光るグリッド」へと変える

この論文の核心的な成果は、これらの圧縮された証明に対する「一様なブール評価（uniform Boolean evaluation）」の作成です。著者たちは、DLDS（圧縮された証明マップ）がどのように機能するかを規定する複雑なルールを取り上げ、それらを固定された論材ゲートのグリッドへと翻訳しました。

証明を都市のグリッドとして想像してみてください。従来の方法では、ルートが有効かどうかをチェックするために、街路を歩き回り、あらゆる交差点を見て、交通信号が正しく機能しているかを確認しなければなりませんでした。これは遅く、その特定の都市のレイアウトに完全に依存していました。著者たちの新しい手法は、あらゆる可能な交差点が潜在的な「セル」として存在する、巨大な既製品のグリッドを構築します。あなたは街を歩くのではなく、代わりにグリッドに指示（「パス割り当ても」）を渡します。「これらの特定の通りに明かりを灯し、残りは無視せよ」という指示です。

そして、回路は巨大な自動検査官として機能します。回路は主に2つのことをチェックします：

1. ルートは適切に形成されているか？ あなたは、有効な論理ステップ（含意の導入や除去など）のシーケンスを選びましたか？ もし何も接続されていないランダムな通りを選んだ場合、回路はそれを「無効（Invalid）」と判定します。
2. 仮定は解消されているか？ 論理においては、しばしば一時的な仮定（例えば「Xが真であると仮定しよう」）から始まります。有効な証明は、最終的にXがもはや重要ではないことを証明しなければなりません。回路は「依存ビット文字列（dependency bitstring）」、つまりどの仮定がまだアクティブであるかを表すライトの文字列を追跡します。もし、ルートの最後において、すべてのライトが消えていれば（つまり、残された仮定がない状態であれば）、回路は「受理（Accepted）」と答えます。

論文は、選択された任意の単一のパスに対して、この回路が完璧に機能することを証明しています。彼らはこれを「点別的な正当性（pointwise correctness）」と呼んでいます。これは、特定のスイッチ操作を与えれば、回路がその特定のパスについて真実を告げることを意味します。

この論文が否定し、明確にしていること

この論文が何を主張していないかを理解しておくことは極めて重要であり、著者たちも非常に慎重に記述しています。彼らは、この手法が伝統的な意味でチェック全体を高速化するものではないことを明示しています。

「グローバル」な条件、すなわち「すべての」パスに対して証明が有効であるかどうかをチェックすることは、依然として非常に困難です。論文では、可能なパスの数は指数関数的（証明が大きくなるにつれて猛烈に増加する）であると指摘されています。回路は、この膨大な計算を魔法のように瞬時に解決するわけではありません。代わりに、著者たちは問題を再定義しています。回路は個々のパスをチェックするためのツールであり、「証明全体の妥当性」は、それらすべてのパスの一つひとつがチェックを通過するという事実として定義されます。

また、彼らは、古典的なステップバイステップの検証において既存の「Flow」関数（これらの証明をチェックする標準的な方法）を改善すると主張しているわけでもないと明確にしています。真の価値は、現在のチェックを速くすることではなく、チェックの「形式」を変えることにあります。証明をブール関数（巨大なオン/オフのマシン）へと変換することで、彼らは量子コンピューティング技術のような、異なる種類の検証手法への扉を開いています。これらは、従来のコンピュータでは不可能な方法で、これら膨大な「全パス」のチェックを扱うことができるかもしれません。

確信の度合いはどの程度か？

著者たちは非常に自信を持っていますが、それは非常に限定的かつ厳密な方法によるものです。彼らは単にコンピュータ上でシミュレーションしたり、うまくいくと推測したりしたわけではありません。彼らは形式的に証明したのです。

彼らは、Lean証明助手を用いて、彼らの構築物全体の形式的な検証を書き上げました。これは、コンピュータが彼らの数学的証明を一行ずつ読み取り、そこに論理的な欠陥がないことを確認したことを意味します。

• 証明済み： 「点別的な正当性」は数学的事実です。固定されたパスに対して、回路は論理が要求する通りに動作します。
• 証明済み（制限付き）： 彼らは、この回路を元の証明構造へと結びつける「架け橋」を証明しましたが、それは「非圧縮の単純な木断片」と呼ばれる、より単純なタイプの証明に対してのみです。
• 今後の課題： 彼らは、「祖先エッジ（ancestor edges）」や再帰的なフロー条件を含む、完全に圧縮された複雑なケースに対する架け橋については、まだ証明していないことを認めています。彼らはこれを、今後の研究課題として残しています。

実践における「ライトアップ」の比喩

これを視覚化するために、数千の小さな電球がグリッド状に配置された、巨大で透明なボードを想像してください。各行は証明のステップを表し、各列は異なる論理式を表します。

• 入力： あなたは、長いボタンリストが付いたリモコンを持っています。各ボタン操作は、次の行との間のどの「ワイヤー」を点灯させるかをボードに伝えます。これがあなたの「パス割り当て」です。
• 回路： ボードの内部には、小さな論理ゲートがあります。もしあなたが「前提A」から「前提B」へとつながるワイヤーを点灯させ、それによって「結論」を形成した場合、ゲートは次のようにチェックします：「これは論理のルールに一致しているか？」もし適合しない二つのものを繋ごうとした場合、ゲートは消灯するか、赤色のエラーライトを点滅させます。
• 出力： ボードの最下部には、単一の「ゴール（Goal）」ライトがあります。もしあなたがすべてのルールに従ったパスを辿り、すべての仮定を正常に「解消」したのであれば、ゴールライトは緑色に点灯します。もしステップを飛ばしたり、仮定を宙に浮かせたままにしたりした場合は、ライトは赤色のままです。

この論文の画期的な点は、どのような圧縮された証明に対してもこのボードを構築できること、そして、どれほど複雑な証明であっても、ライトの振る舞いのルールは常に同じであるということを示した点にあります。これは、抽象的で乱雑な論理的演繹の技術を、スイッチを操作してライトを観察するという、具体的で機械的なプロセスへと変えるものです。

なぜこれが重要なのか

これは純粋に理論的な演習のように聞こえるかもしれませんが、コンピューティングの未来に大きな影響を与えます。証明をブール回路へと翻訳することで、著者たちは現代のハードウェアのネイティブ言語を話しているのです。これにより、量子コンピュータのような高度な技術を用いて、証明を検証することが可能になります。

結論において、著者らは、私たちが「振幅増幅（amplitude amplification）」（量子技術の一種）を用いて、膨大な全パスの空間を探索し、有効なパスを見つけ出したり、あるいは無効なパスが一つも存在しないことを証明したりできる未来を示唆しています。また、これはコンピュータが自ら複雑な数学的問題の証明を見つけ出そうとする「自動定理証明」にも役立つ可能性があると言及しています。

論文は、基礎（回路と、単純なケースにおけるその正当性の証明）は構築したが、完成した建物（複雑で圧縮されたケース）はまだ建設中であることを認めて終わります。しかし、彼らは、複雑に絡み合った論理のウェブを、クリーンで電気的なグリッドへと変える方法を正確に示す、マシンによって検証された完璧な設計図を、建設者たちに手渡したのです。