『ダフニーを使用してラストのアルゴリズムを正式に検証するための9つのルール（パート2）』

『9つのルールでダフニーを使用してラストのアルゴリズムを正式に検証するための方法（パート2）』

range-set-blaze Crateからの教訓

著者：Carl M. Kadie と Divyanshu Ranjan

これは、Dafnyを使用してRustアルゴリズムを形式的に検証する記事の第2部です。ルール7から9を見ていきます：

• 7. リアルなアルゴリズムをDafnyにポートする。
• 8. アルゴリズムのDafnyバージョンを検証する。
• 9. 信頼性向上のために検証を再構築する。

ルール1から6は、Part 1を参照してください：

• 詳細な説明でPythonでテキストから特徴を抽出するためのCountVectorizer
• 会議に窒息することなく、データサイエンティスト/アナリストの関与を促進する5つのアイデア
• 『Gradioを使ったリテンションの理解』

1. Dafnyを学習しない。
2. Dafnyを学習する。
3. アルゴリズムの基本概念を定義する。
4. アルゴリズムを具体化する。
5. Dafnyコミュニティの助けを借りる。
6. 異なる、より簡単なアルゴリズムを検証する。

これらのルールは、私たちが「range-set-blaze」というRustクレートのアルゴリズムを検証する経験に基づいています。

Part 1のルール 6では、InternalAddのアルゴリズムを検証できることを示していますが、これはRustクレートで使用されるアルゴリズムではありません。次にそのアルゴリズムに移ります。

ルール 7: リアルなアルゴリズムをDafnyにポートする。

以下は興味深いRust関数の一部です（一部のコードは省略されています）：

// https://stackoverflow.com/questions/49599833/how-to-find-next-smaller-key-in-btreemap-btreeset// https://stackoverflow.com/questions/35663342/how-to-modify-partially-remove-a-range-from-a-btreemapfn internal_add(&mut self, range: RangeInclusive<T>) {    let (start, end) = range.clone().into_inner();    assert!(        end <= T::safe_max_value(),        "end must be <= T::safe_max_value()"    );    if end < start {        return;    }    //... code continues ...}

Dafnyのポートの始まりは次の通りです：

