太陽に近づきすぎた仮説

1980年代初頭、NASAは今日も safety-critical engineering を悩ませる問いに直面していた:まだ発見されていないバグをどう許容するか?彼らの答えは N-version programming だった。同じ仕様書を3つの独立したチームに渡す。3つのプログラムを並列実行する。出力を投票で決める。1つのチームがバグを書いたとしても、残りの2つがそれを上回るはずだ。

これは数学的な常識のように聞こえる。しかし、それは間違っている。

1986年、John Knight と Nancy Leveson は、NASAの資金で実施された大規模実験の結果を発表した。2つの大学の大学院生27人が、同じ弾道ミサイル迎撃システムの仕様を独立して実装した。個々のプログラムは極めて信頼性が高かった。6つのバージョンは一度も失敗しなかった。23のバージョンは、100万個のランダム生成テストケースのうち99.9%以上を通過した。

しかし、複数のバージョンが同じ入力で失敗したとき、それらは統計的独立性が予測するよりもはるかに高い頻度で同時に失敗した。z-score は100.55だった。99% confidence interval で、独立性の null hypothesis は粉砕された。NASAは人間のミスがランダムだと賭けた。Knight と Leveson は、それがクラスター化する証拠を示した。

N-version programming が実際に約束するもの

N-version programming の背後にある論理は、ハードウェア冗長性から借りてきたものだ。ロケットに3つの同じジャイロスコープを取り付け、1つがずれたら残りの2つがそのずれを上回る。故障は独立している。なぜなら、ジャイロスコープは独立した製造バラツキ、温度勾配、振動モードの影響を受ける物理的な物体だからだ。

ソフトウェアは違う。3つのチームに同じ問題を解かせても、3つの独立したサイコロの目は出ない。同じ曖昧な仕様書を読み、同じ教科書から同じアルゴリズムを学び、同じ言語で同じ標準ライブラリを使ってコードを書く3人の人間が得られるだけだ。彼らの入力が相関するので、彼らのエラーも相関する。

N-version アーキテクチャは、実際にはこう見える:

from typing import Callable, List, TypeVar

T = TypeVar('T')

def n_version_vote(
    implementations: List[Callable[[float], T]],
    input_value: float
) -> T:
    """Run N versions and return the majority output."""
    results = [impl(input_value) for impl in implementations]
    
    # Simple majority vote
    from collections import Counter
    counts = Counter(str(r) for r in results)
    most_common = counts.most_common(1)[0][0]
    
    # Return the actual value that matched the winning string
    for r in results:
        if str(r) == most_common:
            return r
    
    raise RuntimeError("No consensus")

この voter は簡単な部分だ。難しいのは、その中に隠れている仮定だ:implementations[0]implementations[1]implementations[2] が、入力空間の相関しない部分集合で失敗するという仮定。Knight と Leveson は、その仮定こそが欠陥だと示した。

相関した失敗はどこから来るのか

Knight-Leveson 実験は、common-mode failure の2つの明確なメカニズムを明らかにした。どちらも「もっと頑張れ」とチームに求めることでは修正できない。

1つ目は specification ambiguity だ。ミサイル迎撃システムの仕様には、本当に難しいエッジケースが含まれていた。27人のプログラマーのうち8人が、3つのレーダーポイントが共線になるケースを誤って処理した。エラーの内容は異なっていた。1人は配列の添字で off-by-one を起こした。1人は数値安定性の悪いアルゴリズムを使った。1人は境界ケースを完全に忘れていた。しかし、失敗は同じ難しい入力に集中した。なぜなら、問題自体が難しかったのだ。プログラマーが不注意だったわけではない。

これが「difficulty factor」だ。入力が境界条件に位置し、トリッキーな浮動小数点演算を必要としたり、不十分に指定された状態遷移を含んだりすると、独立したチームでも同じ場所で苦労する傾向がある。彼らの解決策は異なる。しかし、失敗領域は重なる。

2つ目のメカニズムは shared mental models だ。同じカリキュラムで訓練されたプログラマーは、同じヒューリスティクスを適用する。同じソートアルゴリズムを、同じ defensive copy パターンを、同じ浮動小数点等値比較の epsilon を手に取る。その共有されたデフォルトが、当面の問題にとって間違っているとき、すべてのチームが同じ崖から転落する。

NASA自身の Software Safety Guidebook は、最終的にこれを明示的に認めた。「多くの専門家が N-version programming を非効率的、あるいは逆効果だとみなしている」と記している。実験機に関する NASA の1つの研究では、テスト中に発見されたすべてのソフトウェア問題が redundancy management system から来ていた。主飛行制御ソフトウェアは完璧だった。N-version 層だけが壊れていた。

誰も話さない複雑性の代償

たとえ N-version programming が宣伝通りに機能したとしても、重い代償を取る。3つの完全な実装の費用を支払う。voter 自体に含まれるロジックの費用を支払う。3つのプロセスを実行し、その出力を調整する運用オーバーヘッドの費用を支払う。

その voter は自明なコード片ではない。同票、タイムアウト、異なる出力フォーマット、多数派が間違っているケースを処理しなければならない。Brunelle と Eckhardt は1985年に SIFT operating system でこれを実証した。2つの新しい N-version が、元の正しい実装を outvote して、間違った答えを生み出した。冗長性システムが、防止すべきエラーを生み出したのだ。

