技術的概要：知的システムのための管理されたメタプログラミング

1. 問題提起

大規模言語モデル（LLM）や自律エージェントを含む現代の AI システムは、実行時に実行可能な構造を合成するようになりつつあります。これらのシステムは、ワークフロー、ツール呼び出しプラン、自己修正コードを生成します。古典的なホモイコン（例：Lisp）やステージング言語（例：MetaOCaml）では、コード表現（データ）から実行可能プログラムへの遷移は、eval や run などのプリミティブによって処理されます。これらの遷移は伝統的に無制限です：いかなる有効な表現も、直ちに実行中のコードとなる可能性があります。

管理された知的システム（明示的な効果の境界、能力制御、監査可能性を必要とするシステム）の文脈において、この無制限な遷移は重大な脆弱性を生み出します。システムが元の管理制約を回避する新しいプログラムを生成できる場合、管理モデル全体が侵害されます。本論文はこれを「メタプログラミングの脱出ハッチ」として特定しています。実行レベルでは管理されているが、コード生成レベルでは管理されていないシステムは、根本的に安全ではありません。

2. 中核的な方法論：eval の再分類

本論文の中核的な方法論的貢献は、eval（または形式から実行への遷移）を言語プリミティブから管理された効果へと再分類することです。

著者は、以下の柱に基づいた管理されたメタプログラミングというフレームワークを提案します。

• マシン形式（Machine Forms）: プログラム表現は、不透明な文字列やバイトコードではなく、第一級の値（構造化されたデータマップ）として扱われます。
• 純粋な形式操作: これらの形式に対するすべての操作（検査、変換、合成、差分比較）は純粋な計算として分類されます。これらは指令を発行せず、I/O を実行したりモデルを呼び出したりする能力を持ちません。
• 権限割り当てとしての具体化（Materialization）: マシン形式から実行可能なマシンへの遷移は具体化として定義されます。これは単なる計算ではなく、実行権限（モデルを呼び出し、I/O を実行し、リソースを消費する権限）の割り当てです。したがって、具体化は管理された効果として分類されます。
• 構造的検査: 具体化が許可される前に、管理システムが形式の決定可能な構造的検査を実行します。この検査は、能力要件、ポリシー準拠、モデル承認、およびリソース見積もりを分析します。

3. 形式的操作意味論

本論文は、純粋な計算と管理された実行の間の境界を強制するために、2 つの異なる判断を用いてシステムを形式化します。

1. 純粋な形式評価（$\Gamma \vdash pure\ e \Downarrow v$）:

   • 形式値に対して動作します。
   • ゼロの指令を発行します（$Dir(e) = \emptyset$）。
   • クォート構築、スプライス評価、ナビゲーション、変換を含みます。
   • 純粋な操作のいかなる系列も、承認されたマシンを生成できないことを保証します。

2. 管理された具体化（$\Gamma; \Pi; \sigma \vdash materialize(v_f) \rightsquigarrow \langle Machine, d \rangle$）:

   • 形式、ポリシー文脈（$\Pi$）、および能力セット（$\sigma$）を受け取ります。
   • 各結果（承認または拒否）に対して、管理決定記録（$d$）を要求します。
   • ちょうど 1 つの管理された指令を発行します。
   • 管理システムは、形式の構造を検査して以下を確認します。
     • 能力の包含（$CapSet(f) \subseteq \Pi.allowed\ caps$）。
     • モデル承認。
     • 構造的ポリシー準拠。
     • リソース境界。

4. 主要な貢献

本論文は、5 つの主要な貢献を提示します。

1. eval の再分類: 具体化を権限割り当てとして正確に特徴づけ、それをプリミティブから管理された効果へと移行させます。
2. マシン形式: quote、splice、reflection 用の構文を持つ、構造化されたプログラム表現のための具体的なデータ型。
3. 形式的意味論: データ操作と実行を厳密に分離する、2 つの判断（純粋な評価と管理された具体化）を用いたシステムの定義。
4. 機械検証された性質: 3 つの中核的な性質が Rocq で形式的に検証されています。
   • 形式操作の純粋性: 形式操作は指令を発行しません。
   • 回避不可能定理（The No-Bypass Theorem）: 純粋な操作のいかなる系列も、直接実行を引き起こすことはできません。
   • 境界の維持: メタプログラミング能力を追加しても、表現力と管理の境界は分裂しません（それらは一致したままです）。
5. 管理された自己修正: 外部のコード生成と同じ管理検査の対象となる進化台帳（evolution ledger）を介して、マシンが自己への構造的変更を提案することを可能にする具体的なメカニズム。

5. 実装と結果

この設計は、BEAM（Erlang VM）バイトコードにコンパイルされる AI ワークフロー用のドメイン固有言語であるMashinTalkで実装されています。

• システムアーキテクチャ: 実装は 3 つのモジュールで構成されています。Form（構築と操作）、FormInspector（管理チェック）、FormMaterializer（管理されたコンパイル）。
• 検証: 中核的な性質は、26 の定理と 662 行のコードで、承認された補題（admitted lemmas）がゼロという状態でRocq（旧 Coq）で機械化されています。これらの定理は、36 モジュールにわたる 454 の定理を含む既存の形式化と統合されています。
• テスト: 51 の単体テストからなるテストスイートが、機能的な正しさと管理の性質を検証します。すべてのテストが合格しました。
• パフォーマンス: Apple M シリーズプロセッサ上では、形式の構築は<1 µs、典型的なマシンに対する構造的検査は<100 µs です。オーバーヘッドは、BEAM バイトコードへのコンパイルと比較して無視できます。

6. 意義と主張

本論文は、管理された知的システムにおける「メタプログラミングの脱出ハッチ」を閉じると主張しています。このメカニズムがなければ、実行レベルで管理されているシステムも、新しい実行可能構造の生成を管理できないため、脆弱なままです。

著者は、自身の実行可能構造を合成する AI システムにおいて、実行権限の割り当ては以下のものでなければならないと論じます。

1. 可視性: データからコードへの遷移は、明確で観測可能な事象であること。
2. 仲介: 構造を検査する管理インタープリターを通過すること。
3. 記録: 決定が追記専用の台帳（進化台帳）にログされること。

本論文は、以下の限界を明示的に認めています。

• ライス定理（Rice's Theorem）: 構造的検査は決定可能ですが、意味論的な振る舞いについて推論することはできません。管理は仲介を保証しますが、生成されたプログラムの意味論的な健全性を保証するものではありません。
• 範囲: 境界維持の議論はアーキテクチャ的なものです。効果シグネチャセットに関する完全な保存性の証明は、将来の課題として先送りされています。
• 適用性: この設計は、MashinTalk のような効果境界構造を持つ言語に固有です。その汎用言語への適用可能性は未解決の問いです。

結論として、本論文は、eval が単なる計算関数ではなく、権限割り当ての事象であることを確立しています。それを管理された効果として扱うことで、知的システムは管理モデルを侵害することなく、自身の実行可能構造を安全に合成および修正できるようになります。