Leanの証明自動化が到来した。難しい部分はただ移っただけだ

Leanの証明自動化は7月26日、Adam Langleyが大規模言語モデルを使って動作するZstandardデコーダーを検証したと説明したことで、重要な一線を越えた。その成果は、ベンチマーク用の定理でも、洗練されたベンダーのデモでもない。難しい不変条件、生成された証明、そして誤った回答を拒否できるコンパイラを備えた、普通のソフトウェアプロジェクトだった。

この組み合わせは、AIの信頼性をめぐる従来の議論を変える。言語モデルは依然として幻覚を起こし、要件を誤解し、無効な構文を生成しうる。それでもLeanは小さな検証カーネルを通じて得られた証明をチェックするため、信頼はモデルの文章を信用することに依存しない。

したがって本当の競争は、AI生成コードと人間が書いたコードの間にあるのではない。検証されない生成と、機械検証された生成との間にある。知識労働者にとって、この違いは、AIが成果物を作り、決定論的なシステムが重要な主張を検証する、より広いモデルを示唆している。

Langleyの実験は、形式検証が安価で簡単になり、あらゆる本番システムに適用できるようになったことを示すものではない。彼はデコーダーを公開しておらず、性能結果も芳しくなかった。しかしこの実験は、検証の経済性が変わりつつあることを示す具体的な兆候となっている。

Zstandardデコーダーが証明自動化の試験になった

Langleyの実験が重要なのは、LLMが孤立した数学問題だけでなく、認識可能なソフトウェア実装の内部で証明義務を処理したためだ。

暗号技術とインターネットプロトコルの仕事で知られる著名なセキュリティエンジニア、Langleyは、LeanでZstandardの展開器を構築した。Leanは、関数型プログラミング言語であると同時に、依存型理論に基づく対話型定理証明支援系でもある。

依存型により、プログラムの型は特定の値に関する事実を表現できる。たとえば関数は、正確な長さを型に記録した配列を返せる。別の関数では、Leanがアクセスを許可する前に、インデックスが配列の範囲内にあるという証明を要求できる。

こうした保証は、従来のソフトウェアではコメント、テスト、あるいは開発者の記憶に委ねられがちな前提を符号化できる。Lean referenceは、他のツールが生成した後に証明項を検査する小さなカーネルについて説明している。生成と検査のこの分離が、本稿の中心にある。

Langleyはテストケースとして、一般にzstdと呼ばれるZstandardを選んだ。Zstdはロスレス圧縮形式であり、検証に意味を持たせるだけの内部的な複雑さがある。LZ77スタイルのマッチングに加え、ハフマン符号化とFinite State Entropy、すなわちFSEを使用する。

公開されている形式の圧縮仕様では、フレーム、ブロック、エントロピーテーブル、シーケンスコード、復号動作が定義されている。そのFSEの節では、可能な入力全体にわたり複数の関係を保たなければならない状態テーブルの構築が説明されている。

通常の実装では、選択したテーブルを既知の出力と照合できる。LangleyのLean版では、テーブル構築関数について普遍的な性質も記述できた。それらの性質には、テーブルに必要なサイズ、シンボル数、テーブルエントリーからの遷移の妥当性が含まれていた。

ここでLLMの貢献が重要になった。Langleyの証明自動化に関する説明によると、複数のモデルが関連する証明を約20分で生成したという。彼によれば、この作業で消費したのは標準的な月額サブスクリプションの利用枠のごく一部にすぎない。

モデルは開発中に未完成の証明を受け入れるLeanの通常の逃げ道、sorryを残さなかった。Langleyは、証明が型検査を通過し、そのような穴がないことを確認したとしている。

これはデコーダーに関するあらゆる主張を独立に検証するものではない。Langleyはソースコードを公開していないため、外部のレビューアはプロジェクトを再現したり、仕様全体を検査したりできない。彼の報告は、査読済み評価ではなく一人称による実験の記録である。