複雑性は、噛みつくまで測定が難しい形で増大する。これで3つの deployable をバージョン管理し、3つのテスト行列を維持し、要件が避けられず変わったときに3つのチームが仕様変更を異なるように解釈するようになった。人間のミスの表面積は、信頼性の向上よりも速く増大する。

代わりに実際に機能するもの

NASAは fault tolerance を放棄しなかった。彼らが放棄したのは、多様性が独立性から生まれるという特定の仮定だ。現代の high-assurance システムは、Knight と Leveson が特定した実際の failure mode に対処する技術の組み合わせを使う。

クリティカルパスへの formal methods。 3つのチームが仕様を正しく解釈することを望むのではなく、仕様を machine-checkable な形で書く。TLA+、Coq、SPIN といったツールは、誰も実装コードを1行も書く前に、設計がその不変条件を満たすことを検証する。NASA自身の Remote Agent Experiment は、SPIN を使って、広範なテストをすり抜けた並行性バグを発見した。

異なる技術スタックを通じた多様性。 冗長性が必要なら、深くする。Airbus A330 の飛行制御システムは、プライマリチャンネルとバックアップチャンネルに、異なるハードウェアアーキテクチャ、異なるプログラミング言語、独立したコンパイラを使う。目標は、独立したチームであることだけでなく、スタックのあらゆる層で independent failure modes を持つことだ。

重複より単純化。 NASA Software Safety Guidebook は、最終的に N-version programming を「小さく単純な関数」に対してのみ推奨する。教訓は派手ではないが効果的だ:最も信頼性の高いシステムは、直接推論できるほど単純なものだ。冗長性管理コードの1行ごとが、失敗しうる1行だ。

以下は、単純化され、仕様主導のアプローチが実際にどう見えるかだ。3つの不透明な実装が出力を投票するのではなく、クリティカルな invariant を明示的にエンコードし、実行時にチェックする:

from dataclasses import dataclass
from typing import Optional

@dataclass(frozen=True)
class LaunchCommand:
    thrust_level: float  # 0.0 to 1.0
    abort_flag: bool
    
    def is_valid(self) -> bool:
        """Runtime invariant check derived from the formal spec."""
        if not (0.0 <= self.thrust_level <= 1.0):
            return False
        if self.abort_flag and self.thrust_level > 0.0:
            return False
        return True

def execute_command(cmd: LaunchCommand) -> Optional[str]:
    if not cmd.is_valid():
        raise ValueError("Invariant violation: command violates safety spec")
    
    # Execute only after the single, explicit check passes.
    return f"Executing thrust={cmd.thrust_level}, abort={cmd.abort_flag}"

これは N-version programming ではない。1つの実装に、1つの明示的でテスト可能な safety boundary がある。ここに労力を注ぐのだ。3チーム中2チームが正解したことを願うのではなく。

現代に響く警鐘

Knight と Leveson の1986年の論文は、年々重要性を増す警告を含んでいる。相関した失敗には、相関したチームは必要ない。相関した入力と相関した難しさがあれば十分だ。AI支援コーディングツールが普及するにつれ、私たちは地球規模で新しい N-version 実験を行っている。重複したコーパスで訓練され、類似したパターンでプロンプトされたモデルは、共有した failure mode を持つコードを生成する。

LLM コード生成に関する最近の研究では、AI生成コンポーネントの co-error rate が15%から30%の間にあることを示唆している。beta factor、つまり共通原因に起因する失敗の割合は、Knight と Leveson が測定した人間プログラマーの値をすでに超えている可能性がある。私たちは、より多くの参加者と同じ欠陥のある仮定を持って、同じ実験を繰り返している。

NASAは高い代償を払ってこの教訓を学んだ。3つの実装は必要ない。述べられ、チェックでき、信頼できる invariant を持つ1つの実装が必要だ。他のすべては、楽観主義を工学に着せ替えたものに過ぎない。

よくある質問

N-version programming とは何ですか?

N-version programming は、複数の独立したチームが同じ仕様を実装するソフトウェア fault tolerance 技術だ。プログラムは並列実行され、voter が多数派の出力を選択する。独立したチームは独立したミスをすると仮定している。

NASAは実際に N-version programming を使いましたか?

はい。NASAはマルチバージョンソフトウェアの初期研究に資金を提供し、ある時点では一部の政策文書が、fault-tolerant システムに対して事実上 N-version programming を義務付けていた。スペースシャトルのエンジン起動シーケンスでも使われたが、NASAは後に実証研究でその限界が明らかになったため、小さく単純な関数への使用に制限した。

Knight-Leveson 実験とは何でしたか?

1986年、John Knight と Nancy Leveson は、27人のプログラマーに弾道ミサイル迎撃システムの仕様を独立して実装させた。100万回以上のテストで、プログラムは統計的独立性が予測するよりも有意に多い coincident failure を示し、N-version programming の根底にある仮定を否定した。

N-version programming は使う価値があるのでしょうか?

限定的なケースではある。NASAの現在のガイダンスでは、true diversity を強制できる小さく明確に定義された関数に適している可能性があると示唆している。一般的なアプリケーション開発では、複雑性のコストと相関した失敗のリスクがメリットを上回る。Formal methods、runtime invariant checking、単純化が、通常はより良い投資だ。