arXiv:2605.29687cs.AIcs.LO2026-05

用大模型生成代码求解带偏好的约束优化问题,确保结果可验证且正确率超80%。

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

  • 大模型将自然语言转为代码,构建偏好型最大可满足性问题
  • 在三类任务上,正确解接受率超80%,远高于其他基线方法
  • 适合需要高可靠性与可验证性的机器人等决策场景

大语言模型(LLMs)在理解自然语言方面表现优异,但在涉及多约束和用户偏好的优化任务中表现不佳,这类问题常见于机器人领域。本文提出一种混合推理方法:让LLM通过代码生成外部化推理过程。给定自然语言问题描述,模型生成编码用户偏好与约束的Python代码,构建偏好型最大可满足性(MaxSAT)问题,并由精确的MaxSAT求解器求解。为保证正确性,模型生成代码返回的解会通过独立验证,对比标准MaxSAT编码,确保可行性与最优性,支持不同编码方式和多个最优解。我们在开源与闭源大模型上评估了三种偏好型推理任务,与直接回答、思维链及程序链基线进行对比。结果显示,这些基线很少生成可行解,而本方法的解接受率显著提升,某些情况下超过80%。结果表明,基于大模型生成代码与偏好型MaxSAT结合的方法,能实现对生成编码的求解器可验证优化,在独立验证的语义下大幅提高正确性。

原文摘要 · Abstract (English)

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.

大模型推理约束优化可验证性MaxSAT

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。