AI 2026年4月21日

LLMに「型」を教えるとはどういうことか——型システムとニューラルネットワークの未解決問題

LLMはコードを「型なし」で吐き出している

LLMがコードを生成するとき、その内部では何が起きているか。答えはシンプルで、次のトークンを確率的に予測しているだけだ。出力の型は LLM : List Token -> D(List Token)、つまり「トークン列を受け取って、トークン列の分布を返す関数」に過ぎない。

型付き言語——IdrisやLean、Agdaといった、証明可能な正しさを志向するプログラミング言語——のコードをLLMが生成するとき、そこには根本的な断絶がある。型チェックと学習が完全に切り離されているのだ。

Bruno Gavranovic氏がGLAIVEブログに寄稿した記事「Types and Neural Networks」は、この断絶をどう埋めるかを正面から論じている。読んでいて「そうか、これはまだ誰も解いていない問題なんだ」と気づかされる内容だった。

現状の2つのアプローチと、その本質的な欠陥

型付き出力をLLMから得るための方法は、現在2つある。

1. 試行・コンパイル・エラー時再試行（Try; Compile; If Error Repeat）

文字通り、モデルに出力させて、型チェッカーに通して、エラーが出たらフィードバックして再生成させる。人間のプログラマーがやっていることをそのままループ化したものだ。

このアプローチの問題は「遅さ」ではなく「無駄」にある。たとえば Either Char Double 型の値を生成させるとき、モデルが [ 1 , 2 と書き始めた時点でもう詰んでいる。この型は [ で始まれないからだ。しかし型チェッカーは最後まで待ってから「NG」と言う。そして次のセッションでもモデルは同じ重みから始まる——何も学習していないから。

2. 制約付きデコーディング（Constrained Decoding）

こちらはトークンを1つ生成するたびに型チェッカーを呼び出し、型的に不正なトークンをマスクする方法だ。JSONスキーマや限定的な型システムへの適用事例がすでにある。

出力は必ず型チェックを通過する。だがここに落とし穴がある。マスクはモデルが「言いたいこと」を変えない。モデルがアルファベットに高い確率を割り当てていても、マスクが強制的にそれをゼロにする。結果として、モデルにとって低確率な選択肢だけが残り、型は正しいが意味をなさない出力が生まれる。そしてこちらも、マスクを通じて勾配は流れない。モデルは学習できない。

要するに、どちらも「訓練済みネットワークを固定したまま後から辻褄を合わせる」アプローチだ。

それでも性能は上がっている——だからこそ問題が見えにくい

奇妙なことに、この「型なし訓練」でもフロンティアモデルは着実に進化している。

記事が引用する数字が興味深い。FrontierMathのスコアはリリース時の2%未満から、2年以内に約50%に達した。ARC-AGI-2やSWE-benchも同様のトレンドを示す。チェスではGPT-4がELO約1371（中級プレイヤー相当）に達している。これは一般的な訓練の副産物として出てきたスコアだ。

ただし、ここで比較すべき数字がある。AlphaZeroだ。

AlphaZeroはゲームの構造（ルール）を訓練に統合している。その結果、超人的なELO（3400超）に達する。GPT-4のパラメータ数が約1.8兆に対して、AlphaZeroは6000万未満——30倍以上少ないパラメータで、だ。そしてAlphaZeroは違法な手を一切指さない。GPT-4は30%のゲームで違法な手を指す。

この対比が示すのは、「ルールを知らないままゲームをプレイしている」状態と「ルールを訓練に組み込んだ」状態の差だ。