A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report
本論文は、Rust から Lean への抽出ツール、形式的暗号ライブラリ、および AI 証明器を統合した健全かつカーネル検証済みの検証パイプラインを提示し、Ethereum Foundation の zkEVM プロジェクトにおける本番環境向け Rust 暗号コードに対して機械検証済みの正しさ証明を成功裏に生成するものである。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
あなたが、巨大で目に見えない金庫（ゼロ知識仮想マシン）のデジタル鍵を製造する、極めて重要な工場を持っていると想像してください。もしこの工場の歯車の一つでさえわずかに曲がっていたら、金庫全体のセキュリティが侵害され、手遅れになるまで誰もそれに気づかないでしょう。
長年にわたり、これらの歯車を点検することは、熟練したメカニックのチームを雇って、一つ一つのボルトを手作業で検査するようなものでした。それは遅く、高価であり、メカニックが何かを見逃さないことに依存していました。
この論文は、3 つのことを行う新しい自動化された組立ラインについて説明しています。
- 複雑な言語であるRustで書かれた工場の設計図を、コンピュータが完全に理解できる普遍的な数学的言語（Lean 4）に変換します。
- 機械がどのように動作すべきかを示す、完璧で事前に書かれた「ゴールドスタンダード」を（ArkLibとCompPolyと呼ばれるライブラリを使用して）提供します。
- 変換された設計図をゴールドスタンダードと比較し、それらが一致することを証明する書面を作成する、超知的な AI アシスタント（AlephとAristotleと呼ばれる）を雇います。
以下に、簡単な比喩を用いてこのプロセスがどのように機能するかを示します。
1. 翻訳機（Rust から Lean へ）
工場の設計図は、エンジニアが高速で安全なソフトウェアを構築するために愛用する言語であるRustで書かれています。しかし、「数学的な裁判官」（Lean 4 システム）は Rust を話せず、純粋な数学のみを話します。
この論文では、AeneasとHaxと呼ばれるツールを翻訳機として使用します。これらは Rust のコードを受け取り、それを「純粋関数」的な数学に変換します。
- 比喩: 料理人の俗語（Rust）で書かれたレシピを、厳格で段階的な化学式（Lean）に翻訳すると想像してください。翻訳機はさらに、各ステップに「安全タグ」を追加します。あるステップが失敗する可能性がある場合（ゼロで割る、または材料が不足するなど）、翻訳はそれを明確にマークし、数学がそれをチェックできるようにします。
2. ゴールドスタンダード（仕様書）
「動作する」ことの定義がなければ、機械が機能することを証明することはできません。
- 比喩: ArkLibとCompPolyを暗号化の「公式ルールブック」と考えてください。これらには、「紙を折りたたむこと」（FRI フォールディング）や「Merkle ツリーのチェック」などの動作が数学的にどのようにあるべきかという、完璧で抽象的な定義が含まれています。
- 目標は、変換された Rust コード（工場の機械）が、ルールブックが言うべきことを、それ以上でもそれ以下でもなく、正確に行うことを証明することです。
3. AI 証明作成者（「脳」）
これが最もエキサイティングな部分です。コードが変換され、ルールブックが準備できたら、それらが一致することを証明する書面を作成する必要があります。伝統的には、人間の数学者がこの証明を書かなければならず、それは巨大で複雑なパズルを解くようなものでした。
この論文では、重労働を行うためにAI 証明機（Aleph と Aristotle）を導入しています。
- 比喩: AI を、疲れ知らずで超高速な探偵だと想像してください。あなたはその探偵に変換された設計図とルールブックを与えると、「つながりが見えました！ここに証明があります」と言います。
- 重要な安全チェック: AI は単に「正しい」と言うだけではありません。AI はLean カーネル（究極の裁判官）が読める言語で証明を書きます。カーネルは AI の論理のすべてのステップをチェックします。AI が間違えて推測した場合、カーネルはそれを拒否します。したがって、AI は創造的であっても、不正はできません。
彼らが実際に行ったこと
チームは、このパイプラインをEthereum Foundationのプロジェクト（具体的にはPlonky3とRISC Zero）で使用されている実世界の暗号化コードに適用しました。
- 成功: 彼らは、コードの特定の部分（データをどのように折りたたむかを計算することや、ツリーが正しく含まれているかを確認することなど）が数学的に完璧であることを証明することに成功しました。
- AI の役割:
compute_log_arity_for_roundという関数に関する特定の例において、AI（Aleph）は以前は行き詰まっていた（「sorry」とマークされており、「それが真であることは知っているが、まだ証明していない」という意味）2 つの複雑な証明を自動的に作成しました。 - 人間の役割: AI は論理パズル、「もし〜なら〜である」というシナリオ、および基本的な数学の処理において優れていました。しかし、それでも人間は以下を必要としました。
- 全体的な戦略（「ルールブック」）の設計。
- 複雑なループの処理（繰り返しシーケンスの中で正しいパターンを見つけるなど）。
- Rust コードが翻訳機にとって難しすぎて処理できない場合の変換エラーの修正。
躓き（エンジニアリングのギャップ）
この論文は、この組立ラインがまだ完璧ではないことを認めています。
- バージョンの不一致: 翻訳機、ルールブック、AI はすべて、数学言語のわずかに異なる「方言」を話します。チームは全員を同じバージョンに合わせるために調整する必要がありました。
- 変換の限界: ジェネリック型や外部ライブラリなどの複雑な Rust の機能は、翻訳機が変換するのが困難です。チームは、翻訳機が理解できるようにするために、いくつかのコードをより単純な「モデル」に書き直す必要がありました。
結論
この論文は、AI が人間のエンジニアに取って代わったと主張するものではありません。代わりに、以下のようなパイプラインを示しています。
- 人間がコードを変換し、目標を設定する。
- AI は、退屈で論理的な証明を書くための強力なアシスタントとして機能する。
- 厳格なコンピュータ裁判官（カーネル）が、安全性を確保するためにすべてを検証する。
その結果、プロダクショングレードの暗号化コードを、機械がチェックし、数学的に保証された証明に変換する稼働システムが実現し、「目に見えない金庫」を大幅に安全にしました。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。