AI生成によるLean証明によりCPythonのバグ418件を特定

AIエージェントにCPythonの内部Cコードを、機械的な数学的証明のために設計された言語であるLeanに書き換えるよう指示することで、研究チームはPythonインタプリタにおける418件のバグを発見しました。この形式化プロセスは、すでに60万行以上の検証済みコードを生成しており、Pythonが「奇妙な」エッジケースでどのように動作するかについて正確な数学的定義を強制することで、従来のテストでは見落とされる可能性のある重大な問題を特定しています。

このチャートは、CPythonコードベース全体におけるプロジェクトの形式化の範囲と進捗を視覚化したものです。

形式化パイプライン

このプロジェクトは、LeanモデルがCPythonのソースを正確に反映していることを保証するために、厳格な4段階のパイプラインに従っています。まず、AIエージェントがC関数をLeanに書き換え、エラーメッセージや整数のオーバーフローを含む正確なロジックを維持します。次に、これらのコピーを実際のPythonインタプリタと並行して少なくとも50,000の入力で実行し、それらが一致することを確認します。

この画像は、AIエージェントが正確なロジックを維持しながらCコードをLeanに書き換えるパイプラインの最初のステップを説明しています。

HN Digestによる図表（broyojo.comの報告数値に基づく）。数値はソースの記載通り。

第3段階として、チームは常に真であるべき特性を記述し、Leanの証明チェッカーを使用してそれらを検証します。最後に、元のモデルを作成しなかった別のAIエージェントが、その作業がソースに対して「忠実」であることを確認するためにレビューを行います。この独立したレビューを通過した関数のみが、受理されたものとしてカウントされます。

「関数の証明を書くことは、それらすべてのケースにおいて関数が正確に何をするかを記述することを強いる。証明チェッカーは曖昧な内容を受け入れないため、何も曖昧にすることはできない。」

— Formalizing CPython

隠れたバグの特定

形式的な証明にはすべての可能な状態の正確な定義が必要なため、このプロセスによってCPythonの動作が意図されたロジックから逸脱しているバグが明らかになりました。例えば、チームはオブジェクトの属性辞書上で特定のキーを使用した際にセグメンテーションフォールトを引き起こす辞書呼び出しを発見しました。

その他の発見には、XML編集におけるメモリ破損や、無視される文字の位置によって不正確なパディングを生成するbase32デコーダーが含まれます。また、このプロジェクトではpickleモジュールのC版と純粋なPython版の間の不一致も特定され、それらは異なるネストの深さで処理を中断することが判明しました。

「有用な」証明の課題

大きな障害の一つは、AIが「空虚な」証明（技術的には正しいが壊れたコードを検知できない記述）を生成するのを防ぐことでした。例えば、「もし関数が値を返せば、その結果は少なくともゼロである」という証明は、関数が常にクラッシュする場合であっても技術的には正しいことになります。

この画像は、記述が技術的に正しいものの機能的なバグを特定できない「空虚な」証明の概念を説明しています。

これを解決するために、レビュー担当者は現在、「壊れたバージョンの関数もこれをパスできるか？」という特定の質問を投げかけます。もし壊れたバージョンがパスしてしまう場合、その証明は却下されます。これにより、メモリ要求の失敗や操作の途中でユーザーコードがエラーを投げる可能性などを考慮するなど、モデルにより現実的なものになるよう強制されます。

制限とトレードオフ

形式的検証は高い信頼性を提供しますが、現在はコードベースのわずかな割合に限定されています。このプロジェクトでは対象範囲内の関数の約15.7%をカバーしており、CPythonのような大規模で古いコードベースのすべての複雑なエッジケースをモデリングすることは労力を要するためです。

さらに、検証された証明は、その記述がLeanモデルに従っていることのみを保証するものであり、必ずしも実際のPythonインタプリタに従っていることを保証するものではありません。もしモデル自体が不完全な場合（例えば、失敗する可能性のあるメモリ要求が常に成功すると仮定している場合など）、実際のソフトウェアにバグが残っていても証明は有効なままになる可能性があります。