形式検証がAIのレビューボトルネックを解決する可能性

形式検証は、AIが生成したコードのレビューボトルネックを解決する可能性を秘めている。従来のソフトウェア工学では、AI生成コードの正しさを保証するために人手によるレビューが必要であり、これが開発効率の大きな障壁となっていた。しかし、形式検証はコードの仕様を形式的に定義することで、AI生成コードの正しさを自動的に検証可能にする。

記事では回路最適化器を例に、この手法の実際の応用を示している。回路最適化器は、出力回路が入力回路と等価であることを保証しつつ、回路サイズを削減することを目的とする。チームはLean言語を用いて約500行の仕様を記述し、最適化器の正しさを厳密に定義した。仕様の記述には約2日、さらに1日のチームレビューを要した。AIエージェントはこの仕様に基づいてすべての最適化器コードとその証明を生成し、人間の介入はほぼ皆無だった。チームはCIラベルとベンチマーク結果を確認するだけでPRを「レビュー」し、生成されたコード自体は一切見ていない。

ベンチマークテストの結果、回路サイズの削減効果は従来のRust実装と同等であり、実行速度は遅いものの、直近3日間で最遅のテストケースが3倍以上高速化した。統合はFFIを介して行われ、LeanでコンパイルされたCコードを既存のRustコードベースに段階的に組み込むことができ、コードベース全体を書き換える必要はない。

著者は、このアプローチが広く適用されるかどうかが鍵であると指摘する。実用的な速度向上を得るには、仕様の記述と監査のコストが実装の記述と保守のコストよりも大幅に低くなければならない。再利用可能な仕様ライブラリが役立つ可能性があり、例えばWebバックエンドのユーザーアカウントやアクセス権限などの概念を形式化できる。最終的に、ソフトウェア開発はコードではなく要件に焦点を当てるようになるかもしれない。重要な特性は形式的に指定され、その他はプロンプトと自動・手動テストで検証される。開発者は生成されたコードを見る必要がなく、使用されているプログラミング言語さえ知らなくてもよい。このパラダイムシフトは、AI時代のソフトウェア工学に新たな可能性を開く。