インタプリタを完成させる

インタプリタを完成させる

公開日: 2026年10月16日

記事: Kiran Gopinathan, Nikhil Pimpalkhare, Yiyun Liu, Zenna Tavares

私たちはLLMに、小さなプログラミング言語がどのように振る舞うべきかについての厳密な数学的規則、すなわち形式的意味論を記述させました。その後、数学的証明の検証ツールであるLeanを用いて、その言語で書かれたコードを実行するプログラム（インタプリタ）が、RISC-Vコンピュータチップが理解する低レベル命令にコンパイルされた後も、これらの規則に従うことを証明しました。

LLMは、実稼働中のソフトウェアにおけるバグを発見・悪用する能力を驚くほど高めており、実世界でのAI支援型ハッキングの報告が増加しています。幸いなことに、LLMは検証済みソフトウェア（コンピュータによってチェックされた数学的証明が付属し、広範なクラスのバグを排除するプログラム）を作成する能力も急速に進歩しています。4月には、私たちのエージェントがJavaScriptからWebAssemblyへのコンパイラを構築しましたが、プログラムの振る舞いを維持していることを証明できませんでした。数ヶ月後、私たちのエージェントはLinuxのnftablesコンパイラを検証しました。これはファイアウォール規則をカーネルが実行する命令に変換するものです。9月には、MITの研究者であるFrans KaashoekとNickolai ZeldovichがAIエージェントを使用してxv6オペレーティングシステムカーネルをマシンコードまで検証しました。

Basisでの私たちの目標は、すべてのソフトウェアに適用可能な検証方法を開発することです。これにより、基幹インフラを支えるシステムは設計段階から安全になり、攻撃者の増大する能力に対抗できるようになります。LLMの能力が進歩するにつれて、ボトルネックは定理証明から仕様の問題へと移行しています。つまり、証明する命題が実際に私たちが気にかけている振る舞いを捉えていることを、どのように確信できるでしょうか？

プログラムについて何かを証明するには、まずそのプログラムが何をするのかを数学的に記述する必要があります。これは、それが書かれているプログラミング言語を記述することから始まります。つまり、各ステートメント、ループ、関数呼び出しが実行時に何を意味するのかを定義することです。これらの記述は形式的意味論と呼ばれ、紙とペンで書くこともできますが、Leanのような証明支援系で表現されることが増えています。少数の言語（Standard ML、WebAssembly、およびCompCert経由のC）には形式的意味論があり、また、多くのプロセッサが実行するRISC-V命令セットにもあります。これらの意味論の開発はそれぞれ数年間の専門家の努力を要しました。

しかし、ほとんどのプログラムは形式的意味論を持たない言語で書かれており、検証済みソフトウェアを大規模に展開する上での大きなボトルネックとなっています。意味論がなければ、証明すべき正確なものがありません。自然な解決策は、LLMを使用して意味論を書かせることですが、LLMは間違いを犯します。そして、壊れた意味論は、その上に構築されたすべての証明を損ないます。テストは役立ちますが、以下に示すように、意味論はすべてのテストをパスしても間違っている可能性があります。必要なのは、意味論自体を検証する手段です。

形式的意味論を持たない言語でも、実際にはそれらのプログラムの意味を定義するインタプリタやコンパイラを持っています。ここで、私たちはラジカルなアイデアを検討します。LLMに、その意味論が、すべてのプログラムについて実際のインタプリタと一致することを証明させるのです。インタプリタをグラウンドトゥルースとして扱います。これを行うために、インタプリタをRISC-Vにコンパイルします。RISC-Vの意味論はすでに形式的に定義されています。これにより、インタプリタが任意のプログラムに対して何をするのかの正確な（ただし読みにくい）記述が得られます。次に、LLMはその言語の読みやすい規則を書き、Leanで、すべての可能なプログラムに対して、それらの規則がコンパイルされたインタプリタが出力するものと正確に一致することを証明します。規則が間違っていれば、証明は行き詰まります。

