🤖 machine learning

Synthesis and Verification of Transformer Programs (Technical Report)

本論文は、トランスフォーマーの表現力を捉える言語構成要素である C-RASP プログラムの自動検証と学習のための新たなアルゴリズム的手法を提示するものであり、Lustre モデル検査および局所探索との関連性を活用することで、トランスフォーマープログラムの最適化および制約付き学習への応用を可能にする。

原著者： Hongjian Jiang, Matthew Hague, Philipp Rümmer, Anthony Widjaja Lin

公開日 2026-05-19

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Hongjian Jiang, Matthew Hague, Philipp Rümmer, Anthony Widjaja Lin

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

非常に賢く強力なロボット（「トランスフォーマー」）が、物語を読み、メールを書き、パズルを解くことができると想像してください。このロボットは仕事において驚くほど優秀ですが、ある種の「ブラックボックス」でもあります。あなたが何をしているかは見えますが、それがどのように思考しているのか、あるいは特定の間違いを決して犯さないことを証明することは容易ではありません。

この論文は、これらのロボットを構築するための新しい設計図の作成方法を紹介します。ロボットの複雑で入り組んだ「脳」を直接理解しようとする代わりに、著者たちはC-RASPと呼ばれる、よりシンプルでクリーンな言語を作成しました。C-RASPは、ロボットが従う「簡素化された取扱説明書」と考えてください。それは私たちが読み、理解し、誤りをチェックするのに十分なほどシンプルでありながら、ロボットが何をしているかを正確に記述するのに十分なだけの強力さを持っています。

以下に、日常の比喩を用いて説明した、彼らの 2 つの主要な成果の概要を示します。

1. 「安全検査官」（検証）

問題点: あなたは C-RASP の取扱説明書（プログラム）を持っており、知りたいのは、「このプログラムは常に正しいことをしているか？悪い単語を受け入れたり、良い単語を拒絶したりすることはないか？」ということです。これを手動で確認するのは、100 万ページもの本からたった 1 つの誤字を見つけようとするようなもので、ほぼ不可能であり、数学的に 100% 確実であることは場合によっては不可能です。

解決策: 著者たちは「安全検査官」を構築しました。彼らは、これらの C-RASP の取扱説明書を、Lustreと呼ばれる非常に厳格な別の言語に変換する方法を考案しました。

比喩: 複雑なレシピが、乱雑な手書きのノート（C-RASP）に書かれていると想像してください。その計算が正しいかどうかは簡単に確認できません。そこで、その乱雑なレシピを、超高速ロボット（「モデルチェッカー」）が瞬時に読み取れる、厳格でコンピュータ可読な形式（Lustre）に変換します。
結果: このロボットはレシピを瞬時にスキャンし、「はい、これは安全です」と言うか、「いいえ、ここが間違ったステップです」と正確に指摘できます。この論文は、新しい AI ロボットを訓練するのに数時間かかるのに対し、この手法が数秒で機能することを示しています。

2. 「自動編集者」（合成）

問題点: 例のリスト（例えば、「これらは良い文、これらは悪い文」）があり、それらに合う C-RASP の取扱説明書を書きたいとします。あなたは取扱説明書を持っていません。ゼロからそれを発明しなければなりません。

解決策: 著者たちは、シミュレーテッド・アニーリングと呼ばれる技術を用いた「自動編集者」を作成しました。

比喩: ケーキの完璧な材料の組み合わせを見つけようとしているが、焼くまで味見ができないと想像してください。
1. 最初は、ランダムで乱雑なレシピから始めます。
2. それを焼いて、あなたの例と一致するか確認します。
3. 近い場合は、わずかな変更を加えます（砂糖を蜂蜜に交換する、塩をひとつまみ加えるなど）。
4. 新しいケーキが良ければ、それを採用します。悪ければ、後でより良いケーキにつながるかもしれないという可能性を考慮して、それでも採用するかもしれませんが、完璧なレシピに近づくにつれて、リスクを取ることは徐々に減らしていきます。
結果: このプロセスは、あなたの例に完璧に合う C-RASP プログラムを自動的に作成します。まるで、最終的な料理を味わうだけでレシピを逆引きできるシェフがいるようなものです。

なぜこれが重要なのか（論文によると）

