制約充足問題における形式化者としての言語モデルの現実検証

arXiv cs.CL / 2026/4/1

💬 オピニオンIdeas & Deep AnalysisModels & Research

共有:

要点

本論文は、大規模言語モデルを「形式化者」（問題文を外部ソルバ向けの形式的なプログラムに変換する）として用いた場合に、実世界の制約充足問題で性能が確実に向上するかどうかを評価する。
4つのベンチマーク、6つのLLM、2種類の形式言語にわたって、LLM-as-formalizer（形式化者としてのLLM）は、24のモデル–データセット組み合わせのうち15件でLLM-as-solver（ソルバとしてのLLM）を下回り、高い検証可能性や解釈可能性があっても、単に課題を自明化するわけではないことを示している。
形式化の探索空間はエンドツーエンドのソルバ探索空間よりはるかに小さいにもかかわらず、スケーリング分析では、LLM-as-formalizerの性能が問題の複雑さの増大に伴って急激に低下し、ソルバ型のアプローチと同様の傾向が見られる。
著者らは重要な限界を特定している。すなわち、モデルが過度な「ソルバのような」推論トークンを生成したり、解を強く埋め込む（ハードコードする）ことさえあるためであり、これらの失敗モードに将来の形式化手法が対処する必要があることを示唆している。

概要: 近年の研究では、記号推論の問題において、エンドツーエンドの解法器としてではなく形式化器として大規模言語モデル（LLM）を用いることで、より優れた性能が得られることが示されています。問題の記述が与えられると、LLMは外部のソルバを介して解を導く形式的プログラムを生成します。私たちは、4つのベンチマーク、6つのLLM、2種類の形式言語にわたる実世界の制約充足問題に対して、LLMの形式化能力を体系的に調査します。その結果、LLM-as-formalizerは決して問題を単純化するものではない一方で、前者の検証可能性と解釈可能性があるにもかかわらず、24のモデル-データセットの組み合わせのうち15の場合でLLM-as-solverよりも性能が劣ることを示します。形式化空間は探索空間より桁違いに小さいものの、スケーリング分析により、LLM-as-formalizerは問題の複雑さが増すにつれて、LLM-as-solverと同様に依然として大きく劣化することが分かりました。この制約をよりよく理解するために、過剰でソルバのような推論トークンが観測され、それが時にハードコードされた解につながることがある点に着目します。これは、LLMベースの形式化を改善するための重要な課題を浮き彫りにしています。