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

📄 arXiv: 2605.29687v1 📥 PDF

作者: Pedro Orvalho, Marta Kwiatkowska, Guillem Alenyà, Felip Manyà

分类: cs.AI, cs.LO

发布日期: 2026-05-28

备注: 17 pages, 1 figure, 4 tables

💡 一句话要点

提出基于偏好最大可满足性的方法以解决LLM优化问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 最大可满足性 优化问题 代码生成 机器人技术 推理方法 偏好处理

📋 核心要点

  1. 现有的LLM在处理多约束和用户偏好的优化任务时，往往无法产生可行的解决方案，导致实际应用受限。
  2. 本文提出了一种通过代码生成将LLM推理外部化的方法，利用偏好最大可满足性（MaxSAT）问题进行优化。
  3. 实验结果显示，基于MaxSAT的解决方案在接受率上显著高于直接回答和思维链等基线方法，提升幅度可达80%。

📝 摘要（中文）

大型语言模型（LLMs）在理解自然语言方面表现出色，但在涉及多重约束和用户定义偏好的优化任务中存在困难，尤其是在机器人领域。本文提出了一种混合推理方法，通过代码生成将LLMs的推理外部化。给定自然语言问题描述，LLM生成Python代码，将用户定义的约束和偏好编码为基于偏好的最大可满足性（MaxSAT）问题，并由精确的MaxSAT求解器解决。为确保正确性，模型生成的代码返回的解决方案会独立验证其可行性和最优性。实验表明，基于MaxSAT的管道在接受率上显著高于其他基线方法，部分情况下超过80%。

🔬 方法详解

问题定义：本文旨在解决大型语言模型在多约束和用户偏好优化任务中的不足，现有方法往往无法提供可行的解决方案，限制了其在实际应用中的有效性。

核心思路：提出了一种混合推理方法，通过生成Python代码将用户定义的约束和偏好转化为偏好最大可满足性（MaxSAT）问题，从而利用MaxSAT求解器进行优化。

技术框架：整体架构包括三个主要模块：首先，LLM根据自然语言问题生成Python代码；其次，生成的代码将约束和偏好编码为MaxSAT问题；最后，使用精确的MaxSAT求解器解决该问题，并对结果进行独立验证。

关键创新：最重要的创新在于将LLM生成的代码与MaxSAT求解器结合，形成了一种新的优化框架，使得生成的解决方案可以被独立验证，从而提高了结果的正确性和可行性。

关键设计：在设计中，关注了生成代码的准确性和MaxSAT编码的有效性，确保了求解器能够处理不同的编码方式，并支持多种最优解的返回。

📊 实验亮点

实验结果表明，基于MaxSAT的管道在接受率上显著高于其他基线方法，部分情况下超过80%。相比之下，直接回答和思维链等方法几乎未能产生可行的解决方案，显示出本文方法的有效性和优越性。

🎯 应用场景

该研究的潜在应用领域包括机器人路径规划、资源分配和决策支持系统等。通过提高LLM在复杂优化任务中的表现，能够为实际应用提供更可靠的解决方案，推动智能系统的进一步发展。

📄 摘要（原文）

Large Language Models (LLMs) excel at understanding natural language but struggle with optimisation tasks involving multiple constraints and user-defined preferences, which commonly arise in domains such as robotics. We propose a hybrid reasoning approach in which LLMs externalise reasoning through code generation. Given a natural language problem description, an LLM generates Python code that encodes user-defined constraints and preferences as a preference-based Maximum Satisfiability (MaxSAT) problem, which is then solved by an exact MaxSAT solver. To ensure correctness, solutions returned by the model-generated code are independently verified for feasibility and optimality against a canonical MaxSAT encoding, allowing for different encodings and multiple optimal solutions. We evaluate our approach using both open-source and closed-access LLMs on three families of preference-based reasoning tasks, and compare it against direct-answer, chain-of-thought, and program-of-thought baselines using the same models. While these baselines rarely produce feasible solutions, the MaxSAT-based pipeline achieves substantially higher acceptance rates, in some cases exceeding 80%. Our results demonstrate that LLM-driven code generation combined with preference-based MaxSAT enables solver-verifiable optimisation with respect to generated encodings, and substantially improves correctness under independently verified reference semantics.