著者たちは、これらのツールを、括弧のバランスが取れているか確認したり、文字を数えたりするといった様々な「パズル」でテストしました。

速度: これらのツールは、これらのパズルを数秒で解決しました。
比較: 彼らは、標準的な AI（GPT-2 など）をゼロからこれらの同じパズルを学習させるように訓練しようとすると、数時間かかり、それでも正解にたどり着けない可能性があることに言及しました。
2 つの素晴らしい用途:
1. 最小化: 巨大で肥大化した取扱説明書がある場合、そのツールは、まだ機能する最小かつ最もシンプルなバージョンに縮小できます。
2. 制約付き学習: プログラムが何をするべきかについての部分的なアイデア（「仕様」）がある場合、そのツールは空白を埋めて、最終的なプログラムがあなたの例とあなたの規則の両方に適合するようにします。

要約すると: この論文は、AI の謎めいた「ブラックボックス」を、明確で、検証可能で、編集可能な取扱説明書に変える方法を提供し、その安全性を検証し、以前よりもはるかに速く新しいものを作成することを可能にします。

技術的概要：トランスフォーマープログラムの合成と検証

問題定義

大規模言語モデル（LLM）の基盤アーキテクチャであるトランスフォーマーは、形式的に分析することが極めて困難であることで知られている。トランスフォーマーは表現力が高く並列化可能である一方、その性質の検証は決定不能であり、Chain of Thoughts（思考の連鎖）との組み合わせによりチューリング完全となる。この課題に対処するため、研究者たちはトランスフォーマーの振る舞いを正確な意味論で捉えるために、RASP（Restricted Access Sequence Processing Language）およびその変種である C-RASP（Counting RASP）のような宣言的言語を開発してきた。

しかし、C-RASP とトランスフォーマーの間の理論的つながりにもかかわらず、以下の 2 つの重要なギャップが残されている：

検証：C-RASP プログラムを自動的に検証する方法が存在しない。C-RASP が自明な言語を認識するかどうかの判定は、一般の場合において決定不能であり、言語の等価性や包含関係といった性質を分析する実用的なツールも存在しない。
合成：例から C-RASP プログラムを自動的に学習または合成する方法は知られていない。既存のアプローチはニューラルネットワークの訓練とルールの抽出に依存しており、実装可能な翻訳を生み出せない場合や、理想化された仮定を必要とする場合が多い。

本論文は、C-RASP プログラムの検証と合成の両方に対する最初の自動手法を開発することで、これらの課題に取り組む。

手法

1. Lustre への還元による検証

著者らは、C-RASP と埋め込みシステムで使用される同期データフロー言語であるLustreとの間の形式的なつながりを確立した。

翻訳：C-RASP プログラムは Lustre ノードに翻訳される。この翻訳は、C-RASP のルールを Lustre の変数（ブール値および整数のストリーム）にマッピングする。
- カウント演算子：C-RASP のカウント演算子 #φ（φ が成り立つ位置を数える）は、無限ストリームにわたって値を累積する補助的な整数変数を用いて Lustre でシミュレートされる。
- 有限と無限：C-RASP は有限語上で動作し、Lustre は無限ストリーム上で動作するため、入力は特定のストリーム終端マーカー（#）および永遠のマーカー（Ω）を持つ無限ストリームとして符号化される。
モデル検査：翻訳後、言語の等価性、包含関係、空性などの性質は、最適化された SMT ソルバー（CVC5、Z3）と連携する最先端のモデルチェッカー（具体的にはKind2）を用いて検証される。
複雑性：#rs,re 演算子内の範囲パラメータが単項符号で符号化されている場合、翻訳のサイズは多項式である。

2. シミュレーテッド・アニーリングによる合成

本論文は、正例と負例から C-RASP プログラムを合成するための、シミュレーテッド・アニーリングに基づく局所探索アルゴリズムを提案する。