それでも、主張された検証ステップは、通常のチャットボットの回答とは異なる位置づけにある。Leanのカーネルが正しく記述された定理の証明を受理するなら、モデルの内部的な推論を信頼する必要はない。チェッカーが得られた形式的オブジェクトを評価する。

これは実用的な形での証明無関係性だ。多くの命題において、ソフトウェアが最終的に必要とするのは、証明がどのように発見されたかについての洗練された説明ではなく、有効な証明である。不格好な機械生成の証明でも、カーネルが受理すれば定理を保証できる。

このデコーダーは、プログラムを証明することと、優れた製品を作ることの境界も明らかにした。Langleyは、自身の実装がコマンドライン版zstdより約10倍遅かったと報告した。検証は、本番性能、保守性、完全な形式カバレッジを自動的にもたらすものではなかった。

価値ある成果は、より限定的である。開発者が汎用LLMを使い、単純ではないプログラムの中で難しい証明義務を果たした。この実験は、かつて支配的なコストだった証明作業が、ますます機械生成の仕事になりうることを示唆している。

Leanの証明自動化がコスト方程式を変える理由

Leanの証明自動化は形式検証のコストをなくすものではないが、そのコストを通常のソフトウェアチームにとって受け入れがたいものにしていた労働の区分を攻めている。

形式検証は長年にわたり、テストでは得られないものを提供してきた。テストは選択された実行を調べる一方、形式的な証明は、そのモデルが対象とするすべてのケースにわたって、記述された性質を確立できる。

この違いは、高保証システムで目覚ましい成果を生んできた。seL4マイクロカーネルには、対応する構成において仕様と検証済み実装を結びつける機械検査済みの証明がある。そのプロジェクト文書では、その証明が2009年に完成して以来、検証済みコードに機能的正しさの欠陥はないと報告されている。

同じseL4 evidenceは、形式手法が専門領域にとどまってきた理由も示している。その検証には、広範な仕様、証明スクリプト、補助ツール、専門家の労働が必要だった。Langleyは、証明作業が設計と実装の作業量のおよそ10倍を要したという回顧的な見積もりを引用している。

彼はまた、証明コードがC実装の20倍以上に達したことにも触れている。正確な比率はプロジェクトや検証目標により異なる。より広い論点は明白だ。より強い保証は歴史的に、大規模な第二の技術作業群を要求してきた。

この作業は、従来型のプログラミングとは異なる感覚を伴う。エンジニアは非形式的な要件を精密な記述へ翻訳し、難しい目標を扱いやすい補題へ分解し、証明システムを不足しているステップへと導かなければならない。小さなコード変更であっても、大規模な証明の修復を強いられることがある。

自動ソルバーは、この負担の一部を軽減してきた。たとえばF*のようなシステムは、適切な証明義務を、対応する論理理論の範囲で証明を探索する充足可能性モジュロ理論ソルバーへ送ることができる。しかし、複雑な目標に対するソルバーの挙動は予測が難しくなりうる。

経験豊富な利用者は、自動化が成功するよう定義をどう記述すべきかを学ぶことが多い。この専門性は依然として価値があるが、作業はソルバーへの適応に移る。小さなモデリング上の選択が、迅速な結果を大きな時間を消費する探索へ変えてしまうこともある。

LLMは異なる形の自動化を提供する。ローカルの定義を読み、コンパイラエラーを解釈し、補題を提案し、コードを書き換え、別の証明戦略を試せる。すべての証明義務が固定された決定手続きに収まる必要はない。

研究はすでに、生成と形式的チェッカーの組み合わせが重要であることを示している。APOLLO paperで説明されたあるコンパイラ誘導システムは、Leanのフィードバックを用いて生成された証明を修復し、失敗した部分問題を切り分ける。報告された結果は、反復的な検証が誘導のないサンプリングを上回りうることを示している。

Langleyのプロジェクトは、このパターンを日常的なソフトウェアエンジニアリングに近づけている。モデルは単にベンチマーク用に選ばれた定理を解くのではない。バイト列の解析、復号テーブルの構築、配列境界の強制によって生じる証明義務に直面する。