私たちは、LLMが小さな言語のために意味論とその証明を同時に開発した実験について報告します。Leanを使用して、その言語で書かれたコードを実行するプログラム（インタプリタ）が、低レベルのマシン命令にコンパイルされた後もこれらの規則に従うことを証明しました。意味論と証明全体は、GitHubで公開されています。この記事の残りの部分では、この実験について詳しく説明します。まず、なぜ意味論が大規模な検証作業のボトルネックとなるのか、そしてなぜテストだけではそれらに対する信頼を構築するのに十分ではないのかを説明します。次に、証明プロセスがどのように意味論を洗練させたか、メモリ推論をどのように処理したか、そしてその結果に基づいてどのようなツールを構築したかを示します。

すべての検証済みプログラムは意味論から始まる

プログラムが何かを行うことを証明する前に、各操作がその状態をどのように変換するかを定義する必要があります。つまり、その意味論を定義する必要があります。ほとんどの言語は、参照マニュアルで意味論を非形式的に文章で説明しており、具体的な詳細はコンパイラまたはインタプリタの実装に任せています。形式的意味論は、Lean 4のような証明チェッカーが使用できるほど正確に、数学で規則を書き留めます。注目すべき例としては、CのCompCert、MLのCakeML、JavaScriptのJSCertの意味論があります。それぞれが数年間の専門家の努力を要し、しばしばその言語の限定的なサブセットしかカバーしません。

この実験では、NielsonとNielsonのSemantics with Applicationsのような教科書で使用されている小さな命令型言語であるWHILEの拡張バージョンを使用しました。私たちのバージョンは、整数、文字列、クロージャを持つ第一級関数、if、while、forループ、および実行時エラーを備えています。そのインタプリタは1,855行のCで書かれており、WHILEプログラムは次のようなものです（55を出力します）：

var i = 0;
var sum = 0;
while (i < 10) {
    i = i + 1;
    sum = sum + i;
}
println(sum);

LLMがWHILEのために書いた意味論は、各種類の式とステートメントに対応する一連の規則です。これらの規則は、式がサブ式に関してどのように評価されるかを説明します。整数加算の規則は次のとおりです。

st, env ⊢ l ⇓ a, st'    st', env ⊢ r ⇓ b, st''    a + b = c
──────────────────────────────────────────────────────────
                 st, env ⊢ l + r ⇓ c, st''

規則は下から上に読みます。一番下の行はその結論です。状態stと環境envから開始して、式l + rはcに評価され（⇓）、状態st''を残します。状態は変数の値、クロージャ、およびこれまでに印刷されたすべてを保持します。環境は、どの変数がスコープ内にあるかを示します。線の上にある前提は、結果がサブ式の結果からどのように導かれるかを説明します。まずlがaに評価され、状態st'が残ります。次に、その状態でrがbに評価され、st''が残ります。最後の前提a + b = cは、WHILEの64ビットラップアラウンド算術を使用して2つの整数値を加算します。

状態[x ↦ 5]と環境{x}で(1 + 1) + xを取ります。xは5を保持し、スコープ内にあります。規則を適用すると、次のようになります。

[x ↦ 5], {x} ⊢ (1 + 1) ⇓ 2, [x ↦ 5]    [x ↦ 5], {x} ⊢ x ⇓ 5, [x ↦ 5]
                              2 + 5 = 7
─────────────────────────────────────────────────────────────────────
              [x ↦ 5], {x} ⊢ (1 + 1) + x ⇓ 7, [x ↦ 5]

つまり、(1 + 1) + xを評価するには、まず(1 + 1)を評価して2を得て、次にxを参照して5を得て、それら2つの値を加算して7を得ます。サブ式のどちらも状態を変更しないため、[x ↦ 5]は変更されません。

最初の前提を正当化するために、加算規則を再度適用します。

[x ↦ 5], {x} ⊢ 1 ⇓ 1, [x ↦ 5]    [x ↦ 5], {x} ⊢ 1 ⇓ 1, [x ↦ 5]
                           1 + 1 = 2
───────────────────────────────────────────────────────────────
              [x ↦ 5], {x} ⊢ 1 + 1 ⇓ 2, [x ↦ 5]

これらの規則の適用は、全体の式の値をその部分の値から導き出すツリーを形成します。