状態空間：探索は、ブールルールの数（ $N_b$ ）、カウントルールの数（ $N_c$ ）、および数値定数の上限（ $K$ ）によって定義される固定された「プログラム形状」に制約される。
変換演算子：アルゴリズムは、現在のプログラムに対して構文変換を適用することで状態空間を探索する。これには以下が含まれる：
- リサンプリング：ルールの右辺を完全に置き換える。
- マイクロ変換：論理結合子の入れ替え、否定の切り替え、比較の厳密さの反転などの局所的な変更。
- 制約：変換は、単純で解釈可能なモデルへの探索を偏らせるため、浅い構文フラグメント（例えば、カウント式については深さ 2）に制限される。
目的関数：スコアリング関数 $E(P)$ は、誤分類の最小化（ $\lambda_{mis}$ ）を最優先し、次に到達不可能なルールのペナルティ（ $\lambda_U$ ）と抽象構文木全体のサイズ（ $\lambda_S$ ）をペナルティとする。
アニーリングのダイナミクス：アルゴリズムは、冷却スケジュールに依存する確率でより悪い解を受け入れることで、局所最適解から脱出することを可能にする。

3. 統合された応用

著者らは、これら 2 つのコンポーネントを統合し、以下の 2 つの応用をサポートする統一フレームワークを構築した：

トランスフォーマープログラムの最小化：C-RASP プログラムが与えられた場合、システムは構造的に小さく等価なプログラムを合成する。これは局所探索と等価性検査を交互に行い、検証器からの反例が探索を導く。
制約付き学習：部分仕様（C-RASP プログラム $P_{spec}$ ）とラベル付き例が与えられた場合、システムは例に適合し、かつ $P_{spec}$ の言語に含まれる（ $L(P) \subseteq L(P_{spec})$ ）プログラムを合成する。

主な貢献

最初の自動検証手法：本論文は、C-RASP プログラムを Lustre に還元しモデル検査を利用することで、C-RASP プログラムを自動的に検証する最初の手法を提示する。これにより、言語の等価性、包含関係、空性の検証が可能となる。
最初の自動合成手法：著者らは、中間的なニューラルネットワークの訓練を必要とせず、直接例から C-RASP プログラムを合成できる局所探索アルゴリズム（シミュレーテッド・アニーリング）を導入する。
実装とベンチマーク：統一された Scala ツールチェーンが実装され、文献からのベンチマークスイート（正規言語、カウントベースの言語、文脈自由言語風の言語を含む）に対して評価された。

実験結果

著者らは、Dyck-1、Majority、および各種 Tomita 自動機などの言語を含むベンチマークスイート上でツールを評価した。

効率性：ツールは、300 秒のタイムアウト内で、ほとんどのベンチマークに対して正しい C-RASP プログラムを正常に合成した。例えば、Dyck-1 のプログラム合成には約 3.92 秒、AnBnCn には 80.05 秒を要した。
精度：合成は、C-RASP の表現力内の言語に対して高い訓練精度および評価精度（しばしば 100%）を達成した。
トランスフォーマーとの比較：本論文は、特定のベンチマークにおいて、正しい言語を達成するためにトランスフォーマー（HuggingFace 経由の GPT-2 など）を訓練するには数時間を要する可能性があるのに対し、C-RASP 合成ツールは数秒でタスクを完了したと指摘している。
限界：表現力理論から予想される通り、C-RASP の能力を超える言語（Parity、Tomita 3、Tomita 5 など）は高い精度で学習できず、最良の訓練精度は 80% 未満に留まった。

意義と主張

本論文は、C-RASP を単にトランスフォーマーの表現力を理解するための理論的ツールとしてではなく、解釈可能な代理モデルとして位置づけている。検証と合成の自動手法を提供することで、著者らは C-RASP が形式的手法（FXAI）を用いて分析可能であり、ニューラルネットワークの「ブラックボックス」性と説明可能性の必要性との間のギャップを埋めると主張している。

その意義は以下の点にある：

実用的な決定可能性：一般的な検証は決定不能であるが、Lustre への還元は、特定の現実世界のトランスフォーマーの振る舞いを検証するための実用的かつ自動化された道筋を提供する。
直接合成：合成手法は、深層ニューラルネットワークの訓練の不安定性や不透明性を経ることなく、解釈可能なプログラムを生成する直接の経路を提供する。
最適化：既存のトランスフォーマープログラムを最小化し、制約の下で学習する能力は、プログラム改良や安全クリティカルな応用における C-RASP の有用性を示している。

著者らは、この研究がトランスフォーマーの形式的分析の基礎を築くものであり、将来の方向性には堅牢性の検証や Chain of Thoughts（CoT）メカニズムの組み込みが含まれると結論づけている。