通过基于偏好的最大可满足性实现大语言模型的可靠推理

大语言模型（LLM）擅长理解自然语言，却难以应对涉及多重约束与用户自定义偏好的优化任务，这类任务常见于机器人学等领域。我们提出一种混合推理方法，让 LLM 通过代码生成将推理外化。给定自然语言的问题描述，LLM 生成 Python 代码，将用户定义的约束与偏好编码为一个基于偏好的最大可满足性（MaxSAT）问题，再由精确 MaxSAT 求解器求解。为确保正确性，模型生成代码所返回的解会对照一个规范的 MaxSAT 编码独立验证其可行性与最优性，同时允许不同的编码与多个最优解。我们使用开源与闭源 LLM，在三类基于偏好的推理任务族上评估该方法，并在相同模型下与直接回答、思维链（chain-of-thought）与程序思维（program-of-thought）基线进行比较。这些基线很少能产出可行解，而基于 MaxSAT 的流水线获得了显著更高的接受率，某些情形下超过 80%。我们的结果表明，LLM 驱动的代码生成与基于偏好的 MaxSAT 相结合，能够实现相对于所生成编码的可由求解器验证的优化，并在独立验证的参照语义下大幅提升正确性。