LLMは約400行のこのような規則をLeanで記述しました（完全な意味論）。各規則はそれ自体は妥当に見えますが、エンドユーザーがそれらがWHILEプログラムが実際に実行されたときの振る舞いを忠実に記述しているかどうかを厳密に判断する方法はありません。

意味論はすべてのテストをパスしても間違っている可能性がある

意味論をチェックする通常の G方法は、それを実行することです。テストスイートを取り、意味論の下で各プログラムを実行し、実際のインタプリタの下でも実行し、それらが出力したものを比較します。残念ながら、実際には、このプロセスは生成された意味論に対する信頼を構築するには不十分です。

例えば、私たちの意味論の初期バージョンはWHILEインタプリタのために生成されたテストスイートをパスしましたが、関数の名前が59文字に達したときにバイナリと矛盾しました。

fn aaa…aaa() {}           // a name of 59 a's
println("" + aaa…aaa);

semantics:  <fn aaa…aaa>
binary:     <fn aaa…aaa

意味論では、関数を文字列と連結すると、その完全な名前が<fnと>の間に含まれるとされていました。バイナリは閉じカッコ>を省略し、長い名前の場合は名前の一部も省略しました。テストスイートのどのテストも、これほど長い名前の関数を試していませんでした。

その理由は、値を文字列に変換するときに+で連結するCインタプリタにあります。

static char *stringify(Value v) {
    ...
    char buf[64];
    switch (v.kind) {
    ...
    case VAL_FN: {
        const char *name = v.as.fn->fn_expr->as.fn.name;
        if (name)
            snprintf(buf, sizeof buf, "<fn %s>", name);
        else strcpy(buf, "<fn>");
        break;
    }
    default: strcpy(buf, "<native fn>"); break;
    }
    ...
}

stringifyは文字列値をそのまま返します。他の値は、まず64バイトのバッファに印刷され、その後新しく割り当てられた文字列にコピーされます。名前付きクロージャは<fn name>として、名前なしクロージャは<fn>としてレンダリングされ、組み込み関数はデフォルトの<native fn>にフォールスルーします。

snprintfは、64バイトのバッファに最大63文字を書き込みます。初期の意味論では、連結と印刷で同じレンダリング規則を使用しており、この制限を見落としていました。バイナリとの一致を証明するために、LLMは連結に独自のレンダラーを与える必要がありました。修正された意味論は、クロージャのレンダリングを最初の63バイトに切り詰めます。

"" + f        ⇓  take 63 ("<fn " ++ f ++ ">")

これは、実装が内部的に蓄積するものの、誰も明示的に書き留めないような詳細です。まさに、手書きまたはLLMによって書かれた意味論が見落とす可能性のある理由です。また、これはどのプログラムも気づかないような詳細でもありません。動的言語のコードは、ログ記録、名前によるディスパッチ、またはシリアライズされた値の比較のために、関数の文字列形式を日常的に利用しています。このような単純な違反でさえ、意味論の上に構築されたあらゆる検証作業を損ない、セキュリティ脆弱性を隠す可能性のある穴を残す可能性があります。安全でスケーラブルな意味論を構築するためには、テストを超えて進む必要があります。なぜなら、テストスイートは、誰か（またはエージェント）が書くことを考えたプログラムしかチェックしないからです。

インタプリタを完成させる

インタプリタを完成させるということは、人々が実際に実行する実装に対して意味論をチェックすることを意味します。言語がすでに持っているインタプリタをコンパイルし、LLMにバイナリが意味論をリファインすること、つまり、両者がすべてのプログラムの出力について一致することを証明させます。

私たちが証明した定理は次のとおりです。

theorem endToEnd_refinement :
  ∀ p c, Loaded interpRunLayout p (fillZero c) →
    (∀ out, BigStep p out ↔ Halts c out 0) ∧
    (Diverges c → ¬ ∃ out, BigStep p out)

