LLMの中にいろんなものを埋め込もうとしたが無理があった話

Qwenputer

先週くらいですかね、SNSで話題になっていたQwenputerのことを書きたいと思います。

これはなんとQwen3.5-4Bのモデル内部に、32ビットのRISC-V CPUを組み込んでしまったというのです。まあ、最初は「LLMがCPUの動きを模倣するように学習したのか？」みたいなレベルの話かなって思ったんですが、そうではなくて、モデルの内部に、CPUとして動作する計算回路そのものを構築しているっぽいです。

既存のQwen3.5-4B（32層）の前に11層を追加し、その重みを機械学習ではなくコンパイラで計算して直接設定するというアプローチをとっているらしいです。「レジスタを読む」「足し算をする」「条件分岐する」といったCPUの基本動作を、Transformerの演算として表現しているわけです。メモリの扱いも面白い。Qwen3.5が持つGated DeltaNetの状態空間を、アドレス指定で読み書きできるRAMとして活用しています。これにより、プログラムカウンタやレジスタ、データなどをモデル内部に保持できるようになっています。控えめに言って頭がおかしいですね。

開発者の技術解説によると、組み込まれたCPUはRISC-Vの公式テストに合格しており、C言語やMicroPythonのプログラムも動かせるとのことです。参照実装と約23万箇所の出力を照合したテストでも、不一致はゼロだったとのこと。計算のベンチマーク結果もありますね。たとえば大きな整数の掛け算では、通常のQwen3.5-4Bの正答率が55%だったのに対し、Qwenputerは97.5%だとか言ってます。まあ40問くらいらしいですが十分インパクトありますね。

頭がおかしいというのはもちろん誉め言葉なんですが、実用的かというとそんなことはない。モデルサイズは約18.8GBと肥大化してるし、通常のCPUで計算するより圧倒的に遅いです。単に四則演算を正確にやりたいだけなら、LLMから外部のPythonを呼び出したほうがずっと手軽で高速でしょう。

では、この研究の何がそんなに面白いのかというとですね、 「LLMの重みが、学習した知識を蓄える場所だけでなく、決定論的な回路を埋め込める」 ってことです。LLMの推論や文章生成は確率的であり、同じ質問でも毎回違う答えが返ってきますね。一方で、内部に追加された回路は、定義された演算を決められた手順通りに実行します。この「確率的な推論」と「決定論的な処理」を、同じモデルの中に同居させられるのが面白い。

LLMのガードレールへの応用

LLMを業務システムやAIエージェントに組み込むときに毎回話に出るのは「絶対にやってはいけないことをどう守らせるか」という問題です。たとえば、「管理者の承認なしにデータを削除しない」「他部署の情報にはアクセスしない」「上限金額を超える発注は行わない」といった業務ルールです。

これらをシステムプロンプトに書いておくことはできます。しかし、プロンプトはあくまでLLMへのお願いに過ぎず、厳密な権限管理の仕組みではありません。文脈の読み違いやプロンプトインジェクションによって、望ましくない操作を実行しようとするリスクはどうしても残ります。

確率的なものだから当然そうなるんですが……これ、決定論的に禁止できるならどうだろう、って思いますよね。で、調べてみたら実はQwenputerの開発者は、CPUの次に、監視機構をモデルの重みに直接埋め込むという実験をもうやってます（Building oversight tools into a model's weights）。

この実験では、モデルの内部状態から「これから嘘をつこうとしている兆候」を検出する線形プローブ（検出器）を作り、それに反応するトリガーとログ記録の仕組みを重みに組み込みました。開発者の評価によると、嘘の91%を検出でき、通常の会話など約2万8,000トークンのテストでは誤検知がゼロだったうえに、プロンプトで「監視を止めろ」と指示しても、重みに組み込まれた監視回路自体は止まりませんでした。

まあ嘘かどうかというのは割と主観的な側面でもあるのでどこまでいっても100%にはならないんじゃないかと思うのですけど、検出率91%はなかなかすごくないですか。まあ、この実験で実証されたのは「監視とログ記録」までであり、危険な出力を自動で完全に遮断する仕組ってわけではないですが……。 でも モデルの内部状態を監視する回路を、プロンプトの指示とは切り離して独立に動かせる ことを示した点はかなり面白いなって思います。