この違いは採用にとって重要である。ほとんどの組織は、競技問題を証明する数学者を雇ってはいない。一方で、パーサー、認可ルール、財務計算、同期ロジック、データ変換を保守するエンジニアは雇っている。

これらのシステムには、チームがすでに不変条件として扱っている無数の記述がある。リクエストは認証済みアカウントに属する。請求書の明細は合計額と一致する。パーサーはバッファーの範囲外を決して読み取らない。ワークフローは、自身の制限された操作を承認できない。

現在、チームはこれらの記述を、型、テスト、レビュー、監視、運用上の制御を組み合わせて守っている。それぞれの方法は重要な失敗を捉えるが、いずれにも隙が残る。要件が変われば、前提もずれていく。

Leanの証明自動化は、選択された前提を実行可能かつ検査可能にする道筋を提供する。LLMが翻訳作業と証明作業の一部を担う。その後Leanが、形式仕様を満たさない成果物を遮断する。

この配置は、AIの信頼度の役割も変える。従来のコーディング支援ツールは、限られたコンテキストウィンドウを確認した後に、パーサーは安全だと述べるかもしれない。証明を生成する支援ツールは、明示的な主張に対してLeanが受理する成果物を提供しなければならない。

受理ゲートが決定論的であるため、モデルは確率的なままでよい。このアーキテクチャは、単一モデルのベンチマークスコアよりも重要である。より優れたモデルは速度とカバレッジを改善し、チェッカーは信頼の境界を維持する。

組織にとって、経済的な問いはより具体的になる。すべてのエンジニアが証明の専門家になるべきかを問う必要はなくなる。代わりに、どの高コストな失敗が形式的な記述とAI支援の証明を正当化するかを問える。

このより狭い採用経路は、静的型付け、自動テスト、継続的インテグレーションの普及に似ている。これらの実践は欠陥をなくしたわけではない。例外的な監査時ではなく、通常の開発中に実行できるほど、特定のチェックを安価にした。

新たな対立相手は検証されない生成だ

中心的な対立は、人間とモデルのどちらがより優れたコードを書くかではない。生成された作業が信頼できる受理テストに直面するかどうかである。

ほとんどの生成AIツールは、検証が弱い領域で動作する。モデルはレポートを下書きし、会議を要約し、予測を提案し、方針を編集する。その出力は、正しいかどうかが判明するずっと前から、もっともらしく見えることが多い。

人によるレビューは依然として標準的な防御策である。しかしレビューアも、自動化を促したのと同じ時間的制約に直面している。流暢な下書きは、欠落した情報源、逆転した条件、根拠のない結論を隠しうる。

ソフトウェアは、ほとんどの知識労働よりも多くの自動フィードバックを提供する。コンパイラは構文エラーと型エラーを拒否する。テストスイートは既知のケースを実行する。リンターは選択されたパターンを特定する。本番監視は、以前のゲートをすり抜けた失敗を明らかにする。

通常、これらの仕組みのどれも広範な意味論的主張を証明しない。テストの通過は、すべての有効な圧縮ストリームが配列境界内に収まることを確立できない。関連する関係が型システムに現れない限り、型チェッカーもその性質を強制できない。

Leanは契約を変える。開発者は、プログラムの型の中、あるいは定理として主張を表現できる。カーネルは次に、与えられた証明が、受け入れられた前提からその正確な主張を確立しているかどうかを検査する。

LLMは権威ではなく、候補となる証明の生成者になる。最終的な保証を損なうことなく、何度失敗してもよい。失敗した候補は、信頼できる成果物に組み込まれる前に却下される。

このパターンは、定理証明をはるかに超えてナレッジワーカーの関心を引くはずだ。多くの業務成果物にはすでに、構造化された証拠に照らして検証できる主張が含まれている。課題は、それらの主張と、依然として文脈に左右される判断とを切り分けることにある。

