正しいコードと検証済みプログラムの間の溝

LLMはコンパイルできてcargo testも通るRustを書ける。しかし、すべての可能な入力に対してコードが正しいことを保証する形式的証明を書くのは、今のところ信頼できない。

問題はRustの構文ではない。形式的検証では、何を証明したいかを明示し、証明を成立させる不変条件を見つけ、それら両方を検証器が受け入れる言語で表現しなければならない。LLMはソースコードで訓練されるが、証明そのものではない。定理は見るが、成功する証明の前にある何十回もの失敗をほとんど見ない。

再帰的な二分探索をGPT-4に貼り付けて「これを証明して」と頼むと、証明らしきものが返ってくる。ループ不変条件や事前条件に言及する。しかし、Dafnyの構文を混ぜたり、存在しない補題を引用したり、事後条件を導くには弱すぎる不変条件を断言したりする。検証するまで正しそうに見える。

Rustの形式的検証が実際にどう見えるか

Rustにはいくつかの検証ツールがある。Kaniは、関数のあり得るすべての状態を限界まで網羅的に探索するモデルチェッカーだ。PrustiとCreusotは、Rustを論理式に変換し、SMT solverに性質の証明を求める推論検証器だ。いずれも特定の構文による注釈が必要だ。

以下は単純な関数と、Creusotにおける実際の推論証明の例だ：

// Requires creusot-contracts crate
use creusot_contracts::*;

#[requires(a.len() > 0)]
#[ensures(result == a[0])]
pub fn first<T>(a: &[T]) -> &T {
    &a[0]
}

Creusotは、事前条件a.len() > 0が事後条件result == a[0]を保証することを検証する。これは論理が単純なので自明だ。次に難しくしてみよう：

use creusot_contracts::*;

#[requires(n <= 1000)]
#[ensures(result == n * (n + 1) / 2)]
pub fn sum_to(n: u32) -> u32 {
    let mut i = 0;
    let mut s = 0;
    #[invariant(i <= n)]
    #[invariant(s == i * (i + 1) / 2)]
    while i < n {
        i += 1;
        s += i;
    }
    s
}

不変条件が難しい部分だ。人間は、反復のたびに何が真であり続けるかを考えて書く。LLMは訓練データにそのパターンがあるからとs == i * (i - 1) / 2を推測したり、不変条件を完全に省略してsolverを失敗させたりする可能性がある。

LLMに証明を頼むと何が起きるか

これをいくつかのモデルでテストした。プロンプトは「Creusotを使ってnの階乗を計算する、完全な事前条件・事後条件・ループ不変条件を持つ検証済みRust関数を書いて」だった。

返答は3つのカテゴリーに分かれた。

第一に、見かけは正しそうだが誤った構文を使う注釈を出力したモデルがある。#[requires(...)]の代わりに#[precondition(...)]と書いたり、Prustiの構文とCreusotの構文を混ぜたりした。コードはパースすらしない。

第二に、構文的には正しいが不変条件が弱すぎる注釈を出力したモデルがある。階乗関数にはres == fact(i)のような不変条件が必要だ。モデルはしばしばres >= iと書く。これは真だが、事後条件の証明には役立たない。Creusotは目標を導けないと報告し、LLMには修正する仕組みがない。

第三に、不変条件自体は合っていたが、補助補題を幻覚ででっち上げた返答もある。Creusotの標準ライブラリに存在しないmath::fact関数を参照した。この論理的定義を自分で構築しなければ証明は成立しない。

いずれのモデルも、初回で検証を通る証明を出力しなかった。

検証ワークフローでLLMが実際に役立つ場所

これはLLMが形式的検証に役立たないという意味ではない。正しい用途で使う必要があるという意味だ。

定型コードの生成には長けている。関数シグネチャが与えられれば、LLMは通常、自明な契約を捉える#[requires]句と#[ensures]句を出力できる。fn divide(a: i32, b: i32) -> i32という関数に対して、正しく#[requires(b != 0)]と#[ensures(result * b == a)]を提案する。これは深い洞察ではないが、打鍵数を減らせる。

検証器のエラー説明にもそれなりに使える。Creusotが「cannot prove loop invariant」と報告したら、そのエラーメッセージをLLMに貼り付けると、不変条件が何をすべきかの有益な説明が得られることが多い。正確な不変条件を提案はしないが、探索空間を絞り込める。