method InternalAdd(xs: seq<NeIntRange>, range: IntRange) returns (r: seq<NeIntRange>)  requires ValidSeq(xs)  ensures ValidSeq(r)  ensures SeqToSet(r) == SeqToSet(xs) + RangeToSet(range){  var (start, end) := range;  if end < start {    r := xs;    return;  } //... code continues ...}

興味があるポイント：

• Rustコードでは、selfとオブジェクト指向のカプセル化が使用されています。Dafnyはこのコーディングスタイルをサポートしていますが、単純化のために今回は使用しません。具体的には、Rustコードはselfを変更しますが、Dafnyコードはより関数的に記述されており、変更不可のシーケンスを受け取り、新しい変更不可のシーケンスを返します。
• Rustコードは借用チェッカーでメモリを管理しています。これにより、range.clone()などの式が生まれます。Dafnyはガベージコレクタを使ってメモリを管理します。いずれの場合でも、メモリの安全性は確保されます。そのため、この検証では無視します。
• RustコードはTにジェネリック化されており、それは標準のRust整数型（例：u8、isize、i128）を含むよう他で定義されています。Dafnyコードはintで定義されており、任意のサイズの整数を表す単一の型です。これにより、このDafnyポートでは整数オーバーフローのチェックは必要ありません。[Kani Rust検証器を使用してオーバーフローの安全性を形式的に証明する方法については、以前の記事を参照してください。]
• Rustコードには、Rustで特定のケースを禁止するために必要な実行時のassert!が含まれています： u128::max_valueをRangeSetBlaze<u128>に挿入する。Dafnyは任意サイズのintを使っているため、この特殊なケースは無視されます。

アサイド：Rust-inclusive range 0..=u128::max_valueの長さは何ですか？答えはu128::max_value+1であり、標準のRust整数型では表現できないほど大きな値です。range-set-blazeクレートでは、長さをu128で表現できるように0..=u128::max_value-1の範囲に制限されています。

次に、internal_addアルゴリズムの残りを考えてみましょう。ソートされた不連続な範囲のリストと、挿入したい非空の新しい範囲があるとします。例えば

このアルゴリズムでは、新しい範囲の開始点の前（または同じ位置に）ある既存の範囲を見つけます。これを「前の」範囲と呼びます。そして、次の4つのケースを考慮します：

• ケース1：新しい範囲が前の範囲に接触していない場合、新しい範囲を挿入し、他の範囲に接触するかどうかをチェックします。
• ケース2：新しい範囲が前の範囲に接触しており、その先に広がっている場合、前の範囲の終点を延長し、他の範囲に接触するかどうかをチェックします。（他の範囲に接触しない場合、非常に高速になります。）

• ケース3：新しい範囲が前の範囲に接触していますが、その先に広がっていない場合、何もしません。（これは常に非常に高速です。）

• ケース4：新しい範囲がどの範囲よりも前に始まる場合、他の範囲に接触するかどうかをチェックしながらそれを追加します。

こちらがRustのアルゴリズムのコードです：

// コードの続き...// FUTURE: would be nice of BTreeMap to have a partition_point function that returns two iterators    let mut before = self.btree_map.range_mut(..=start).rev();    if let Some((start_before, end_before)) = before.next() {        // Must check this in two parts to avoid overflow        if match (*end_before).checked_add(&T::one()) {            Some(end_before_succ) => end_before_succ < start,            None => false,        } {            self.internal_add2(&range);        } else if *end_before < end {            self.len += T::safe_len(&(*end_before..=end - T::one()));            *end_before = end;            let start_before = *start_before;            self.delete_extra(&(start_before..=end));        } else {            // completely contained, so do nothing        }    } else {        self.internal_add2(&range);    }}

そして、こちらがDafnyのコードです：

// コードの続き...  var beforeHi := IndexAtOrBeforePlusOne(xs, start);  if beforeHi > 0 { // 最初ではない    var (startBefore, endBefore) := xs[beforeHi-1];    if endBefore+1 < start {      r := InternalAdd2(xs, range);    } else if endBefore < end {      r := xs[..beforeHi-1] + [(startBefore, end)] + xs[beforeHi..];      assume exists i: nat :: i < |r| && r[i] == (startBefore,end) && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..]);      r := DeleteExtra(r, (startBefore,end));    } else{      r := xs;    }  }  else // 最初  {    r := InternalAdd2(xs, range);  }}

興味がある可能性のあるポイント：

• Rustのコードは、キーと値を使ってBTreeMapを操作します。Dafnyのコードは、 (ランダムアクセス可能な) インデックスを使ってソートされたseqを操作します。私はDafnyの操作をRustの操作と合わせるようにしましたが、これによりDafnyのコードはより自然ではありません。
• Rustのコードはまた、self.len（RangeSetBlaze内の個々の整数の数）も更新します。 Dafnyのコードはこれを無視します。（lenの更新は将来Dafnyのコードに追加できる機能です。）
• 前述のように、Rustのバージョンには、Dafnyが無視するオーバーフローを防ぐためのコードも含まれています。

私は、internal_add2とdelete_extra、つまりinternal_addが呼び出す2つの関数のDafnyバージョンを書くことで、ポートを続けました。私は、これらの2つのメソッドが呼び出すメソッドを書くことでポートを完了しました。等。完全なポートは約185行のコードです。こちらでご覧いただけます。

これはバリデーションされていません。次にバリデーションを行います。

ルール8：Dafnyバージョンのアルゴリズムをバリデーションする。

このステップでは、assert文の形でコードにバリデーションヒントを追加します。Dafnyは、これらのヒントを使用してコードをバリデーションしようとします。Dafny初心者として、私（Carl）はヒントの追加がコーディングよりも難しかったことに気づきました。一部は、Dafnyがいつ（またはもし）満足して停止できるかわからなかったためです。

ただし、私はどのように開始すべきかを学びました。たとえば、InternalAddのコードの場合、検証エラーが2つ報告されます。まず、Dafny検証器は、ensuresのうちの1つが成立しない可能性があると報告します：

This postcondition might not hold: SeqToSet(r) == SeqToSet(xs) + RangeToSet(range)

注：「事後条件」はensuresに対応します。「事前条件」はrequiresに対応します。

次に、Dafny検証器は、DeleteExtraの事前条件（つまりrequiresの1つ）が証明できないと不平を言います。

まず、この問題に対処するために、メソッドの最下部にassertを追加します。これはensuresを反映するように書かれています。

// ... InternalAddの最後の行にこれを追加assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range);}

一旦、DeleteExtraの問題は無視します。

// ...      assume exists i: nat :: i < |r| && r[i] == (startBefore,end) && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..]);      r := DeleteExtra(r, (startBefore,end));//...

Dafnyバリデーターは、今でも新しい最終的なassertについて苦情を言います。それは「確認が成立しない可能性がある」と言っています。

InternalAddコードは、ネストされたifステートメントを使用して作業を5つのケースに分割します。次に、メソッドの末尾ではなく、各ケースの末尾にassertを移動します。結果の// caseコメントで終わる行を探してください：

method InternalAdd(xs: seq<NeIntRange>, range: IntRange) returns (r: seq<NeIntRange>)  requires ValidSeq(xs)  ensures ValidSeq(r)  ensures SeqToSet(r) == SeqToSet(xs) + RangeToSet(range){  var (start, end) := range;  if end < start {    r := xs;    assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 0 - 成功    return;  }  var beforeHi := IndexAtOrBeforePlusOne(xs, start);  if beforeHi > 0 { // 前に配置しない場合    var (startBefore, endBefore) := xs[beforeHi-1];    if endBefore+1 < start {      r := InternalAdd2(xs, range);      assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 1 - 成功    } else if endBefore < end {      r := xs[..beforeHi-1] + [(startBefore, end)] + xs[beforeHi..];      assume exists i: nat :: i < |r| && r[i] == (startBefore,end) && ValidSeq(r[..i+1]) && ValidSeq(r[i+1..]);      r := DeleteExtra(r, (startBefore,end));      assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 2 - 失敗    } else{      r := xs;      assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 3 - 失敗    }  }  else // 前に配置する場合  {    r := InternalAdd2(xs, range);    assert SeqToSet(r) == SeqToSet(xs) + RangeToSet(range); // case 4 - 成功  }}

Dafnyは現在、ケース0、1、および4が妥当であることを示しています。 ケース2は失敗します（そして、削除する必要があるassumeが含まれています）。 ただし、今のところ、ケース3に取り組みましょう。

この記事のルール7から思い出してください。ケース3は、既存の範囲（青い「前の」範囲）に完全に含まれる新しい範囲（赤）を追加する場合です。したがって、コードは何もする必要はありません。

したがって、論理的に考えると、何が分かりますか？「前の」範囲に含まれる整数が新しい範囲に含まれる整数の上位集合であることがわかります。また、「前の」範囲が元のソートされた不連続な範囲（青い範囲）の一部であることもわかっています。これらの2つのヒントをassert文を使用してコードに追加しましょう。

Dafnyはこれらの2つのヒントが真であることを確認しました（緑のチェックマーク）。しかし、まだ興味深いassertを受け入れていません（赤いマーク）。

もう1つのヒントが必要なようです。具体的には、Dafnyに、前の範囲に含まれる整数がすべてのソートされた不連続な範囲の整数の部分集合であることを納得させる必要があります。直感的には、これは前の範囲がリスト内の範囲の1つであるため真であると言えます。

このヒントを本体のない補題として書きます。Dafnyはそれを受け入れます。

余談：なぜDafnyが本体のないこの補題を受け入れるのでしょうか？私はわかりませんし、良い直感もありません。ただうまくいっただけです。うまくいかなかった場合は、本体にassert文を追加してみます。

補題を使用すると、ケース3は現在妥当です。

これにより、ケース0、1、3、および4が妥当であることが確認されました。次に、ケース2に進むことにしましょう。さらに、DeleteExtraなどの一部のメソッドはまだ妥当ではなく、それらに取り組む必要があります（ここで現在のコードを見ることができます）。

検証デバッグの一般的なアドバイスについては、Dafnyユーザーガイドのこのセクションを参照してください。また、Stack Overflowの回答とJames Wilcox教授によるミニチュートリアルもおすすめです。

全体的に、アルゴリズムの検証タスクを多数の小さな検証タスクに分割するアイデアです。プログラミングよりも難しいと感じましたが、あまり難しくなく、楽しい作業でした。

私は185行の通常のコードに約200行の検証行を追加しました（こちらで完全なコードをご覧ください）。最後のメソッドが検証できたとき、私は間違って終わったと思いました。

驚きと失望のたまご、すべてが最初に検証できた時点で作業が終了するわけではありません。プロジェクトが再度検証され、他の人にも検証されることも確認する必要があります。次に、このルールについて説明します。

ルール9：信頼性のために検証を見直す。

私は終わったと思っていました。その後、数式のMin関数の6行の定義をDafny標準ライブラリからコードに移動しました。これにより、検証が論理的な理由なく失敗しました。後で、それを修正したと思っていた後、使用されていないメソッドを削除しました。再び、検証は論理的な理由なく失敗し始めました。

何が起こっているのだろうか？ダフニーはランダムな探索によってヒューリスティック的に動作します。コードを表面的に変更したり（またはランダムなシードを変更したり）すると、探索に必要な時間が変わる場合があります。時間の変化が劇的になることもあります。新しい時間がユーザーが設定した時間制限を超えた場合、検証は失敗します。[詳細については、以下のヒント＃3で説明します。]

異なるランダムシードを試して検証の信頼性をテストする必要があります。以下は、10個のランダムシードを使用してファイルを検証するために使用したコマンドです（Windows上で使用しています）。

@rem Dafnyの場所を検索して、パスに追加する pathset path=C:\Users\carlk\.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%path%dafny verify seq_of_sets_example7.dfy --verification-time-limit:30 --cores:20 --log-format csv --boogie -randomSeedIterations:10

結果は*.csvファイルであり、スプレッドシートとして開くことができ、その後失敗を探すことができます：

余談：Dafnyの検証信頼性の測定方法については、このStack Overflowの回答[*.csvファイルの分析] とこのGitHubのディスカッション [dafny-reportgeneratorツールの推奨] を参照してください。

問題の箇所を発見した後、共著者のDivyanshu Ranjanを引き入れて助けを求めました。Divyanshu Ranjanは、Dafnyの経験を活かしてプロジェクトの検証の問題を修正しました。

以下は、プロジェクトの具体例を交えた彼のヒントです：

ヒント＃1：可能な場合は、「forall」と「exists」を関連付けたrequire文を削除してください。

（ルール4で説明したように）ゴースト関数SeqToSetは、ソートされたかつ互いに素な非空範囲のリストによってカバーされる整数の集合を返します。無効なValidSeq関数を使用して「ソートされており互いに素」とを定義しています。このforallの式を削除することができます：

ghost function SeqToSet(sequence: seq<NeIntRange>): set<int>  decreases |sequence|  // removed: requires ValidSeq(sequence){  if |sequence| == 0 then {}  else if |sequence| == 1 then RangeToSet(sequence[0])  else RangeToSet(sequence[0]) + SeqToSet(sequence[1..])}

私たちの視点からは、同じ有用な関数を持っています。Dafnyの視点からは、この関数は2つのforallの表現を避け、適用しやすくなっています。

ヒント＃2 Dafnyによる推測作業を回避するためにcalcを使用してください。

Dafnyのcalcステートメントを使用すると、結論に到達するために必要な正確な手順をリストアップします。たとえば、DeleteExtraメソッドからのcalcの例です：

calc {    SeqToSet(xs[..indexAfter+1]) + SeqToSet(xs[indexAfter+1..]);  ==    { SeqToSetConcatLemma(xs[..indexAfter+1], xs[indexAfter+1..]); }    SeqToSet(xs[..indexAfter+1] + xs[indexAfter+1..]);  ==    { assert xs == xs[..indexAfter+1] + xs[indexAfter+1..]; }    SeqToSet(xs);  ==    { SetsEqualLemma(xs, r[indexAfter], r2, indexAfter, indexDel); }    SeqToSet(r2);  }

コードのこの部分では、xsは範囲のシーケンスですが、ソートされていたり互いに素である必要はありません。このcalcは、次のように主張しています：

1. xs の二つの部分がカバーする整数は
2. その二つの部分の連結がカバーする整数は
3. xs がカバーする整数は
4. rs です。

各ステップでは、ステップの証明を助けるために補題またはアサートを含めることが許されます。例えば、次のアサートはステップ3からステップ4への移行を証明するのに役立ちます:

{ assert xs == xs[..indexAfter+1] + xs[indexAfter+1..]; }

効率と制御のために、これらの補題とアサートはそのステップを超えてバリデータには表示されません。これにより、Dafnyの焦点が絞られます。

Tip #3: timeLimit を使用して必要な場所で計算を提供する。

Dafnyは、ユーザが設定可能な timeLimit でメソッドのバリデーションの試行を停止します。10秒、15秒、または30秒の制限は一般的です。なぜなら、私たちユーザーとしては、絶対に起きないバリデーションが素早く失敗することを望むからです。しかし、バリデーションが最終的には成功することがわかっている場合、メソッド固有のタイムリミットを設定することができます。例えば、Divyanshu Ranjanは、DeleteExtra が通常はバリデートされるが他のメソッドよりも時間がかかることに気づき、メソッド固有のタイムリミットを追加しました:

method {:timeLimit 30} DeleteExtra(xs: seq<NeIntRange>, internalRange: IntRange) returns (r: seq<NeIntRange>)// ...

余談: timeLimit はコンピュータの速度の違いを考慮していないため、少し余裕をもって設定します。

Tip #4: split_here を使用してバリデーション問題を二つに分割する。

Dafny FAQs に説明されているように、時には一緒にアサートをバリデートする方が早く、時には一つずつバリデートする方が早いことがあります。

アサートのシーケンスを二つの部分に分割するために、assert {:split_here} true; 文を使用します。例えば、timeLimit でも DeleteExtra はタイムアウトしていましたが、Divyanshu Ranjan は次のように追加しました:

// ...else  {    r := (s[..i] + [pair]) + s[i..];    assert r[..(i+1)] == s[..i] + [pair];    assert r[(i+1)..] == s[i..];    assert {:split_here} true; // バリデーションを二つに分割    calc {      SeqToSet(r[..(i+1)]) + SeqToSet(r[(i+1)..]);// ...

Tip #5: 補題は小さく保ちます。必要に応じて、複数の補題に分割します。

時には補題が一度に行うことが多すぎることがあります。例えば、SetsEqualLemma を考えてみましょう。これは冗長な範囲を削除することに関連しています。例えば、xs に a を挿入すると、”X” でマークされた範囲は冗長になります。

SetsEqualLemma の元のバージョンには12の requires と3つの ensures が含まれていました。Divyanshu Ranjan はそれを二つの補題に分割しました: RDoesntTouchLemma (11の requires と2つの ensures) と SetsEqualLemma (3つの requires と1つの ensures)。この変更により、プロジェクトのバリデーションがより信頼性を持つようになりました。

これらのヒントを適用することで、証明の信頼性が向上します。バリデーションを100%信頼性のあるものにすることはできるでしょうか？残念ながら、それはできません。幸運のないシードによってDafnyがバリデートに失敗する可能性が常にあります。では、いつバリデーションの改善をやめるべきでしょうか？

このプロジェクトでは、Divyanshu Ranjanと共にバリデーションコードを改善し、任意の単一の実行でのバリデーションエラーの確率が33%以下になるまで改良しました。そのため、10回のランダムな実行で2〜3回の失敗が生じませんでした。100回のランダムな実行も試しました。100回の実行では30回の失敗がありました。

結論

以上がRustアルゴリズムの正当性を証明するための9つのルールです。このプロセスが簡単または自動化されていないことに失望するかもしれませんが、私はこのプロセスが可能であることに励まされています。

余談：高校の幾何学の授業以来、数学の証明は魅力的でイライラすると感じています。数学の定理は一度証明されれば永遠に真実とされます（ユークリッドの幾何学は今でも真実とされていますが、アリストテレスの物理学はそうではありません）。証明の過程は、どの公理を仮定できるかや証明がどれくらい大きなステップを踏むことができるかについて私の数学の授業はいつも曖昧だったため、「イライラする」とも言えます。Dafnyや同様のシステムは、この曖昧さを取り除き、自動的な証明チェックを行うことで、私たちが深く関心を持つアルゴリズムについての証明を作成するのに役立ちます。

アルゴリズムの正式な証明を行う価値はいつあるのでしょうか？関わる作業を考慮すると、アルゴリズムが複雑で重要である場合、または容易に証明できる場合に限って再度行うでしょう。

将来的には、このプロセスはどのように改善されるでしょうか？以下の改善点を見てみたいと思います：

• システム間の相互運用性 – 一度証明された幾何学の定理はもう二度と証明する必要がありません。アルゴリズムの証明をチェックするシステムがお互いの証明を使用できるようになると良いです。
• Dafnyと同じく簡単に使用できる全Rustシステム – この方向性のための作業については、[1,2]を参照してください。

余談：容易に使用できるRustのバリデーションシステムを知っていますか？それをinternal_addのバリデーションに適用することを検討してください。これにより、Rustシステムの使いやすさとパワーをDafnyと比較することができます。

• RustのCargo.lockファイルの証明のアナロジー – Rustでは、Cargo.lockを使用してプロジェクトの依存関係を確実な組み合わせで固定します。Dafnyが例えばメソッドを証明できた場合、その証明手順を固定することができれば、バリデーションも信頼性が高まります。
• バリデーションのためのAIの改善 – 私の直感では、わずかに改善されたChatGPTは必要なバリデーションコードの90%を作成するのに適していると思います。私は現在のChatGPT 4がDafnyに対して十分でないと考えています。おそらく、Dafnyのトレーニング例が不足していることが原因です。
• AIのためのより良いバリデーション – AIがコードを生成する際には、そのコードの正確さについて心配します。形式的なバリデーションは正確性の証明に役立つことがあります。（この例の小さな例については、私の記事Check AI-Generated Code Perfectly and Automaticallyを参照してください。）

プログラムの正当性に関する私たちの旅に参加してくれてありがとうございました。もし証明が必要なアルゴリズムがあり、これらの手順が証明の見つけ方に役立つことを願っています。

VoAGIでCarlにフォローしてください。私はRustとPythonの科学的なプログラミング、機械学習、統計について執筆しています。通常、月に1つの記事を書いています。

Divyanshu Ranjanの彼のブログで彼の他の作品を読んでください。形式的な手法に加え、そのブログでは幾何学、統計学などにも触れています。

We will continue to update VoAGI; if you have any questions or suggestions, please contact us!