LLMの指示追従におけるニューロ・シンボリック検証

TL;DR（結論）

大規模言語モデル（LLM）が複雑な指示を誤解したり無視したりする問題に対し、指示を制約充足問題（CSP）として定式化し、論理的および意味的な制約の両面から出力を厳密に検証する汎用フレームワーク「NSVIF」が開発されました。 本手法は、指示を1階述語論理の式に変換した上で、客観的な論理制約は自動生成されたPythonコードで、主観的な意味制約はLLMによる解析で個別に判定し、最終的にZ3ソルバーを用いて指示全体の整合性を数学的に検証する仕組みを持っています。 新たなベンチマーク「VIFBENCH」を用いた検証では、従来のLLMを直接評価者とする手法を大幅に上回る精度を達成し、違反箇所の特定といった解釈可能なフィードバックを提供することで、追加学習なしでLLMの指示追従能力を向上させることに成功しました。

なぜこの問題か

大規模言語モデル（LLM）を実世界の重要なアプリケーションに適用する際、モデルがユーザーの指示に完全に従わないという根本的な問題が大きな障壁となっています。LLMは指示の重要な部分を誤解したり、特定の制約を無視したりすることが頻繁に報告されており、これらの違反は一見しただけでは観察や確認が困難な場合が多いのが現状です。特に、複数のエージェントが連携するワークフローにおいては、一つのステップでの指示違反が推論チェーンを通じて伝播し、最終的にシステム全体の失敗や重大なインシデントを引き起こすリスクがあります。このような違反の連鎖は、システムの信頼性を著しく損なうだけでなく、どの段階で誰が失敗したのかという責任の所在を明らかにすることを困難にしています。 現在の一般的な対策として、別のLLMに判定を任せる「LLM-as-a-judge」という手法が広く用いられていますが、これは複雑な指示の検証においては信頼性が低いことが判明しています。…

核心：何を提案したのか

本論文では、LLMの出力が指示に従っているかを検証するためのニューロ・シンボリック・フレームワーク「NSVIF」を提案しています。このフレームワークの核心は、指示追従の検証を「制約充足問題（CSP）」として定式化することにあります。具体的には、ユーザーの指示を複数の独立した制約の集合として捉え、それらの関係を1階述語論理の数式モデルとして構築します。これにより、指示の検証は「出力が論理式を満たすかどうか」という数学的な問題に置き換えられ、従来の曖昧な評価から脱却することが可能になりました。 NSVIFは、制約を「論理制約」と「意味制約」の2つのカテゴリに分類して処理する「分割統治」戦略を採用しています。論理制約は、語彙、フォーマット、構造、順序などの客観的なルールを指し、これらはシンボリックな推論や実行可能なコードによって厳密に検証されます。…

続きはログイン/プランで閲覧できます。