この定理は、任意のWHILEプログラムpと任意のマシン構成cについて、マシン構成がLoadedプロパティを満たす場合、意味論はコンパイルされたバイナリが行うことと一致することを述べています。ここでLoaded interpRunLayout p (fillZero c)は、cがインタプリタバイナリを通じてpを実行しようとしているマシンであることを示します。最初の結論 (∀ out, BigStep p out ↔ Halts c out 0)は、意味論が出力outを導き出すのは、マシンがoutを出力して終了コード0で停止する場合と（成功裏に終了するプログラムの場合、予測される出力は同等です）、そうでない場合のみであることを意味します。2番目の結論は、マシンが無期限に実行される（Diverges c）任意のプログラムpは、意味論が終了出力を導き出さないプログラムであることを示しています。

この定理を、意味論とバイナリが出力の点で一致することを示す可換図として視覚化できます。以下の図では、上の矢印はプログラムpと意味論によって予測される出力outの関係を示しています。下の矢印は、マシン状態cとバイナリが正常に停止したときに出力される出力の関係を示しています。左側の破線は、プログラムとマシン状態を接続するLoaded条件です。この条件の下で、定理は両方の出力が一致することを示しています（右側の二重線で示されています）。オレンジ色の矢印は、その一致を証明する試みが失敗した場合に、LLMが意味論を修正するために戻る方法を示しています。

［画像: The top arrow relates program p to output out through BigStep. The bottom arrow relates machine state c to out through Halts. Loaded connects p and c on the left; a double line marks equal outputs on the right. An orange arrow returns failed proof obligations to the semantics for correction.］

マシンにロードされたプログラムについて、意味論と成功した実行は出力に関して一致します。

この定理は、両方向で誤った意味論を捉えます。意味論が過度に寛容であれば、バイナリが決して出力しない出力を導き出し、左から右への半分が失敗します。意味論が厳密すぎると、バイナリが行うことに対して規則がなくなり、右から左への半分が失敗します。いずれの場合も、LLMは解決できない証明義務を受け取ります。私たちの経験では、その義務は通常、間違った規則を指し示します。

RISC-Vはオープンなプロセッサ設計です。私たちは、Sailで記述されLeanに変換されたその形式モデルを使用して、各マシン命令がどのように実行されるかを定義します。バイナリは実際のELF実行可能ファイルです。1,855行のインタプリタCコードがgccでコンパイルされ、dlmallocとnewlibにリンクされており、合計で25,336命令です。比較のために、MachCSLで検証されたxv6カーネルは8,697のRISC-V命令で、6,593行のCとアセンブリから構築されていますが、その証明は並列処理もカバーしており、私たちのものには必要ありません。Cコンパイラの出力、Cライブラリ、およびメモリ割り当て器はすべて私たちの定理に含まれています。結果を信頼したい人は、上記のステートメント、仮説Loaded、およびHaltsとDivergesの2つの短い定義を読みます。彼らはBigStepを信頼する必要はありません。なぜなら、証明はそれをバイナリに対してチェックするからです。

意味論と証明を同時に開発する

証明の開発により、LLMは意味論の4つの詳細を考慮する必要がありました。

• 整数演算は64ビットでラップアラウンドする必要がありました。なぜなら、最小の整数の否定がマシンに対して満たされないためです。
• forループの初期化子は、Cが行うように、突然の状態を無視する必要がありました。
• 組み込み関数は、printと連結で異なるレンダリングを行う必要がありました。
• 長いクロージャ名は63バイトに切り詰める必要がありました。

各修正は、閉じられない義務として、または意味論と矛盾するバイナリの実行として開始されました。

63バイトの切り詰めは代表的な例です。連結ケースの証明では、意味論のレンダリングがバイナリのものと一致する必要がありましたが、長い名前では一致しなかったため、規則が変更されるまで義務は解決できませんでした。

証明はまた、LLMが生成したCライブラリに関する補題の誤りも捉えました。LLMは各関数が何をするかを述べ、そのステートメントをマシンコードに対して証明しました。単一のmalloc(24)の後にヒープが満たされないアロケータの予約、サイズがラップアラウンドする場合には偽となるrealloc補題、そしてそれを述べていない補題なしにerrnoを書き込むexitルーチンはすべて、閉じられない義務として同じように現れました。

分離論理によりバイナリ証明が扱いやすくなる

