なぜ数学（一人では）私たちが助けられないのか：ソフトウェア検証の計算量理論的限界

カーリーオンでの再講演に感謝いたします。昨年は継続体とモナドについてご講演し、今年はソフトウェア検証における計算量理論の結果について講演しました。対象は現在開発中の「ギャラクシー（Galaxy）」プロジェクトです。本記事は講演の拡大版であり、正しいプログラムを書くことの根本的な困難さを解説します。

1. プログラムと正しさの関係：完全な理解との不可避な矛盾

計算可能性理論と計算量理論の主要結果をレビューし、以下を明らかにします。

• 「完全な理解」は不可能である： プログラムの正しさを保証するには多大なコストがかかります。これはエントロピーを減少させるためのエネルギーコストと同様に、**回避不可能な計算の「自然法則」**によるものです。
• ツールの限界： ツールが助けになりますが、それだけでソフトウェアの正しさが容易に達成されるわけではありません。
• 本記事の目的： 正しいソフトウェアを生み出す困難さに関連するいくつかの結果を単一の場所に集約し、誤った楽観論への反駁を行うことです。

2. 第 1 章：基礎 —— 形式的証明の不可能性

理論的なコンピューターサイエンスは、数学的形式化の限界に直面しています。

ヒルベルトの計画とゲーデルの不完全性定理

• ヒルベルトの目標： すべての数学を形式化し、以下の 3 つを満たす体系的な証明を目指しました。
  • 一貫性： 体系内で矛盾が生じないこと。
  • 完全性： すべての真の命題が証明できること。
  • 判定可能性（Entscheidungsproblem）： 任意の文の真偽を決定するアルゴリズムが存在すること。
• 崩壊： デービッド・ヒルベルトの計画は、カール・ゲーデルによって以下の定理によって破られました。
  • 第一不完全性定理： 一貫な形式体系内では、すべての真の命題を証明することはできません。
  • 第二不完全性定理： 体系的な一貫性を証明することもできません。

停止定理（The Halting Theorem）：計算科学の最初の定理

• 発見： 1936 年、アラン・ターリングとアルロンゾ・チャーチにより独立して証明されました。
• 核心： 与えられたプログラムがいつ停止するかを決定するアルゴリズムは存在しません。
• 証明の概要（対角化法）：
  • プログラム $H(M, x)$ が「$M$ が $x$ で停止すれば TRUE、ELSE FALSE」であると仮定します。
  • 次にプログラム $G(y) = \text{if } H(y, y) \text{ then loop forever else stop}$ を構築します。
  • $G(G)$ を実行すると、自己言及により矛盾が生じます（$H$ が予測した挙動と実際の挙動が逆になります）。

ビジー・ビーバー定理（Busy Beaver Theorem）と動的視点

• 関数 $f(n) = \text{制御状態数が } n \text{ の停止する TM が取る最大ステップ数}$ を定義します。
  • この関数 $f$ は計算不可能です。
  • $f(n)$ よりも大きい任意の関数は、すべて計算不可能です。
• 意味： プログラムサイズに対する「最悪のケース（停止時間）」を知ることはできません。

静的視点とゲーデルの第二不完全性定理の応用

• 関数 $g(n) = \text{停止する TM の最小証明の最大サイズ}$ も計算不可能です。
• 応用例（Adam Yedidiya と Scott Aaronson の研究）：
  • ZFC 集合論内では、4K のコード量で収まるプログラムが存在し、その振る舞い（停止するか否か）を証明することが「独立」（ZFC では証明も反証もできない）です。
  • これは数学的に決定不可能な小さなプログラムが実際に存在することを意味します。

結論：コンピューターサイエンスは数学ではない

• チャーチ＝ターリングの仮説： すべての計算可能プロセスはチューリング機械でシミュレート可能です。しかし、これは物理的な制約を無視した抽象です。
• 「人間」による計算： アルゴリズムは物理的プロセスとして実行される必要があります。無限を対象とする純粋な数学とは異なり、実用的な検証には時間とリソースの限界があります。

3. 第 2 章：計算量 —— 困難さの定量化

停止問題の有無だけでなく、「どれくらい時間がかかるか」という複雑性が重要です。

有界停止と対角化

