4月21日、Bruno Gavranovic氏が「Types and Neural Networks」と題した記事を公開した。
GPT-4は1.8兆のパラメータを持つ巨大モデルだが、チェスでは中級者レベル（1371 ELO）にとどまる。一方、わずか6000万パラメータのAlphaZeroは超人的な強さ（3400+ ELO）を誇る。この30倍の性能差の秘密は構造を学習プロセスに組み込むかどうかにある。同じ問題が、現在のLLMによる型付きコード生成でも起きているというのだ。
なぜLLMは型付きコードが苦手なのか
GitHub Copilotの普及やOpenAI o1の登場により、AI支援プログラミングは現実的になった。しかし、Lean、Agda、Idrisといった依存型を持つ言語や定理証明器での生成品質は依然として課題だ。
その原因は、LLMの根本的な設計にある。現在のLLMは本質的に以下の型を持つ関数だ：
LLM : List Token -> D (List Token)
つまり、トークン列を受け取り、トークン列の分布を返すだけ。型チェックは生成後の後処理として別途実行される。これは、構造化されたプログラムを生成したいのに、その構造を学習から完全に切り離していることを意味する。
既存手法の2つの限界
現在、型付きコードの生成には主に2つの手法が使われているが、どちらも根本的な欠陥がある。
1. Try-Compile-Repeat（試行錯誤型）
モデルがコードを生成し、コンパイルエラーが出れば再生成を試みる手法。人間のプログラマーも実際にやっている方法だが、効率が悪い。
例えばEither Char Double型の値を生成する際、モデルが"[ 1 , 2"で始めた場合を考えよう。この型では[で始まる値は存在しないため、最初のトークン時点で回復不可能だ。しかし完全な生成が終わるまでエラーに気づかない。
2. Constrained Decoding（制約付きデコーディング）
各トークン生成前に型チェッカーに相談し、型エラーを引き起こすトークンをマスクする手法。GuidanceやOutlinesといったライブラリで実装されている。
型チェックは保証されるが、重要な欠陥がある：モデルが何を言いたがっているかは変わらないのだ。モデルがアルファベット文字に高確率を割り当てているのに、それらがマスクされると低確率のトークンからサンプリングせざるを得ない。結果として型チェックは通るが意味不明な出力が生成されがちだ。
AlphaZeroが示す「構造の力」
ここで冒頭のチェスの例に戻ろう。なぜAlphaZeroは30分の1のパラメータでGPT-4を圧倒できるのか。
GPT-4は大規模言語モデル訓練の副産物として約1371 ELOに到達し、30%のゲームで違法な手を打つ。一方、ゲーム構造を訓練時に活用するAlphaZeroは、違法な手を一度も打たずに超人的な強さに到達する。
重要なのは、構造を後から制約として加えるのではなく、学習プロセス自体に組み込むことの威力だ。これはリッチ・サットンの苦い教訓（Bitter Lesson）に反するものではない。むしろスケールを適切なオブジェクトに対して機能させるための基盤として働く。
新手法：「構造に関する微分」の実用的意味
記事の核心は、型付き出力を生成する2つの根本的に異なるアプローチの区別にある。
従来のアプローチ（構造を通じた微分）では、プログラマーが入力空間の分割を事前に決める。Either a b型の値を生成する場合、以下のような固定的な構造になる：
f (x, p) = if c (x, p) then Left (f_l (x, p))
else Right (f_r (x, p))
モデルが間違った分岐を選んだ場合、勾配更新で修正できない構造的な問題がある。
新しいアプローチ（構造に関する微分）では、3つの微分可能な写像を用いる：
f_c : X × P -> D(Bool)- 選択の分布を生成f_A : X × P -> A- A型の値を生成f_B : X × P -> B- B型の値を生成
離散的な選択を通じて微分するのではなく、各選択の証拠を収集し、正規化してからサンプリングする。これにより、ネットワークは適切な出力型を学習できるようになる。
実用的な観点から言えば、この手法により以下が期待できる：
- 型エラーの大幅な削減：構造が学習に組み込まれるため、型に適合する出力の生成精度が向上
- 効率的な学習：Try-Compile-Repeatのような非効率な試行錯誤が不要
- 意味のある出力：Constrained Decodingで起きがちな「型は通るが無意味」な出力を回避
型理論との深い関係
これらの型付きアクション空間を統一的に記述する数学的言語は、コンテナ（containers）と依存レンズ（dependent lenses）の理論に帰着するという。
特に、プログラミング言語の構造が豊かであるほど、この手法の恩恵は大きくなる。Haskellのような高階関数型言語や、Coqのような定理証明器での応用が期待される分野だ。
型レベルの選択を固定された足場ではなく、ネットワークが学習できるものとして扱うという発想の転換が、この研究分野の核心となる。両方のアプローチとも型付きの出力を生成するが、後者のみが出力の詳細を学習可能にするのだ。
詳細はTypes and Neural Networksを参照していただきたい。