LLMは証明のすべてを書きました。困難のほとんどはメモリの推論にありました。malloc（メモリを割り当てる関数）の仕様が必要でした。これにより、新しいブロックの割り当てがインタプリタがすでに保持しているデータを維持することを証明できます。println("n = " + x)でさえ、3つの文字列を割り当て、そのうち2つを解放します。これらの呼び出し全体を通して、プログラムの変数と半構築された結果は無傷でなければなりません。

これを実現するための教科書的な方法は、各関数にフットプリント（関数が書き込む可能性のあるバイトのセット）とともにHoareトリプルを与えることです。フットプリントの外側のメモリに関する事実は、呼び出し全体で変更されずに引き継がれます。トリプル{ P } code { Q }は、「Pがcodeの実行前に成り立つ場合、Qが実行後に成り立つ」と読みます。mallocの場合、そのような仕様は、Fが固定アドレスのセットであるとすると、大まかに次のようになります。

{ heap H }
  p := malloc(n)
{ heap ((p, n) :: H)  and  p is fresh }
modifies F

残念ながら、そのようなFは存在しません。同じヒープから、malloc(32)は新しいトップチャンクのヘッダーをアドレス0x82000238に書き込みます。したがって、Fはそのアドレスを含める必要があります。しかし、malloc(64)は代わりにブロック[0x82000210, 0x82000250)を返します。これはそのアドレスを含んでいます。呼び出し元がそのブロックを所有すると、そのバイトに関する事実は後続の呼び出しでも維持されなければならないため、Fは0x82000238を除外する必要があります。LLMは、Leanで証明しました、固定アドレスのセットでは両方の要件を満たせないことを、問題を1つの事実ずつ回避しようとした最初の試みが3週間停滞した後で。

［画像: Two runs of malloc from the same heap. malloc(32) writes the new top chunk's header at 0x82000238; malloc(64) returns the block from 0x82000210 to 0x82000250, which contains 0x82000238.］

同じヒープから、malloc(32)はmalloc(64)が呼び出し元に渡すバイトを書き込みます。アロケータの書き込みフットプリントは、メモリの所有権が変更されるにつれて変更される必要があります。

分離論理は、フットプリントをヒープに依存させることでこれを解決します。私たちは、xv6証明の背後にある論理であるMachCSLを、新しくリリースされたiris-leanに移植しました。1 分離論理では、アロケータはアリーナの空きバイトを所有しており、mallocの仕様はそれらの一部を呼び出し元に渡します。

{ isHeap H }
  p := malloc(n)
{ (p = 0 ∗ isHeap H) 
  ∨ (isHeap ((p, n) :: H) ∗ blockOwn p n) }

ここで∗は分離結合子であり、その2つの半分がメモリの分離された部分に成り立つことを示し、結果pはnullまたは新しいブロックです。isHeap Hは、ライブブロックH以外のすべてのアリーナバイトを所有します。最初に、アロケータは0x82000238を所有しているため、malloc(32)はそのバイトを書き込むことができます。呼び出し元が代わりにmalloc(64)を要求した場合、そのバイトはblockOwnを通じて呼び出し元に渡され、後続の呼び出しはそれに触れることができません。呼び出し元が所有する他のすべては仕様で言及されておらず、フレーム規則はそれを1ステップで呼び出しを通過させます。移植後、証明の残りは数日で閉じました。