検証言語間の翻訳にも役立つ。Dafnyの証明をPrustiに移植したいとき、LLMは構文の対応付けの大部分を処理できる。根底にある論理は同じだ。これはまさにLLMが得意とするパターン認識の作業だ。

根本的限界：証明は探索であり、補完ではない

証明を書くことは、Webサーバーを書くこととは違う。Webサーバーを書くとき、正解は多数ある。証明を書くとき、正解はただ一つ、あるいはごく少数の族しかなく、それ以外はすべて誤りだ。

LLMは次トークン予測器だ。文脈を踏まえて最もありそうな続きを生成する。証明のステップは、最もありそうな続きではない。証明責務を閉じるステップであり、20番目や2000番目にありそうな選択肢かもしれない。

ソート関数が入力の順列を返すことを証明することを考えてみよう。核心的な洞察は通常、多重集合を定義するか、出現回数を数えることだ。LLMは長さを比較することを提案するかもしれない。これは必要だが十分ではない。長さの等しさが順列を意味しないことを認識し、カウント不変条件を導入するのは人間の仕事だ。

Kaniを使ったモデルチェックは、不変条件を必要としないため、この問題の一部を回避する。LLMはkani::proofハーネスを、ユニットテストのように見えるため、より確実に生成できる。しかしKaniは限界検証にしか使えない。無限の証明が必要なら、依然として人間が必要だ。

両方を使う実用的なワークフロー

今日Rustを検証したいなら、ここに実際に機能するワークフローがある。

まず普通にコードを書く。cargo testを実行する。次に契約を追加する。LLMを使って、関数シグネチャから#[requires]句と#[ensures]句を生成する。注意深くレビューする。モデルは簡単なものは正しく、難しいものは微妙に間違える。

検証器を実行する。少なくとも一つのループで失敗する。エラーメッセージを取って、どの不変条件が欠けているかLLMに説明させる。その説明を答えではなく出発点として使い、不変条件は自分で書く。

繰り返す。検証器は不変条件が十分強いか教えてくれる。LLMは教えてくれない。モデルを、構文は知っているが証明を完成させたことがないペアプログラマーとして扱え。

この問いへの正直な答え

LLMはRustの形式的証明を書けるか？　いいえ。まだできない。論理を理解した人間なしには無理だ。

フレームワークの作成、エラーの説明、ツール間の翻訳はできる。しかし、証明を成立させる不変条件や補題、帰納法の仮説を見つけるのは、いまだに人間のスキルだ。

分離論理やHoare tripleの学習を飛ばせるツールを探しているなら、LLMはそれではない。構文や定型コードを処理して、自分は論理に集中できるようにすることで、学習曲線を緩やかにするツールを探しているなら、LLMは試す価値がある。

不変条件なしで限界チェックがしたいならKaniから始めよう。無限の証明が必要になったらCreusotかPrustiに移行しよう。構文を正しくするのにLLMを使うが、証明は自分で書くつもりでいよう。

よくある質問

Rustにおける形式的検証とは何か？

形式的検証は、数学的論理を用いて、プログラムがすべての可能な入力に対して仕様を満たすことを証明する手法だ。Rustでは、Kani、Prusti、Creusotなどのツールが関数に注釈を追加し、事前条件・事後条件・不変条件を記述する。検証器がこれらの性質が成立するかを検証する。

ChatGPTはKaniの証明を書けるか？

ChatGPTは、#[kani::proof]属性を持つユニットテストのようなKani証明ハーネスを書ける。これらのハーネスはループ不変条件を必要としないため、推論証明より生成しやすい。ただし、仮定や表明を含む複雑なハーネスは、依然として人間のレビューが必要だ。

KaniとCreusotの違いは何か？

Kaniは限界モデルチェッカーだ。限界までのすべての可能な実行経路を探索し、パニックや表明違反を検出する。Creusotは推論検証器だ。Rustを論理式に変換し、SMT solverを使ってすべての入力についての性質を証明する。無限ループも含めて扱えるが、ユーザーが提供した不変条件が必要だ。

なぜLLMはループ不変条件に苦労するのか？

ループ不変条件は、反復を通じて何が真であり続けるかを推論する必要があり、これは帰納的推論の一形態だ。LLMは、ありそうな文章の続きを予測するように訓練されるが、証明責務を閉じる正確な論理的記述を探索するように訓練されていない。正しい不変条件は、最もありそうな次のトークンではないことが多い。