正しさは証明した瞬間には決まらない AIが呼び戻した1979年の反論

3行まとめ

• AIがコードを書く時代に、形式検証形式検証プログラムが仕様を満たすことを、数学的な証明で確かめる手法です。すべての入力が対象になります。への関心が再燃しています
• 1979年の論文は「証明は社会的なプロセスだ」と反論していました
• 数学でも証明は出発点で、他者が咀嚼して初めて信じられます

何が起きたか

形式検証が久しぶりに脚光を浴びています。プログラムが正しいことを数学的に証明する手法で、長らく一部の分野だけのものと見られてきました。それが直近2年で、Google トレンドの検索数が大きく跳ねています。

証明を書くための言語 LeanLean証明を機械が検査できる形で書くための言語です。形式検証の再流行のなかで学ぶ人が増えています。 を学ぶ人が増え、新しい仕様仕様そのプログラムが何を満たすべきかを、曖昧さなく書き下したものです。記述言語も次々に生まれています。Signal Shot のように、大きなアプリを丸ごと検証しようという試みもあります。

Antithesis の Will Wilson は Bug Bash 2026 の冒頭講演で勝利を宣言しました。講演のタイトルは「We won, what now?」です。

火をつけたのはAIコーディングです。AIが書いたコードには人間の理解が届かない穴が残り、別の手段で正しさを担保する必要が生まれました。この空気のなかで、1979年の反論論文が読み直されています。

なぜ難しい・何がすごいか

「数学で証明する」が何をすることなのか、そこが分かれ目です。まず、そのプログラムが満たすべき条件を、曖昧さのない形で書き下します。これを仕様と呼びます。

次に、実装が仕様を必ず満たすことを、論理の積み重ねで示します。テストとの違いは範囲です。テストは入力を何百通り試して、落ちないことを確かめます。

証明はすべての入力について成り立つことを示します。だから強い。

1979年の論文は、その手前に穴があると指摘しました。頭のなかにある曖昧な要求を仕様に翻訳する作業そのものは、数学の外にある人間の解釈です。翻訳の途中で取りこぼしたものは、いくら証明を積んでも戻ってきません。

たとえ話

数学の証明も、書き上げた瞬間には終わっていません。論文が出たあと、他の数学者がそれを読み、自分の言葉で追い直し、別の分野の結果とつなげていきます。その過程を通り抜けて、はじめて「あれは正しい」と共有されます。

1979年の論文が言うのは、証明は到達点ではなく伝達の手段だということです。

用語ミニ辞典

• 形式検証: プログラムが仕様を満たすことを、数学的な証明で確かめる手法です。すべての入力が対象になります。
• 仕様: そのプログラムが何を満たすべきかを、曖昧さなく書き下したものです。
• Lean: 証明を機械が検査できる形で書くための言語です。形式検証の再流行のなかで学ぶ人が増えています。
• Quint: 仕様を対話的に動かし、細かい条件が意図どおりかを確かめられる仕様記述言語です。
• モデル検査: 対象を有限の状態モデルに落とし、機械が全状態を網羅的に調べる検証手法です。

技術者向けの深掘り

1979年の反論は6つあり、効き目が落ちたものと残っているものが分かれます。

完全な自動検証は実現しない、という反論は弱まりました。Igor Konnov は Lean で Ben-Or プロトコルの安全性を証明した経験を公開しています。LLM を積んだ道具が、人手に頼っていた部分を急速に埋めつつあります。

残っているのは仕様を書く人間の側です。コーディングエージェントにコードと証明を作らせることはできます。しかし何を正しさとするかを決める役は、人間から動きません。

完全な検証だけが信頼性の道でもありません。監視や多層防御、うまくいった設計の使い回しといった工学的な手立ても、同じ重みを持ちます。

これは自分に関係ある？

• コードを書かない人: AIが書いたソフトウェアをどう信用するかという問題が、金融や重要インフラの側から降りてきます。正しさの担保そのものが製品の価値になる局面が増えます。
• AI専門ではないエンジニア: 完全な形式検証に踏み込まなくても、仕様を精密に書く訓練は効きます。エージェントに何を作らせたいかを言葉にする作業と地続きだからです。
• 形式手法に触れてきた人: 要求から仕様への翻訳という穴だけは、半世紀近く経っても埋まっていません。