週次アップデートを作成するプロダクトマネージャーを考えてみよう。AIアシスタントは、検索可能なナレッジベースを通じて、プロジェクトノート、意思決定、顧客フィードバック、デリバリー指標を収集できる。人がその週を振り返って再構成するよりも速く、ストーリーを下書きできる。

しかし、組織には依然としてチェックポイントが必要だ。引用するすべての顧客発言は、録音またはノートに対応付けられるべきである。出荷済みのすべての機能は、承認済みのリリース記録に対応付けられるべきだ。すべての指標には、定義と報告期間を付与する必要がある。

これらは、現状では定理証明のタスクではない。ただし、同じアーキテクチャを共有している。生成は成果物を提案し、別のシステムが明示的なルールと証拠に照らして主張を検証する。

財務アナリストは、生成されたメモ内のすべての数値が提出書類または承認済みデータセットにまで遡れることを求めるかもしれない。研究者は、すべての引用がそれを含む文を裏付けることを求めるかもしれない。コンプライアンスチームは、ポリシー条件を機械検証可能なワークフローに組み込むことができる。

形式言語は、この種の検証の上限を引き上げる。単純な検証スクリプトではきれいに表現できない関係性も表現できる。LLMはその後、ユーザーによる仕様記述、形式間の橋渡し、必要な証拠の構築を支援する。

これは、信頼できるAIをより有用に定義するものだ。信頼は、モデルに慎重であるよう求めることから生まれるのではない。裏付けのない成果物が重要な境界を越えられないプロセスを設計することから生まれる。

このアプローチは、人間の判断がどこで不可欠であり続けるかも明確にする。Leanが検証するのは、誰かが書いた定理である。その定理がユーザーの実際の要件や組織のリスク全体を捉えているかどうかまでは判断しない。

完全に証明された仕様であっても、誤った振る舞いを指定している可能性がある。配列境界に関する定理は、デコーダーが本番サービスに必要なすべての機能を扱えることを示すものではない。セキュリティ証明は、現実的な攻撃者の能力を見落とすことがある。

したがって、AI支援による検証は、人間の労力を仕様へと移す。どの特性が重要か、どの前提を受け入れられるか、証明がどのシステム境界をカバーするかを、人が決めなければならない。

この変化は、スプレッドシートが会計にもたらした効果に似ている。自動化は計算作業を減らすが、正しいモデルと入力を選ぶ重要性を高める。完璧な計算でも、誤ったビジネス上の問いに答えていることはあり得る。

最も強いチームは、生成された証明を飾りとして扱わない。現在アーキテクチャやセキュリティ境界に払われているのと同じ注意を、定理文、前提、インターフェースのレビューに向けるだろう。

Zstandardの実験が証明していないこと

検証済みの証明は有効であっても、周辺ソフトウェアが遅い、不完全、仕様不足、あるいは本番運用に不向きである可能性は残る。

最も直接的な制約は再現性だ。Langleyは、この実装を参照用デコーダーではなく学習プロジェクトと捉えていたため、公開しなかった。この選択により、コード、証明構造、モデルワークフローを独立して検証することが妨げられる。

したがって読者は、報告された20分間の証明生成結果を経験報告として扱うべきである。これは、1人の熟練エンジニアが1つのプロジェクトでこのワークフローを機能させた証拠ではある。一般的な性能測定ではない。

モデルは証明を探索する中で、実装コードの一部も変更した。Langleyは、局所的に命令型計算を表現できるLeanの仕組みであるId.runを使用していた。彼によれば、このスタイルは証明機構によるコード分析を難しくしたという。

この細部は、順調な成功談よりも多くを示している。AIによる証明自動化は、任意の実装をそのまま認証したのではない。プログラムを形式的に推論しやすくする変更を促した。

こうした変更は構造を改善し得るが、エンジニアリング上の優先順位を歪めることもある。開発者は、現在の証明ツールが扱いにくいという理由で効率的な表現を避けるかもしれない。より速い検証を得るために、より遅いコードを受け入れる可能性もある。