［画像: The development in three lanes: fixed inputs (the interpreter, its binary, the Sail model, Lean's kernel), what LLMs wrote (the semantics, the representations, the separation-logic proof), and what is checked and read (boot witnesses and the refinement theorem).］

LLMは意味論と、それを既存のインタプリタバイナリにリンクする証明を書きます。Leanはその証明をマシンモデルに対してチェックします。

証明はピーク時には約100万行のLeanになり、そのうち3分の2はLLMが書いた35のスクリプトによって生成され、バイナリを読み込み、約11,800命令それぞれについて証明規則を出力しました。後続のパスで生成された証明ファミリーを抽象化されたもの（マシンコードのシンボリックエグゼキュータなど）に置き換え、証明を200,000行未満にしました。Leanの標準公理（propext、Classical.choice、Quot.sound）以外の公理は使用していません。

定理は実際のプログラムに適用される

仮説を持つ定理は、その仮説が満たされる場合にのみ有用です。もしLoadedが決して発生しないマシン状態を記述していた場合、私たちの定理は空虚に成り立ち、バイナリについて何も教えてくれません。

私たちはLLMに、Leanで10個のプログラムに対してLoadedが成り立つことを証明させました。それぞれについて、インタプリタのエントリポイントで、プログラムがバイナリ、ランタイム、アロケータと共にメモリ上にあるマシン状態を構築しました。Leanは各状態が定理の前提条件を満たしていることをチェックしました。2

［画像: A memory map of the machine at the interpreter's entry, from 0x80000000 to 0x88000000: the ELF's code and constants byte for byte, runtime state in .data and .bss, the dlmalloc arena in its initial state holding the global frame and the AST of p, an 8 MiB stack with the interpreter object, and the registers pc, sp, gp, a0 to a3 at interp_run's entry.］

Loadedは、インタプリタバイナリを通じてプログラムを実行するために必要なメモリとレジスタを指定します。プログラムは構文ツリー（オレンジ色）として入力され、周囲のコードとランタイム状態はインタプリタから取得されます。

また、実行可能ファイルからの85,483ステップのマシン実行をリプレイし、結果のメモリが構築された状態とバイト単位で一致することを確認しました。実行可能ファイルとそのブートトレースからその状態へのリンクはスクリプトによってチェックされ、Leanは前提条件とそれ以降の実行をチェックしました。完全なループテストプログラム（以前の例に2つの追加の合計を追加したもの）については、バイナリはそれぞれ55、2500、36を別々の行に出力して停止することが証明されています。

前提条件には、プログラムのための十分なヒープとスタック領域が含まれています。後続の定理は、これらの2つの仮説を、実行時にチェックするチェッカーに置き換えます。

セマンティクスを信頼すれば、ツールは安価になる

検証済みの意味論はインターフェースとしても機能します。BigStepに対して健全だと証明されたものは何でも、リファインメント定理と組み合わせることでバイナリに対しても健全になります。そしてその組み合わせは、数行のLeanで済みます。そこで、LLMにそれを基盤とした4つのツールを構築させました。

［画像: A stack: the binary on Sail at the bottom, the refinement theorem above it, the semantics above that, and four tools on top: a type system, a program logic, an abstract interpreter and a verified compiler.］

型システム、プログラム論理、およびアナライザは、インタプリタのリファインメント証明を再利用します。コンパイラは、RISC-V上で直接同じ意味論を実装することが証明されています。

リファインメント証明は約1ヶ月かかり、約140,000行のLeanで構成されています。以下の4つのツールは3日間でプルリクエストとして公開され、合計で約33,000行、そのほとんどがコンパイラです。

最初のツールは型チェッカーです。プログラムが実行される前に無効な操作を検出します。例えば、次の2つのプログラムは拒否されます。

"a" - 1;               // subtracting an integer from a string

var x = 1;
x = "s";               // assigning a string to an integer variable

これらの例の証明は、どちらのプログラムもチェッカーをパスできないことを示しています。その健全性定理は、受け入れられたプログラムにおける型エラーを、インタプリタバイナリを通じて実行される場合でも排除します。ゼロ除算、失敗したassert、およびインタプリタのコール深度制限は依然として可能です。これらには、型だけでなく値に関する推論が必要です。

2番目のツールはプログラム論理であり、特定のプログラムが何を計算するかを証明できます。この投稿の冒頭近くのループは、1から10までの整数を加算します。完全なテストプログラムは、breakとcontinueを使用して1から100までの奇数も加算し、ネストされたループを使用して3番目の合計を計算します。LLMは、このプログラムをインタプリタバイナリを通じて実行すると、正確に次の値を出力して終了することを証明するために、この論理を使用しました。

55
2500
36

3番目のツールは抽象インタプリタであり、プログラム全体で可能な値を追跡し、潜在的な実行時エラーに対して警告を発する分析です。これは同じテストプログラムをアラームなしで分析し、実行時エラーがないことを証明します。また、sum、total、accの最終値がそれぞれ55、2500、36であることを確立します。この分析はこれらの結果を自動的に計算し、その健全性証明はそれらをバイナリの実行に結び付けます。

4番目のツールはインタプリタを完全に省略します。4月には、私たちのエージェントがコンパイラを構築しましたが、その正しさを証明できませんでした。ここでは意味論が先行し、LLMはWHILE全体（文字列、クロージャ、呼び出し、for、return、assert）からRISC-Vへの検証済みコンパイラを構築しました。上記の合計プログラムをコンパイルすると、生成されたマシンコードは同じ3つの数値を出力します。正しさの定理は、前提条件を満たすすべてのプログラムについての一致を確立します。チェック済みのバージョンは割り当てコストを分析するため、その定理は利用可能なヒープスペースに関する仮説を必要としません。

インタプリタを省略すると、WHILEプログラムはより高速になります。インタプリタのテストスイートのすべてのプログラムを、spike RISC-Vシミュレータで両方の方法で実行しました。インタプリタが評価を開始した時点からカウントすると（解析はそれに課金されないため）、コンパイルされたコードは2.7から8.2倍少ない命令をリタイアし、両方のルートは同じ出力を生成します。これらはハードウェアでのタイミングではなく、シミュレータでの命令数です。

［画像: Paired bars on a log scale of instructions retired per test program, interpreted versus compiled: arithmetic 2.7 times fewer when compiled, strings 3.1, functions 6.5, scope 6.7, for 6.9, recursion 8.0, while 8.2.］

これらのWHILEプログラムをコンパイルすると、命令数は2.7〜8.2倍削減され、出力は保持されます。カウントはspike RISC-Vシミュレータからのもので、インタプリタによる解析は除外されます。

意味論が信頼されるようになると、それは言語そのものとなり、最初に参照したバイナリはWHILEプログラムを実行するためにもはや必要なくなります。

次は何へ：Lua、OCaml、そしていつかCPythonへ

WHILE言語での実験は、トイ言語を対象としていました。LLMはその形式的意味論を開発し、コンパイルされたインタプリタがそれに従うことを証明し、その上に検証済みツールを構築しました。私たちは現在、このアプローチを実際の言語にスケールアップしています。

Ship your LuaはLua 5.4.7をベアメタルRISC-Vにコンパイルすることを対象としています。バイナリはすでにSailモデル上で実行されており、ネイティブLuaと一致しており、計画では証明をVMで分割します。まずバイトコードインタプリタをバイトコード意味論に対して、オペコードごとに断片化し、次にソース言語をバイトコードに対して検証します。

Ship your OCamlは、OCamlが自己ブートストラップする方法を利用します。OCamlのブートストラップコンパイラは、バイトコードboot/ocamlcとしてリポジトリにチェックインされており、ocamlrun上で実行されます。ocamlrunはSailモデル上で実行されており、実際のboot/ocamlcでプログラムをコンパイルしています。そこでの計画は、不動点に至ります。ソース意味論がコンパイラが自身のソースコードをboot/ocamlcのバイトと正確に一致するようにコンパイルすると述べ、コンパイラのバックエンドが正しいと証明されれば、それらのバイトは412,000バイトコード命令を1つずつ検証することなく意味を持つようになります。

両方のプロジェクトで、すでに主要な定理をLeanで記述しています。残りは証明を完了することです。

北極星はCPythonです。現在のエージェントは、十分な計算能力があれば、PythonのLLMによって書かれ、マシンによって検証された意味論を実現可能にすると信じています。前述のようなツールは、CPythonバイナリにまで及ぶ保証とともに、その上に構築できるようになります。

1. iris-leanが登場するまで、プロジェクトは本当に停滞していました。その著者たちに一杯おごる必要があります。↩︎

2. より強力なステートメントとして、バイナリがすべての適切に形成されたプログラムに対してLoaded状態に到達するということは、パーサーを検証する必要があることを意味します。パーサーはinterp_runの前に実行され、私たちの定理の範囲外です。↩︎

---