AIにソフトウェアの推論を教える

アマゾン・ウェブ・サービス（AWS）のチームが、Soteriaのシンボリック実行トレースを用いてAIモデルにコードの推論を教える研究を発表しました。彼らの成果は顕著です：80億パラメータのモデルをSoteriaが生成した数千のトレースで継続訓練したところ、C言語のバグ検出において、4倍のサイズのモデルを上回る性能を示しました。

現代のAIコーディングアシスタントはソフトウェア開発を変革していますが、根本的な限界があります。正しく見えるコードを生成できても、そのコードが実際に正しいかどうかを理解するのが苦手です。大規模言語モデルは膨大なソースコードから学習しますが、ソフトウェア工学は単に構文的に正しいコードを生成することではありません。人間のソフトウェアエンジニアは、プログラムの実行を観察することで理解を深めます。デバッグセッション、実行トレース、テスト失敗などが、より深い意味論的理解をもたらします。

AWSの研究者はこのギャップを直接測定しました。C言語の500検証タスク（メモリ安全性、オーバーフロー、停止性、到達可能性、データ競合をカバー）で評価したところ、モデルはプロパティが成立することを確認するのは得意（ほとんどのモデルで90%以上）ですが、違反を検出するのは苦手であることが明らかになりました。14モデル中4モデルは実際のバグの半分未満しか検出できず、プログラムが長くなるにつれて精度は急落しました。

ここでSoteriaが登場します。Soteriaはソフトウェアの振る舞いを深い意味論レベルで推論するシンボリック実行ツールです。プログラムの状態、シンボリック値、パス条件、分岐決定を記録し、バグが発生する正確な条件を捉えます。これらのトレースは機械可読なJSONやインタラクティブなHTMLとしてエクスポートでき、シンボリック実行を検証技術から訓練データのソースへと変えます。

研究者はSoteriaをオープンソースのCコード上で実行し、トレースを収集。それらを用いてQwen3-8Bモデルを継続事前訓練しました。結果、訓練されたモデルはソフトウェア検証タスクで大幅に向上しました。最も効果的だったのは、Soteriaのバグトレースで訓練し、推論時にステップバイステップで推論させる組み合わせで、違反検出がベースラインから17.9ポイント向上しました。訓練後の8Bモデルは、未訓練の32Bモデル（57%）よりも高い違反検出率（67%）を達成しました。

さらに重要なのは、訓練が5つのプロパティタイプすべてに一般化したことです。モデルは特定のバグ形状を記憶するのではなく、一般的な推論パターンを学習していました。これは、次世代AIがソースコードだけでなく、プログラムの実行方法を示す意味論からも学習できることを示しています。

Soteriaチームは、これによりAIと検証の間に強力な好循環が生まれると見ています。AIがコードを生成し、Soteriaがそのコードを分析して意味論トレースを生成し、トレースがより良いAIモデルの訓練に役立ち、さらに高品質のコードが生成されるというサイクルです。長期的な目標は、crates.io（Rustのパッケージレジストリ）全体でSoteriaを実行し、Rustコードのこれまでにない大規模な意味論データセットを構築することです。

ソフトウェア工学の未来は、AIと形式検証の相互作用によって形作られるでしょう。最も強力なシステムは、最新の言語モデルの創造性とスケーラビリティを、形式推論の厳密さと精度と組み合わせたものになると考えられます。Soteriaはその交差点に構築されました。