ハクソク

世界を動かす技術を、日本語で。

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

2025年5月14日原文(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コード生成技術の 品質向上 や 実用化 に向けた基盤技術として期待されることを強調。

関連情報

  • 論文情報：arXiv:2504.09246 [cs.LG]、DOI: https://doi.org/10.48550/arXiv.2504.09246
  • 著者：Niels Mündler
  • データセット：HumanEval, MBPP
  • 対象言語：simply-typed language, TypeScript

提案

  • 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/。

Hacker Newsで議論の続きを見る