ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification
本論文は、大規模Cプログラムおよび変換されたLFモデルの検証における状態空間爆発を克服するために、大規模言語モデルを活用して関数契約を合成し、CEGAR-CEGISループを通じてそれらを反復的に改良するトップダウン型の構成的検証ツールであるConVerを導入する。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
巨大で複雑な工場の完璧な稼働を証明しようとしていると想像してください。その工場には、巨大な網の目状に接続された数千台の機械、コンベアベルト、そして作業者がいます。もし、すべての機械、すべての歯車、すべての作業者を同時に監視して誤りを見つけようとしたら、圧倒されてしまいます。膨大な情報量のために、誤りを見つける前にあなたの脳が「爆発」してしまうでしょう。これは、大規模なコンピュータプログラムを検証しようとするソフトウェアエンジニアが直面する問題と全く同じです。コンピュータが一度にチェックできる状態の数が多すぎるのです。
本論文は、この「圧倒」の問題を、コードのチェックの「方法」を変えることで解決する新しいツール「CONVER」を紹介します。工場全体を一度に見つめるのではなく、CONVER は問題を小さく管理可能なピースに分解する、賢明なトップダウン型の管理者のように機能します。
以下は、簡単なアナロジーを用いた CONVER の仕組みです。
1. 「トップダウン」戦略：設計図対レンガ
通常、プログラムを検証するには、システム全体をチェックする前に、すべての関数（すべての小さな機械）に対して詳細なルールブック（「契約」）を作成する必要があります。これは、車が安全であると宣言する前に、車のすべてのネジのマニュアルを作成しようとするようなものです。これには永遠の時間がかかり、専門家が必要です。
CONVER はこの脚本を逆転させます。
- アナロジー： 目標は「工場は決して赤いウィジェットを製造してはならない」とします。
- 従来の方法： 各作業者に「あなたのルールは何ですか？」と尋ね、ボトムアップでシステムを構築しようとします。
- CONVER の方法： まず大きな目標（「赤いウィジェットなし」）から始めます。その後、AI アシスタント（大規模言語モデル、LLM）に、その大きな目標を確実に達成するための各作業者のルールを推測させます。「組立ラインの作業者がこの単純なルールに従えば、最終製品は安全になる」という具合です。作業者の脳がどのように機能するかを知る必要はなく、ルールに従うことだけが重要です。
2. 「賢明なループ」：探偵と AI
AI がルール（契約）を推測すると、CONVER は探偵と容疑者が「ルールを当てよう」というゲームをするような、2 段階のループを用いてそれらをテストします。
- ステップ A：システムチェック（管理者）： CONVER は、全員が推測されたルールに従う場合、工場全体が機能するかを確認します。機械の中身を見るのではなく、ルールを信頼するだけです。
- ステップ B：関数チェック（検査員）： CONVER は、実際の機械がそのルールに従えるかを確認します。
- 「CEGAR」ループ： 機械がルールに従えない場合、CONVER は諦めません。特定の誤り（「反例」）を取り出し、それを AI に示します。
- アナロジー： AI は「作業者は 50 ポンドを持ち上げられると思った」と言います。検査員は「いいえ、作業者は 50 ポンドの箱を落とした」と言います。AI はこの特定の失敗から学び、「作業者は最大 40 ポンドまで持ち上げられる」というより良い新しいルールを書き換えます。
- ルールが完璧になるまで、このプロセスが繰り返されます。
3. 「SMART ICE」学習：ノイズのフィルタリング
AI が誤りを犯すのは、ルールが間違っているからではなく、質問を誤解したからである場合があります。これを修正するため、CONVER は「SMART ICE 学習」と呼ばれる技術を使用します。
- アナロジー： 犬に芸を教えると想像してください。あなたが「待て」と言ったときに犬が座れば、それは良い芸です。しかし、犬がリスを見て座ったのであれば、それは誤警報です。
- 仕組み： CONVER は「誤警報」（ノイズ）をフィルタリングし、「実際の誤り」（シグナル）のみを保持します。エラーを「正（これが機能した）」「負（これは明らかに失敗した）」「含意（これが起これば、あれも起こらなければならない）」に分類します。これにより、AI は自分の誤りに混乱することなく、はるかに速く学習できます。
4. 「事前抽象化」のトリック：漫画版
無限ループを持つ工場のように、コードの一部はあまりにも複雑で、ルールをチェックすることさえ困難な場合があります。
- アナロジー： 機械を詳細に描くのが難しすぎる場合、CONVER はまず簡単な漫画版を描きます。漫画版が機能するかを確認し、機能すれば、漫画版を実際の機械に差し替えて再度チェックします。
- これにより、CONVER は通常、コンピュータのメモリをクラッシュさせるようなプログラムを処理できるようになります。
彼らが発見したもの
研究者たちは、CONVER を 4 つの異なる「コードのジム」でテストしました。そこには、単純な数学パズルから、複雑な現実世界のファイルパーサーや再帰ループまでが含まれていました。
- 単純なプログラム： 45 件の標準プログラムにおいて、CONVER は驚くほど成功し、その82% から 96%を検証しました。これらの大部分は、たった1 ラウンドのチェックで解決されました。つまり、AI は最初の時点でルールをほぼ完璧に推測したのです。
- より困難なプログラム： セキュリティ証明書の解析や複雑な再帰ループなど、より困難なセットでは、成功率は**33% から 64%**に低下しました。これは、これらのプログラムがはるかに理解しにくいものであるため、予想されることです。
- 「AI」要因： 彼らは 3 つの異なる AI モデル（Qwen、Claude、GPT）をテストしました。AI モデルが賢いほど、CONVER のパフォーマンスは向上しました。最も賢い AI（GPT-OSS 120b）が最も多くの問題を解決し、AI の「推測」の質が成功の鍵であることを証明しました。
結論
CONVER は、AI を用いてソフトウェアの「ルールブック」を作成し、その後、それらのルールブックを完璧になるまで修正する、賢明で反復的なプロセスを用いるツールです。それは、巨大で解決不可能なパズルを、小さく解決可能なステップの連続に変換します。
- 検証の必要性を置き換えるものではありません。 最も困難な部分（ルールの作成）を自動化します。
- すべての複雑なプログラムで 100% の成功を保証するものではありません。 しかし、以前は自動的にチェックすることが不可能だった多くの問題を解決します。
- 失敗を聞いて機能します。 ソフトウェアが失敗するたびに、このツールは「なぜ」失敗したかを正確に学び、AI により良い推測で再挑戦を求めます。
要するに、CONVER は、巨大な問題を小さなタスクに分解し、すべての失敗から学び、仕事が完了するまで計画を絶えず洗練させる、疲れを知らない超賢明な管理者のようなものです。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。