型制約付きコード生成と言語モデル

377日前原文(arxiv.org)

概要

LLMによるコード生成は進歩しているが、 型エラー などで コンパイル不可 な出力が多い。
既存の 制約付きデコーディング は主に構文やドメイン固有言語に限定。
本研究は 型システム を活用した新しい 型制約付きデコーディング を提案。
提案手法は prefix automata と型探索を利用し、 TypeScript でも実装・評価。
HumanEvalやMBPPでの実験により、 コンパイルエラー半減 ・ 機能的正確性向上 を確認。

型制約付きデコーディングによるLLMコード生成の高信頼化

背景と課題認識

大規模言語モデル（LLMs） はコード生成で顕著な成果を示すことが可能。
しかし、 次トークン推論 はコードの形式的側面を十分に扱えず、 コンパイル不可なコード を頻繁に生成する傾向。
制約付きデコーディング は有望な手法だが、これまで構文や ドメイン固有言語 への適用に留まっていたことを確認。
- 型エラーは構文エラーと異なり、 制約化が困難 である点を問題視。

本研究の提案内容

型システム を活用し、LLMによるコード生成を 型安全 に誘導する 型制約付きデコーディング 手法を提案。
prefix automata（接頭辞オートマトン） と inhabitable types（充足可能型）探索 を組み合わせ、 型整合性 を保証する仕組みを構築すること。
提案手法を simply-typed language で理論的に定式化し、 TypeScript への拡張も実施すること。

実験と評価

HumanEval および MBPP データセットを用いて、提案手法の 有効性 を検証すること。
- コード合成、翻訳、修復タスクで コンパイルエラー率を半減 させることに成功。
- 機能的正確性も大幅に向上することを確認。
- 30Bパラメータ超 の最先端モデルを含む 多様なLLMファミリー で効果を確認。

意義と今後の展望

型システムの形式的ルール によって、LLMのコード生成に 高い信頼性 と 汎用性 を付与できることを示す提案。
今後のLLMコード生成技術の 品質向上 や 実用化 に向けた基盤技術として期待されることを強調。

提案

LLMコード生成における 型制約の導入 を推進すること。
prefix automata および型探索の技術応用を拡大すること。
実運用環境での 型安全性検証 を強化すること。

Hackerたちの意見

これは明らかに次のステップだね。今の製品は、せいぜい有効なJSONや特定のJSONスキーマにトークン予測を制限することしかできない。制約付き出力モードでこれだけが唯一の文法である必要はないよね。本当の課題は、自動で言語を検出して切り替えることになると思う。例えば、コードのスニペットにコメントとしてLaTeXの数式が含まれていて、文字列リテラルにSQLがあるみたいな感じ。シェルスクリプト内の正規表現など、もっとたくさんの例があるよね。その次の明らかなステップはバックトラッキングだと思う。正しいトークンを出力することは可能だけど、その後有効な補完ができなくなることもある。つまり、モデルが自分を追い詰めることができるってこと。私の知る限り、現在のオンラインLLMサービスでバックトラッキングを使っているものはないし、みんな前に進むモード（"forwards"）だけで動いてる。

└

バックトラッキングのアイデアは面白いね、もしかして拡散（diffusion）が助けになるかも？ある時点でSATソルビングに変わるけど。

└

マイクロソフトが君が提案しているようなバックトラッキングを行うフレームワークを導入したと思うけど、どれだけ注目されたかはわからないな。

└

SRLCG: 多次元思考と動的バックトラッキングを用いた自己修正型大規模コード生成 https://arxiv.org/abs/2504.00532 IterGen: バックトラッキングを用いた反復的セマンティック対応構造LLM生成 https://arxiv.org/abs/2410.07295 ROCODE: コード生成のための大規模言語モデルにおけるバックトラッキングメカニズムとプログラム分析の統合 https://arxiv.org/abs/2411.07112v1

└

言語の検出と切り替えについて：いくつかの制約システムを並行して実行して、どれかが入力を拒否したら、別のが受け入れるまで切り替えるって手もあるよ。この論文の核心部分はプレフィックスプロパティを確保することなんだ。つまり、常に正当な完了があって、モデルが「コーナー」に追い込まれないようにすること！どんな言語や言語機能にこのプレフィックスプロパティが保証できるか、研究が必要だね。

TypeScriptはLLMにとって最適な言語になるポジションにいると思う。たくさんのトレーニングデータ（JSの例も活用できるし）に加えて、LLMが従うべき型の構造や、それを強制するツールもあるからね。

└

神様、助けてくれ…

└

KotlinやRust、Haskellみたいに、TypeScriptよりもずっと厳しく型を制約する言語もあるよね。型が厳しければ厳しいほど、プログラムが正しくなる可能性が高くなる。

└

LLMはどんな静的解析ツールとも相性がいいよ。Claudeに「go vet」や「deadcode」みたいなことを使わせることがよくあるんだけど、そうすると、壊れたゴミみたいなコードを書きまくって「ミッション完了！」って言うんだよね。

└

これがジョークであってほしいのは俺だけじゃないよね。

└

確かに良くなってるけど、パワーTSユーザーとしては、まだコード生成がイマイチだし、ジェネリクスで失敗したり（使わなかったり）単純な型でもたまにおかしくなることがあるよ。

└

完全に同意！$20/月のCursorプランの基本的なLLMでも、TypeScriptのコードベースではそれ以外の時より10倍速く作業できるし、Pythonだとその倍数は2-3倍くらいに感じる。特に、よく整理された型システムがあるとオートコンプリートがすごいよね。それに、隣のコメントに対する返事として、多くの重要なTSコードベースではeslintで明示的な「any」の使用を無効にするんだよね - https://typescript-eslint.io/rules/no-explicit-any/。