ガードレールを二層に分けて考える

この考え方を整理すると、AIシステムのガードレールは次の二層に分けて設計するのがよさそうです。

第1層はいままでのガードレールに近いですね。自然言語の微妙なニュアンスや文脈を扱ってある程度防ぐ感じです。逆に第2層は、あらかじめ定義されていない未知のリスクを見つけるのは苦手ですが、明文化されたルールを100%通りに強制することができます。AIエージェントがAPIを操作する場面なら、こんな感じ。

文字がでかいな。そんな大声でいうことじゃないぞ。

それはさておき、第2層の判定をLLM自身の自己申告に任せちゃうと結局は確率論になっちゃうので、そこはやっちゃダメってことが大事です。独立した決定論的な回路の判定結果によって、実際の操作を実行するかどうかを制御するわけですね。

結局はモデルの外で止めたほうがいい

まあ、ガードレール込みでモデルを配布できるという意味では面白いんですが、結局のところ実務システムとして考えるなら、第2層の決定論的なガードレールはモデルの「外」に置くほうがやっぱり合理的なんですよねー。外部のポリシーエンジンやAPIゲートウェイとして実装すれば、モデル自体を改造せずに導入できるし、異なるモデルに同じルールを適用できますし、社内の権限データベースや承認ワークフローとの連携も簡単です。

まあ、さっきの実験のように「モデル内部の活性値（これから嘘をつこうとしている兆候など）を直接観測できる」というのは、モデル内部の回路ならではの強みなんでこれはこれでやったほうがいいなと思うんですが、結局のところ、内と外のハイブリットになるのかなと思います。こんな感じ。

だから文字がでかいって。

しかしまあ、これあんまりおもしろくはない結論ですね。せっかく中で検証できると思ったのにな。

Anthropicの形式検証

そーいえば、決定論的な検証ってなんか、Anthropicが最近やってなかったっけ、っと思って思い出したのが、10/22に公開された形式検証（Formal Verification）の研究です。

これが何かって言うとですね。「プログラムの振る舞いが数学的に記述された仕様を満たしていることを厳密に証明する手法」ですね。通常のテストって「試した入力では問題がなかった」をたくさんやって確認することしかできないんだけど、形式検証は 「一定の前提条件のもとで、起こり得るすべての入力に対して指定した性質が成り立つ」 ことを保証できるんですよね（あ、ちなみに形式検証はバグがないプログラムを保証してるわけではないので夢の技法ではないんですよね、残念）。

数学的な証明を書く作業は非常にコストが高くて、これまで一部の重要なシステムにしか使われてきませんでした（そうだったのか。知ららんかった）。AnthropicはそいつをLLMによって大規模に進められるということを言ってます。Claudeがプログラムを解析し、必要ならバグを修正したうえで、形式的な証明コードを生成。「その証明が正しいかどうか」はClaude自身ではなく、Rocq（旧Coq）という証明チェッカーが機械的に判定 するとのこと。実際に123のオープンソースライブラリに含まれる239のエントリーポイントについて、「64MB未満の入力でクラッシュしないこと」などを形式的に証明できたと言ってます。よくわからないけど、たぶんすごいです。

このアプローチで面白いのは、「LLMが書く証明そのものは、途中で間違っていても構わない」 という割り切りです。

これは文字がでかくても重要だから許します。

ちなみに、証明が通らなくても、ただちにプログラムが間違っているとは限りません。単に証明の書き方が不十分なだけかもしれないですからね。でも、証明チェッカーを通過していないものは、保証済みとして扱わない というルールを徹底することはできます。

検証器をどこに置くか

話がようやく戻ってきました。さて、このAnthropicの研究ですが、こいつとQwenputerをかけあわせたら小型の形式検証器やチェッカーを、学習とは切り離された決定論的な回路としてモデル内部に組み込むとかできないんかなと思ったんですよね。

そんなわけでGPT Solさんに聞いてみたんですが、

