Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability

技術的サマリー：選好に基づく最大充足可能性問題を用いた大規模言語モデルによる信頼性の高い推論

問題定義

大規模言語モデル（LLM）は自然言語理解やコード生成において強力な能力を示す一方で、複数の制約とユーザー定義の選好を伴う複雑な最適化問題が課された場合、著しい信頼性の欠如を露呈する。ロボット工学や物流など、正しさおよび証明可能な最適性が不可欠な領域において、LLM は内部推論（例：思考の連鎖）や直接回答生成のみに依存する場合、硬制約を満たすこと、または目的関数を最小化することができず、失敗することが多い。これらの失敗は、最適化問題の組み合わせ的な性質と、LLM が厳密な推論を行う能力の欠如に起因し、検証が困難な実行不可能または非最適の解をもたらす。さらに、最大充足可能性問題（MaxSAT）のような既存の形式手法は、ユーザーが選好を PDDL などの専門的で硬直的な言語で表現することを要求しており、非専門家にとって参入障壁となっている。

手法

本論文は、推論を LLM から形式ソルバーへ外部化するハイブリッドな神経記号アプローチを提案する。この中核となるパラダイムは「vibe coding」と呼ばれ、LLM が自然言語による問題記述を実行可能な Python コードに変換し、それを正確な MaxSAT ソルバーによって解くというものである。

提案されたパイプラインは、以下の段階から構成される：

1. 中間計画：コード生成前に、LLM に意思決定変数、硬制約、および軟選好の構造化された記号的記述を生成させるようプロンプトする。このステップは、問題の体系的な分解を強制することで、モデルリングの精度を向上させることを目的とする。
2. コード生成：LLM は PySAT API を用いて Python コードを生成し、問題を重み付き部分 MaxSAT インスタンスとして符号化する。硬制約は硬節として、ユーザー選好は重み付き軟節として符号化される。
3. MaxSAT 求解：生成されたコードを実行し、MaxSAT ソルバー（具体的には PySAT の RC2）を呼び出す。ソルバーは、符号化された問題に対して、返される割当が実行可能（すべての硬節を満たす）かつ最適（満たされない軟節の総重みを最小化する）であることを保証する。
4. 検証：LLM の内部推論に依存せずにシステムを評価するため、著者は各問題インスタンスに対して「標準的」な MaxSAT 符号化を構築する。この標準的符号化は、検証のための真実値（ground truth）としてのみ機能する。LLM 生成コードによって生み出された解は、この標準的符号化に対して検証され、以下の点が確認される：
   • 実行可能性：解はすべての硬制約を満たしているか？
   • 最適性：解は標準的最適解と同じ目的値を達成しているか？
   • 注記：この検証は、参照意味論の下で正しい限り、代替の符号化および複数の最適解を許容する。
5. フィードバックループ：コードが実行に失敗するかエラーを生成した場合、エラーメッセージは LLM に返され、改善が行われる。重要なのは、生成プロセス中にモデルへのフィードバックとして、標準的検証結果（実行可能性/最適性のチェック）は使用されない点である。これにより、データ漏洩や参照への過学習が防止される。

主要な貢献

• 神経記号フレームワーク：著者は、LLM が重み付き部分 MaxSAT ソルバーへの自然言語インターフェースとして機能し、コード生成を通じてユーザーの意図を形式的な MaxSAT 定式化に変換する方法を提示する。
• 独立した検証：本研究は、LLM 生成の解を、実行可能性および最適性の両方について標準的符号化に対して検証する評価プロトコルを導入し、解の有効性を LLM の内部推論の正しさから切り離す。
• 選好の実証的分析：本論文は、さまざまな制約最適化問題において、異なるユーザー定義の選好構成が LLM の推論性能にどのように影響するかを分析する。
• 中間計画の評価：本研究は中間計画ステップの有効性を調査し、強力なモデルでは性能を向上させるが、弱いモデルでは誤りの伝播を引き起こす可能性があると結論づける。

実験結果

本アプローチは、最大独立集合（MIS）、スケジューリング、集合被覆という 3 つの選好ベース推論タスクファミリーで評価された。データセットは、4 つの LLM（GEMINI-3.1-PRO、GPT-5.5、LLAMA3.3、および QWEN3-CODER）でテストされた 300 インスタンス（ファミリーあたり 25 × 4 つの選好バリエーション）で構成された。

• ベースライン性能：直接回答および思考の連鎖（CoT）ベースラインは性能が低く、MIS およびスケジューリングタスクではしばしば 0% の受入率しか達成できなかった。思考のプログラム（PoT）ベースラインはわずかな改善を示したが、MaxSAT ベースのアプローチに比べて依然として著しく低かった。
• MaxSAT パイプライン性能：提案された MaxSAT ベースのパイプラインは、はるかに高い受入率を達成した。GEMINI-3.1-PRO や GPT-5.5 などの強力なモデルの場合、集合被覆タスクでは受入率が 80% を超え、中間計画を使用した場合、スケジューリングおよび MIS タスクでは約 56〜59% に達した。
• 計画の影響：中間計画は、最も強力なモデル（例：GEMINI-3.1-PRO は MIS で 36% から 56% に改善）の性能を一貫して向上させた。しかし、LLAMA3.3 や QWEN3-CODER などの弱いモデルでは、計画が時として性能を低下させ、モデルが計画を実行可能なコードに忠実に変換できない場合、誤りの伝播が発生する可能性があることを示唆した。
• 選好感受性：ユーザー選好は一般的に「選好なし」設定と比較して受入率を低下させたが、MaxSAT ベースのアプローチは、すべての選好バリエーションにおいてベースラインよりも頑健であった。

意義と主張

本論文の主な貢献は、新しいソルバーアーキテクチャではなく、選好を考慮した最適化のために形式ソルバーへのインターフェースとして LLM を使用する実証的かつ方法論的な実証にあると主張する。著者は以下を主張する：

1. 外部化が鍵：LLM は内部で最適化推論を行うことを信頼すべきではなく、代わりに自然言語の制約を実行可能なコードに変換する点で極めて効果的である。
2. ソルバーによる信頼性：最適化と検証を健全かつ完全な MaxSAT ソルバーに委譲することで、純粋な LLM 推論では提供できない実行可能性と最適性の形式的保証をシステムが達成する。
3. 頑健性：LLM 駆動の意味解釈と MaxSAT 求解の組み合わせは、専門的なドメイン言語を必要とせずにユーザー選好を許容する、頑健で検証可能な意思決定を可能にする。

著者は、意味解釈（LLM）と形式的最適化（MaxSAT ソルバー）を分離することが、特に正さが最優先される分野において、信頼性が高くユーザーに開かれた意思決定システムを構築するための有望な方向であると結論づける。また、今後の研究では、この神経記号ループの支援によりユーザーが選好を反復的に洗練できるインタラクティブな設定を探求すると述べている。