Langleyのデコーダーは、確立されたコマンドライン実装よりおよそ10倍遅かったと報じられている。この差は証明を無効にするものではない。正確性、網羅性、性能が依然として別個の次元であることを示している。

証明エンジニアリングも消え去ったわけではない。大規模プロジェクトでは、コードが変化しても証明が維持できるよう、補題と抽象化を組織する。LLMが低コストで証明を再生成できるなら、一部の保守戦略の重要性は下がる。他方で、証明探索自体が高コストになり得るため、必要であり続ける戦略もある。

proof-state snapshottingに関する最近の研究は、このインフラ上の問題を示している。著者らは、状態の再構築を繰り返す処理が、自動化されたLean探索の大部分を占める可能性があると報告している。提案された再利用メカニズムは、選定されたベンチマーク全体で大幅な高速化を実現した。

これは、証明自動化がモデルの知能だけに依存するわけではないことを思い出させる。高速なコンパイラフィードバック、依存関係管理、関連する補題の検索、制御された探索、再現可能な環境が必要になる。

規模は別の不確実性を生む。圧縮デコーダーには制約された仕様と認識しやすいアルゴリズムがある。エンタープライズシステムは、データベース、ネットワーク、ユーザーインターフェース、外部サービス、変更可能な権限、不完全な業務ルールを組み合わせる。

こうした境界を形式化するコストは、局所的な関数を証明するコストより高くなる場合がある。認可ルールに関する定理が役立つのは、IDデータ、サービスの振る舞い、デプロイ構成がモデルの前提と一致する場合に限られる。

非常に強力な型は、プログラム全体に変更を広げる可能性もある。あるデータ構造に新たな不変条件が加わると、それを構築または変換するすべての関数が、より強い要件を満たさなければならない。この波及は価値がある一方で、移行コストを増やすことがある。

LLMは影響を受けた証明を修復できるが、コードからプロダクトの意図を常に推論できるわけではない。再生成された証明は、実際には新しいものが必要な場面で、昨日の定理文を維持してしまう可能性がある。自動化は、古くなった正しさを維持しやすくする。

ツールチェーンにはセキュリティ上の懸念もある。Leanカーネルは、証明を信頼するために正しく振る舞わなければならないソフトウェア、すなわち信頼できるコンピューティング基盤を縮小する。しかし、ビルドシステム、パーサー、コンパイラ、デプロイパイプラインは依然としてカーネルを取り囲んでいる。

証明は、明示された前提や公理にも依存する。チームには、未完成のプレースホルダー、想定外の公理、誤った依存関係バージョンに対して生成された証明を拒否するポリシーが必要だ。エディタ上の緑色のインジケーターだけでは、十分なガバナンスにならない。

技術に詳しくない意思決定者にとってのリスクは、「証明」という言葉を過大に解釈することだ。形式検証が確立するのは、定義された前提のもとでの定義された特性である。一般的な品質、倫理的な振る舞い、使いやすさ、法令遵守、事業価値を認証するものではない。

この精密さは強みとして扱うべきだ。チームは、何が正確に証明され、何が境界の外に残されたかを検査できる。代替案はしばしば、散在するテストと自信に満ちた文章で支えられた、広範な保証の主張である。

したがってLangleyの結果は、方向性を示すシグナルとして最も強い。LLMは、形式証明の構築をより省力化できる。残るボトルネックは、仕様、システム境界、性能、統合へと移る。

証明自動化が広がるかを示す3つのシグナル

次の段階は、再現可能なソフトウェア事例、証明を意識した開発ツール、そして検証済みシステムが実際の変更後も保守可能であることの証拠にかかっている。

最初のシグナルは、AI生成のLean証明を中心に構築された、完全で一般的なソフトウェアプロジェクトの公開である。ベンチマークは依然として有用だが、変化する要件、依存関係のアップグレード、性能チューニング、本番デバッグを捉えることはできない。