• 有界停止： 「$n$ ステップ以内にプログラムが停止するか？」を判断する問題です。
• 結果： $O(n)$ の時間で解決でき、さらに速くすることは不可能です（$\Omega(n)$）。
  • 理由： プログラムが何を行うかを知るには、実際に実行するか、少なくとも同等の時間を費やす必要があります。「プログラムについてより早く答えることは実行するよりもできない」ためです。

検証はコンピューターサイエンスで最も難しい問題

• 一般化された検証問題（V）： 任意の決定問題 $P$ をシミュレートし、その真偽を返す問題です。
• 時間階層定理より： すべての計算可能な関数に対して、より複雑な問題が存在します。
  • したがって、検証問題 $V$ は、既知の上界を持つすべての決定問題よりも困難です。
  • 結論：検証は「有界停止」に還元され、極めて難しい問題です。

モジュール化の限界（正しさは分解しない）

• 着想： プログラムを小規模なコンポーネントに分割し、個別に検証すれば全体が簡単になるか？
• 結果： 「正しさは分解しない」。
  • コンポーネント同士の相互作用（合成）を検証する際、複雑性は加算されるのではなく、乗数的または非決定可能な性質を帯びます。
  • Goldbach 予想に基づくプログラム例では、単独で正しい部品を組み合わせたものが、300 年間解明されなかった問題に突入します。

言語抽象化の効果

• 記号モデルチェッカー（Symbolic Model Checking）： プログラムの簡潔な表現を利用しても、最悪ケースでは $PSPACE$ 完全の問題になり得ます。
  • 簡潔なプログラムを状態遷移図に展開すると、その爆発は構文から独立したものです。
• 抽象化の影響： 変数や並行性による抽象化は、検証複雑性を指数関数的に増大させる可能性があります（状態空間の直積）。

4. 第 3 章：検証手法とその限界

モデルチェッカー（Model Checker）

• 仕組み： 有限状態機械（FSM）の状態空間を完全探索します。
• 問題： **「状態爆発（State Explosion）」**という現象に直面します。
  • 小さなプログラムの違いが巨大な状態空間を生みます（例：自動車の CAN バスプロトコルや、ハノイの塔の状態空間）。
  • 複雑性は $O(|S|)$（状態数）で決まり、実用的な規模では非現実的です。

推論的証明（Inferential Proofs）

• 仕組み： M ⊢ φ のように形式的に証明を行います。
• 問題：
  • 証明を見つけるのは人間にとって非常に困難です。
  • プログラムのサイズに対して多項式長の証明が存在するかは未解決（$NP = coNP$ に依存）です。
  • 高信頼性ソフトウェアには「複雑性の価格」を払う必要があります。

抽象解釈と型理論（Abstract Interpretation & Types）

• 仕組み： プログラムを簡素化したモデルに変換し、近似して検証します。
• 限界：
  • 依存型がない場合： 検証可能な性質は FSM の性質に限定され、Turing 完全なプログラムの深層には届きません（Rice の定理の回避）。
  • 依存型がある場合： 具体的なタイプの数が無限になり、推論コストは依然として非決定可能（$\Omega(\infty)$）です。

結論：銀の弾丸はない

Fred Brooks（「No Silver Bullet」著者）と Władysław M. Turski は、以下の点を指摘しました。

• 数学的限界： Gödel の結果により、いくつかのことは計算不可能です。ソフトウェア開発には万能薬はありません。
• 楽観主義への警告： 難しい問題を「簡単な解決策」があるはずだと信じるのは危険です。

私たちはどうすべきか？

1. 経験主義への回帰：
   • 検証可能でないすべてのプログラムを網羅的検証することは不可能です。
   • 人間が書いたプログラムという事実を利用して、バグの原因（心理学的効果、エラーハンドリングの欠落など）を統計的に分析し、「安価な検証」可能なカテゴリーを見つけるべきです。
2. 複雑性の受容：
   • 「複雑性は不可欠であり、制御不可能」と受け入れる必要があります。
   • 一つのアプローチで全てを解決することはできません（ad hoc テクニックの組み合わせが必要）。

「難しい問題には簡単な解決策はありません。」 これが計算量理論が私たちに伝えるメッセージです。