Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability
本論文は、多様でタスク等価なプログラム実装を生成することが、形式的な証明に適したバリアントを特定することによって自動検証の成功率を大幅に向上させることを示す、LLMベースのパイプラインであるDiversify2Verifyを紹介するものである。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
あなたは、数学パズルを解くことができるロボットを作ろうとしていると想像してください。あなたには、コードを書くのが得意な超スマートなAIアシスタント（大規模言語モデル）がいます。通常、私たちはAIに「このパズルを解くコードを書いて」と頼み、ロボットがいくつかのテスト走行に合格するかどうかを確認します。合格すれば、「よくできました！」と言います。
しかし、**形式検証（formal verification）**の世界では、いくつかのテストに合格するだけでは不十分です。それは、橋を建設する際に、おもちゃの車を走らせてみるようなものです。本当に安全であるためには、いかなる車、いかなる時間、いかなる条件下でも、その橋が耐えられるという数学的な証明が必要です。これが「演繹的検証（deductive verification）」と呼ばれるものです。
問題は、単に正しいだけでなく、証明しやすいコードをAIに書かせることは非常に難しいということです。時として、AIは完璧に動作する解決策を提示しますが、その構造があまりに乱雑だったり、奇妙だったりするため、「証明チェッカー」（Why3と呼ばれるツール）が混乱して検証できなくなることがあります。
大きなアイデア：一つの方法だけに固執しない
著者であるShirley Yu氏とRuben Martins氏は、次のようなシンプルな問いを投げかけました。「もし、たった一つの解決策を求めるのではなく、同じ解決策の異なるバージョンをたくさん求めたらどうなるだろうか？」
これは、固い瓶の蓋を開けようとしている状況に似ています。
- バージョンA： 右手で蓋を回そうとする。
- バージョンB： 左手で蓋を回そうとする。
- バージョンC： スプーンで蓋を叩いてみる。
- バージョンD： お湯をかけてみる。
「右手での回転」（AIが最初に書いたコード）が、証明チェッカーにとって掴みどころのない、滑りやすいものかもしれません。しかし、「左手での回転」は、その形状がチェッカーの論理に完璧にフィットするかもしれません。論文ではこれを Diversify2Verify と呼んでいます。一つの完璧なコードを期待するのではなく、彼らは同じタスクに対して4つの異なる「フレーバー（味付け）」を生成しました。
- 配列 + 命令型（Array + Imperative）： 一列に並んだ人々を一人ずつ確認しながら進むようなもの。
- 配列 + 再帰型（Array + Recursive）： ヘルパーたちがリレー形式でタスクを伝えていく「伝言ゲーム」のようなもの。
- リスト + 命令型（List + Imperative）： インデックスカードの束をパラパラとめくるようなもの。
- リスト + 再帰型（List + Recursive）： 各人形の中に次の人形が入っている、ロシアのマトリョーシカのようなもの。
実験：73個のパズル、292回の試行
チームは、73種類の異なるプログラミングパズル（主に数値、リスト、配列に関するもの）を含む特別なプレイグラウンドを構築しました。各パズルについて、彼らはAIにこれら4つの「フレーバー」すべてを生成させました。これにより、テスト対象となる292個の異なるコード試行が得られました。
彼らは単にAIにコードを書かせたのではなく、厳格な3段階のプロセスを設定しました。
- ステージ1（契約/コントラクト）： まず、AIに「どのように行うか」を心配することなく、コードが「何をしなければならないか」を記述した「契約（ルールブック）」を書かせました。次に、このルールブックが意味の通るものであることを、例題を用いて確認しました。一度承認されたルールブックは、凍結されました。後からルールを変更することはできません！
- ステージ2（コード）： 次に、AIに4つのフレーバーそれぞれの実際のコードを書かせ、基本的なテスト走行に合格することを確認しました。
- ステージ3（証明）： 最後に、各コードのバージョンが凍結されたルールブックを満たしていることを証明しようと試みました。もし証明に失敗した場合は、AIにヒント（修復）を与えて証明を修正させましたが、これは証明のみに対するものであり、コードやルールを変更するためのものではありませんでした。
結果：多様性が勝つ
実行結果の数字は以下の通りです。
- 「ワンショット」の失敗： AIが書いた最初のコードをそのまま使って証明を試みた場合、292個中96個（約32.9%）しか成功しませんでした。これは3件に1件未満です！
- 修復の力： AIに2回まで証明の修正を許可すると、数は292個中154個（約52.7%）へと跳ね上がりました。
- 多様性の力（真の勝者）： 73個のパズル全体として見たとき、49個のパズル（成功率67.1%）において、少なくとも一つのバージョンが正しく証明できることがわかりました。
これが主要な発見です。**「タスクとして同等な実装であっても、検証可能性（verifiability）は大きく異なる」**ということです。言い換えれば、全く同じことを行う2つのコードであっても、その証明のしやすさは天と地ほどの差があるのです。
何ではないのか（否定された事項）
この論文は、自分たちが主張していないことについても非常に慎重に記述しています。
- より良いコードについての話ではない： 「配列の方がリストより優れている」とか「再口帰の方がループより優れている」といったことは、彼らは見出していません。実際、結果は混在していました。再帰的なコードは一般的に命令型（ループベース）のコードよりも証明しやすい傾向にありましたが、配列とリストのパフォーマンスは全体として同様でした。重要なのは、どのスタイルが「ベスト」かを選ぶことではなく、選択肢を持つことでした。
- ルールを変更することではない： 彼らは、AIが証明を容易にするために「契約（ゴール）」を変更することを厳格に禁止しました。もしAIがゴールを書き換えて証明を楽にしようとしたなら、それは失敗とみなされました。彼らは、より弱いゴールではなく、元のゴールを証明することを求めていたのです。
- あらゆるものに対する魔法の杖ではない： この研究は、整数、配列、リストを含むパズルのみを対象としています。これが浮動小数点数や複雑な3Dグラフィックス、あるいはインターネット通信を行うプログラムにも通用するとは主張していません。
どれほど確信しているのか？
著者らは、測定については自信を持っていますが、全体像については慎重です。
- 測定されたこと： 彼らには明確な数字があります。ツールを実行し、成功数をカウントし、多様性が個々のアーティファクトの成功率を32.9%から52.7%へ、タスク全体の成功率を67.1%へと向上させたことを確認しました。
- 示唆されていること： 彼らは、命令型コード（ループ）の証明が難しかった理由として、ループの中で何が起きているかについてのルールである「ループ不変量（loop invariants）」の自動生成がAIにとって困難であることを示唆しています。もしAIにこれらのルールを推測するためのより優れたツールを与えれば、その差は縮まるのではないかと彼らは考えています。
- 未証明（現時点）： 彼らは、「配列の契約」と「リストの契約」が数学的に同一であることを証明したわけではありません。タスクの説明に基づき、それらが同じ意味を持つと仮定したに過ぎません。また、ルールがパズルと一致しているかを判定する「判定器（judge）」は完璧な人間専門家ではないため、微細なミスが紛れ込んでいる可能性も認めています。
まとめ
この論文は、AIに「検証済み」のソフトウェアを求める際、一つの答えを求めて期待するだけでは不十分であることを示唆しています。代わりに、選択肢のメニューを求めるべきです。同じ問題を解決するための異なる方法を生成することで、証明チェッカーが実際に理解できるバージョンを見つけられる確率が高まります。
それは、鍵穴に合う鍵を探すようなものです。もし鍵を一つしか持っていなければ、行き詰まってしまうかもしれません。しかし、たとえそれらがすべて同じドアを開けるものであったとしても、鍵のリングを丸ごと持っていれば、その中のどれかが鍵穴に完璧にフィットする可能性は極めて高いのです。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。