説得力のあるプロジェクトは、ソース、定理文、プロンプトまたはエージェントのワークフロー、モデルバージョン、証明確認コマンド、制約を公開すべきだ。独立したチームが、ホストされたモデルを信頼せずに、受け入れられた証明を再現できる必要がある。

パーサー、暗号コード、金融ロジック、プロトコル実装にまたがって複数のプロジェクトが登場すれば、Langleyの結論はより強まる。事例が小規模なまま、または未公開のままであれば、日常的な導入を支持する根拠は弱まる。

2つ目のシグナルは、主流の開発ワークフローへの統合だ。証明自動化は、研究環境というよりも、コードレビュー、継続的インテグレーション、エディタの型チェッカーのように感じられる必要がある。

重要な機能には、ローカルライブラリからの信頼性の高い検索、短いフィードバックループ、説明可能な失敗、未完了の前提を厳格に検出する仕組みが含まれる。チームには、コード変更と並べてレビューできる、バージョン管理された証明成果物も必要になる。

ツールは、証明本文だけでなく、証明対象となる定理文の変更も強調すべきだ。定理を密かに弱めるモデルは、困難な失敗を誤解を招く成功へと変えてしまう可能性がある。レビューインターフェースは、そのような変更を明白にしなければならない。

組織は、ベンダーが非形式的な要件をどのように形式的な定理文へ接続するかも注視すべきである。証明を生成することはワークフローの半分にすぎない。システムは、人間の意思決定から機械検証可能な特性までのトレーサビリティを維持しなければならない。

ここで、ナレッジマネジメントは運用インフラとなる。アシスタントが責任を持って形式化するには、要件、意思決定、例外、根拠となる証拠に、永続的な文脈が必要だ。パーソナルナレッジシステムはその文脈を支えられるが、形式的な受け入れには依然として専用の検証ツールが必要である。

3つ目のシグナルは、大きな変更後の保守コストだ。一度きりの証明はレビュー担当者を感心させるかもしれないが、次のリリースでは負担になり得る。より重要な指標は、振る舞いを変更した後、チームがどれだけ速く検証済みの状態を回復できるかである。

研究者とエンジニアリングチームは、変更を中心とした評価を公開すべきだ。データ構造を変更し、仕様を強化し、アルゴリズムを置き換え、依存関係をアップグレードする。そのうえで、人間の労力、モデルの試行回数、検証時間、性能低下を測定すべきである。

AIが、明確にレビューされた定理文を維持しながら証明を修復できるなら、形式手法は反復的なソフトウェア開発とより両立しやすくなる。変更のたびに制御不能な探索や広範な書き換えが発生するなら、導入は高保証が求められるニッチ領域に集中し続けるだろう。

ナレッジワーカーも、自身のAIシステムに同じパターンを見出すべきだ。持続的な優位性は、より多くの下書きを生み出すことからは得られない。文書、ポリシー、データ、チームが変化しても信頼性を維持する受け入れゲートを構築することから得られる。

Leanの証明自動化は、生成と検証が別々の役割を担うため、非常に明快な例を示している。LLMは創造的で、一貫性がなく、ときには誤ることもある。それでもカーネルは有効な形式成果物を要求する。

この設計は、AI生成の成果物をめぐるすべての問題を解決するものではない。しかし、より良い標準を確立する。モデルには提案させ、明示的なシステムには検証させ、人には仕様を担わせる。

次に問うべき実務的な論点は、すべての職場がLeanを導入すべきかどうかではありません。自信に満ちた一段落の説明や、簡単なテスト以上に強固な検証が必要な反復的な主張は、どれなのかということです。コストの高い前提を一つ特定し、その根拠と結び付けたうえで、行動に移す前にどのような決定論的なゲートで確認できるかを問いましょう。この演習によって、AIが安全に業務を加速できる領域と、依然として人間によるレビューが全面的な責任を担う領域が明らかになります。Leanによる証明自動化は到達点をより見えやすくしましたが、どの主張を証明する価値があるかは、組織がなお選ばなければなりません。