└

同意する人は、Anders Hejlsbergらによる「Introducing TypeChat」（2023）に興味があるかもね：[1] [1]: https://microsoft.github.io/TypeChat/blog/introducing-typech...

└

他の多くの言語とは違って、TypeScriptの型は非常に表現力豊かなんだよね。例えば、APIから受け取ったスネークケースのキーを持つオブジェクトを引数に取って、そのオブジェクトをキャメルケースのキーに変換して返す関数を書けるんだ。これはTypeScriptコンパイラの「特別なケース」じゃなくて、TypeScriptの機能から自然に出てくる能力なんだよ。他にこんなことができる言語は知らないな。ほとんどの人はこれを効果的に使うほどのTypeScriptの知識がないけど、LLMを訓練すればこれにすごく強くなると思う。LLMがそんな高度な制約を自分に課して、それに基づいてコードを生成するっていう組み合わせは、めちゃくちゃ強力に感じる。

└

たくさんのトレーニングデータ（JSの例も活用してるし）多いことが必ずしも良いとは限らないよ。

└

Scalaはその型システムが正式にモデル化されているから、最適だと思うよ。https://infoscience.epfl.ch/entities/publication/6c6bb09d-a4...

ヘイルズバーグは、LLMに迅速に正確な型情報を提供できる能力が、tscをGoに書き直す理由の一つだと言ってたよね。https://youtu.be/10qowKUW82U?t=3186

└

でもTypeScriptって最初から型付き言語じゃないの？

コードはここにあるよ: https://github.com/eth-sri/type-constrained-code-generation

本当にすごい結果だね！この研究が大学から出てきたっていうのが、AIの大手ラボがまだ大きなモデルが必要だと思ってるってことを示してる気がする。

└

+1 これは健全な発展に見えるね。

└

ありがとう！

これを正しくやるには有限モデル理論を使うのが正解だけど、まだそこには到達してないね。

MultiLSPyもチェックする価値ありだよ、複数のLSPをラップするPythonのラッパーみたいなものだね：https://github.com/microsoft/multilspy いくつかの似たような出版物でも使われていて、「モニターを使ってグローバルコンテキストでコードの言語モデルをガイドする」っていう論文（https://arxiv.org/abs/2306.10763）でも使われてる。これは型システムを超えた静的解析を使って、無効な変数名や無効な制御フローをフィルタリングするんだ。

└

この研究もめっちゃクールだよ！LSPは、プレフィックスプロパティを確保するために必要な型を解決することを保証できないことに注意してね。これを利用してバックトラッキングや生成ループを避けてるんだ。

私たち（.txt、アウトラインの人たち）は、この論文についてTwitterでちょっとしたスレッドをやったよ、興味があれば見てみてね： https://x.com/dottxtai/status/1922322194379551128

小さなAIラボだったら、これをやるのがいいと思う。すべてのベンチマークを超えるフロンティアLLMを作ろうとするんじゃなくて、1つのプログラミング言語で世界最高のLLMを作ることを目指そう。RLパイプラインを作って、その言語でLLMを最高にするためにすべてのリソースを投入するんだ。もしGitHubに人間が作ったトレーニングデータが少ないなら、さらに良いね。競合他社はそれが苦手になるから。Googleは最近のGemini-2.5 ProリリースでJavaScriptでこれをある程度やったけど、もっと小さな言語でやるのはどう？Googleはそれをやらないだろうけど、需要はまだたくさんあるよ。

└

一つのプログラミング言語に特化するのは理にかなってるけど、その一つのドメインにLLMの知的スペースを全部捧げるっていうのは、逆に言うと、間違ったプログラミング言語でもトレーニングデータが多ければLLMの鋭さや推論能力がどれだけ上がるのか気になるな。開発者としては、特定の言語のプログラミングスキルは他の言語を知ることで向上したと思うし、対比して比較できるからね。

└

これは悪いアイデアだとは言わないけど、かなりリスクのある提案に聞こえるね。要するに、LLMがプログラミング言語を横断して一般化する能力や、構文以上の深いレベルで概念を埋め込む能力に賭けているわけだ。多くの人がそう思ってるけど、AIラボを運営してる人がどれだけいるかは分からないな。

└

LLMにとって言語自体を使うことは挑戦じゃないんだよ、彼らはそれを非常に高い成功率でやってるからね。数ヶ月間、LLMが構文エラーを出すのを見たことがないよ。正しいパラメータで正しい関数を呼ぶことが、君の仮想のAIラボが解決しなきゃいけない課題なんだ（それを手抜きして素晴らしいベンチマーク結果を出すかもしれないけど）。

この論文の著者として、ここでの素晴らしい議論を見られてとても興奮してるよ！何人かの人が生成 - コンパイル - 修正ループについて言及してたね。私たちのアプローチは生成ステップだけでなく、修正ステップにも効果があることを思い出してほしいな。修正は本質的にLLMにコードの新しいバージョンを生成させることだからね。実際に論文には「修理」の実験があって、私たちのアプローチはこの実験でかなりの成果を上げてるんだ、つまり機能的正確性で37%の相対的改善を達成してるよ。

└

研究してくれてありがとう、本当に素晴らしい仕事だね！

└

37%の増加って、何に対しての話？生成された関数のうち、どれくらいが間違ってたの？

ハクソク