Qwenputerは、まさにそうした回路を重みに実装する技術的な入り口を示しているが、実用システムにおいては、やはり当面は証明チェッカーをモデルの外部に置くほうが合理的。現時点でQwenputer上にRocqのような本格的な証明チェッカーは載っていない。現在のモデル内CPUは計算速度やメモリの面で大きな制約がある。たとえ回路が決定論的であっても、検証器自体の実装バグや計算モデルの前提条件、検証結果をバイパスさせない出力制御など、クリアすべき課題がおおい。

さすがにハードルがありすぎる感じですかそうですか……。

数理最適化に組み合わせたらどうなるか？

話がどんどん飛びます。次に思ったのは最近ゼンクでやってる 数理最適化（とりわけ量子アニーリングなど）への応用 です。

いまぼくたちが取り組んでる量子技術を使った最適化ではこんなことをよく言います「LLMでは制約を絶対守ることができず、破った解を出してきてしまう。数理最適化は違う。制約を守った解を得ることができる」だから「説明できる解を得られる」ってロジックなんです。

じゃあ、さっきの技術で決定論的に制約を守らせることができるLLMってつくれるんじゃない？　って思いませんか。

LLMの場合、そもそも最適解の保証はないです。ただこれって量子技術でも実は変わりません。実務で数理最適化や量子アニーリングを扱う場合、計算時間や問題規模の制約から、「実務上十分に良い解」しか得られないときってそれなりにあるわけです。だからそっちはLLMでも量子最適化でも同じなんですよ。なので問題は制約、とりわけハード制約のほうです（ソフト制約は結局ペナルティ項目に入れるので破ることがあります）。

探索と検証を完全に切り離す

ここで、これまでのガードレールや形式検証とまったく同じ構造が使えます。解の探索と、制約の検証を切り離す。

たとえば配送経路最適化（CVRP）なら、LLMが配送エリアの分割や探索の戦略を立て、ソルバーが具体的なルート候補を高速に探索します。そして最後に、独立した決定論的チェッカーが「すべての顧客を訪問しているか」「各車両の積載量を超えていないか」「発着点が正しいか」をチェック。

これはまさにNP問題ってやつです。これは「問題そのものを解くのは非常に難しいが、提示された候補が正しいかどうかのチェックは簡単という問題」です。

計算時間の上限が来たら、その時点までにチェックを通過した候補の中から最もスコアの良いものを返せばよいのです。もし1つも見つからなければ、正直に「時間内に実行可能な解が見つかりませんでした」と返します。制約違反の解を黙って現場に渡してしまう事態は、これで確実に防げますね。

LLM自身が量子アニーリングや既存の最適化ソルバーに計算力で勝つ必要がないように、こんなふうにするとよさそうですね。データサイエンティストがいまはやってる「問題をどう小さく分割するか」「どのソルバーに投げるか」「制約違反が起きたときにどう初期解を修正するか」みたいなことをLLMが担当し、計算をソルバーが行って、決定論的なチェッカーが厳格にチェックする………

あれ、これ別にモデル内部にCPUを埋め込む必要ない。

うーん、決定論はどこに行ったんだ。

これは ただのデータサイエンティストエージェント じゃないか……。

ガードレールと形式検証につづいてこのスジもだめっぽいです。

面白くもないまとめ

というわけで。

今回、Qwenputerから始まっていくつかの研究や応用分野を思い付きでつなげてみたんですけど、結局のところ、まとめると

「LLMそのものを無理に決定論的にせず、LLMの非決定性が、安全上のルール違反に直結しないシステム構造を作ればよい」

になります。これはようするにハーネスでやれってことで、いままでやってきたことと何も変わりません。さんざん新しい技術に興奮して考えた結果がこれです。面白くないなー。面白くはないんですが、まあ、そんな簡単にブレイクスルーがおきたりするわけじゃないってことですね。

ChatGPT はぼくがいろいろ聞いたら最後はこんなこといってました。

Qwenputerは、今すぐ実務に投入するためのCPU内蔵モデルという以上に、そうしたAIシステムの設計思想を改めて考えさせてくれる面白い研究でした。Anthropicの形式検証や量子最適化と重ね合わせて見ることで、単なる奇抜な実験を超えた、これからのAIアーキテクチャのヒントが見えてくる気がします。

やかましいよ。

ではまた。