LeanとLLMによる証明の自動化
LeanとLLMによる証明の自動化
LLMsは形式検証を実用的にする
依存型言語の導入における歴史的な障壁は、「証明の労力」—プログラムが指定された不変条件を満たすことを証明するために必要な莫大な手作業の量—でした。seL4マイクロカーネルプロジェクトはこのオーバーヘッドのベンチマークとして機能し、エンジニアはシステムの設計と実装にかかる時間の約10倍を証明に費やし、その結果、Cコードの20倍の証明コード行数が生じました。
大規模言語モデル（LLMs）は、これらの証明の生成を自動化することでこの状況を変えています。Leanなどの依存型システムは、証明が正しいかどうかを機械的に検証できるため、LLMの「幻覚」のリスクは排除されます：LLMが間違った証明を生成しても、型チェッカーは単にそれを拒否します。この変化により、ソフトウェアエンジニアリングの負担は、実装と証明の作成から正確な形式仕様の作成へと移ります。
ケーススタディ：Leanにおける検証済みZstandardデコンプレッサー
LeanとLLMの自動化の交差点を探るため、Zstandard（zstd）デコンプレッサーが実装されました。Zstandardは、LZ77と高度なエントロピーエンコーダであるFinite State Entropy（FSE）の組み合わせを利用する高性能な圧縮ユーティリティです。
FSEの課題
FSEは、シンボルごとに分数ビットを許容する状態マシンベースのエントロピーエンコーダで、複数の状態にシンボルを分布させることで実現します。これにより、ビット単位の増加に限定されるハフマン符号化よりも高い圧縮率を達成できます。ただし、FSEではブロックの終端からビットを後ろ向きに読み取る必要があり、実装の複雑さが大幅に増加します。
不変条件の形式化
標準的な言語では、最適化されたデコードループに必要な仮定は通常、コメントまたはランタイムチェックに追いやられます。Leanでは、これらは形式的な定理としてエンコードできます。FSEテーブルの構築において、以下の普遍的な性質はLLMの支援を受けて形式的に証明されました：
- 正しいテーブルサイズ: テーブルは指定された精度定数と一致します。
- シンボル分布: シンボルに割り当てられた状態の数は、その確率を正しく反映します。
- 状態の妥当性: 任意の状態に対して、ベースライン値と読み取ったビットを加えることで常に有効な状態番号になります。
- 到達可能性: 確率がゼロでないすべてのシンボルに対して、任意の目標状態に到達できる状態はちょうど1つあります。
これらの証明は、従来なら手作業で数時間または数日かかるものですが、LLMによって約20分で生成されました。
システムプログラミングにおけるLeanの技術的利点
Leanは、従来の定理証明器よりもプログラミングに適したいくつかの機能を提供します：
- 厳密な評価: Haskellの遅延評価とは異なり、Leanは厳密評価であり、パフォーマンスとリソース使用量の理由付けが容易になります。
- 命令型の糖衣構文: Leanのモナディックな
do表記は、forループ、return文、break文をサポートし、命令型のコーディングスタイルを可能にします。 - 参照カウント最適化: Leanは、オブジェクトの参照カウントが1の場合、インプレースでの変異を行うことができ、これにより命令型言語と同様に効率的な配列更新が可能になります。
検証済みソフトウェアの将来の展望
仕様エンジニアリングへのシフト
業界の議論では、プログラマーの役割が「仕様エンジニアリング」にシフトしていると示唆されています。実装がLLMによって生成された成果物であり、定理証明器によって検証される場合、ソフトウェアにおける人間向けの部分は仕様そのものだけになります。これにより、仕様はモジュール化され、合成可能であり、人間が検証できるほど短い必要があります。
スケーリングの問題
一部の批評家は、依存型は一般的なメンテナンスにはスケールしないと主張しています。プログラムに新しい不変条件を追加すると、計算と証明が intertwined であるため、すべての依存型を洗練し、コードベース全体の証明を適応させる必要がしばしば生じます。提案されている代替策は、依存型を主にモジュール境界で使用して不透明な型を公開し、内部の懸念は別に扱うことです。
検証済みアセンブリとパフォーマンス
AWSのLNSym（AArch64向けのセマンティクスとシミュレータ）などのツールを使用して、高レベルのLean関数と最適化されたアセンブリ実装の等価性を証明することに大きな関心が寄せられています。これにより、等価性が形式的に検証できるため、LLMは機能的なバグを導入することなくアセンブリコードを積極的に最適化できるようになります。
The "間違ったものの正しさ" Risk
形式検証は、実装が仕様に一致することを証明しますが、仕様そのものがユーザーが実際に意図したものであることを証明することはできません。コミュニティの議論で指摘されているように、LLMに提供された仕様も逆に間違っている場合、LLMは逆に実装された機能の正しさを熱心に証明することがあります。