PaperlayerView exact revision on arXiv

Source-linked AI summary

SatLM: Satisfiability-Aided Language Models Using Declarative Prompting

Xi Ye, Qiaochu Chen, Isil Dillig, Greg Durrett

arXiv:2305.09656v3cs.CLcs.AI

TL;DR

Constraint-solving tasks can exceed the planning abilities of imperative chain-of-thought and program-aided language models. SATLM instead has an LLM produce declarative constraints and delegates planning and execution to an automated solver, consistently outperforming imperative baselines across eight datasets, including a 23% GSM-SYS advantage and new state-of-the-art results on LSAT and BOARDGAMEQA.

  • Problem

    Imperative reasoning procedures are less effective for constraint-solving problems that require planning and search rather than fixed forward reasoning.

    Source: §1 · p. 2

  • Method

    SATLM prompts an LLM to parse natural-language tasks into declarative logical specifications and uses an automated theorem prover to plan and execute the solution.

    Source: §1 · p. 2, §2 · p. 3

  • Results

    SATLM consistently outperforms COT and PROGLM across 8 datasets; it exceeds PROGLM by 23% on GSM-SYS and sets new state of the art on LSAT and BOARDGAMEQA.

    Source: §1 · p. 2, §4.2 · p. 7

  • Takeaways & Limitations

    Delegating planning and execution to a solver addresses planning errors while enabling solver-based abstention on unsatisfiable or ambiguous specifications.

    Source: §1 · pp. 2–3

    SATLM may be less effective when a problem’s natural-language description is more compatible with imperative solving, and it inherits computational and expressiveness limitations of SAT solvers.

    Source: §6 · p. 10

Abstract

from arXiv · show

Prior work has combined chain-of-thought prompting in large language models (LLMs) with programmatic representations to perform effective and transparent reasoning. While such an approach works well for tasks that only require forward reasoning (e.g., straightforward arithmetic), it is less effective for constraint solving problems that require more sophisticated planning and search. In this paper, we propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of LLMs. We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. This approach has two key advantages. The declarative specification is closer to the problem description than the reasoning steps are, so the LLM can parse it out of the description more accurately. Furthermore, by offloading the actual reasoning task to an automated theorem prover, our approach can guarantee the correctness of the answer with respect to the parsed specification and avoid planning errors in the solving process. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm. In particular, SATLM outperforms program-aided LMs by 23% on a challenging subset of the GSM arithmetic reasoning dataset; SATLM also achieves a new SoTA on LSAT and BoardgameQA, surpassing previous models that are trained on the respective training sets.

1 Introduction

SATLM addresses constraint-solving problems where imperative chain-of-thought procedures struggle to plan, by having an LLM parse declarative constraints and a solver perform reasoning. Across eight datasets, it consistently outperforms imperative baselines and supports solver-based error handling and abstention.

Motivation

  • Imperative CoT and program-aided approaches are less effective when problems provide constraints without a clear reasoning plan.These approaches work better when the natural language already specifies a forward-solving procedure.Source: §1 · pp. 1–2

Approach

  • SATLM prompts an LLM to translate natural-language problems into logical constraints, then invokes a SAT solver to plan and execute the solution.The LLM handles parsing, while the solver handles reasoning and guarantees execution correctness relative to the parsed specification.Source: §1 · p. 2, Figure 1 · p. 2

Results

  • 23%: SATLM outperforms PROGLM on GSM-SYS, a challenging arithmetic-reasoning subset.On GSM, SATLM reaches 84.8% with self-consistency decoding and matches prior work using the full training set and the same LLM.Source: §1 · p. 2
  • SATLM consistently outperforms COT and PROGLM across 8 datasets spanning arithmetic, logical, symbolic, and regex-synthesis tasks.It also sets new state of the art on LSAT, BOARDGAMEQA, and STRUCTUREDREGEX.Source: §1 · p. 2

Analysis

  • Solver feedback can identify invalid, unsatisfiable, or ambiguous specifications, allowing SATLM to abstain from uncertain predictions.This extends beyond execution-error detection available from the executor used in PROGLM.Source: §1 · pp. 2–3

2 Overview

SATLM separates parsing from planning and execution: an LLM produces a formal declarative specification, while a symbolic solver derives the answer. This design targets planning errors and provides soundness relative to the parsed facts and query.

Framework

  • Natural-language reasoning tasks can be decomposed into parsing, planning, and execution.The input describes facts Φ and a question Q, and the goal is to derive an answer from those facts.Source: §2 · p. 3

Declarative parsing

  • SATLM uses an LLM to parse natural language into a formal specification containing facts and a query, without explicitly generating reasoning steps.The specification interleaves natural-language statements with logical formulas, from which the formal task is extracted.Source: §2 · p. 3

Solver reasoning

  • A SAT solver performs both planning and execution from the predicted specification and returns the assignment for the query variable as the answer.The solver can produce a proof of validity for the resulting entailment.Source: §2 · p. 3
  • Because the solver is sound, its assignment satisfies the parsed formula by construction, assuming the parsed facts and query match the original problem.The guarantee concerns correctness with respect to the specification produced by parsing.Source: §2 · p. 3

Example

  • Figure 2 contrasts parsing and reasoning failures in COT and PROGLM with SATLM’s solver-based derivation of the correct answer.COT misparses an equation, while PROGLM generates an incorrect reasoning chain.Source: Figure 2 · p. 4, §2 · p. 4

Comparison

  • SATLM differs from CoT and PROGLM by moving planning from the LLM or an imperative program into a symbolic solver.The approach is designed to address planning errors in addition to execution errors.Source: §2 · p. 4

3 SAT-Aided Language Models using Declarative Prompting

SATLM uses few-shot declarative prompting to convert natural-language tasks into general SAT instances, then applies an automated theorem prover to solve them. The solver also supplies diagnostic feedback that supports selective abstention.

3.1 Declarative Prompting

  • Few-shot prompting generates an interleaved specification of natural-language statements and logical formulas for each test input.The formal specification is obtained by extracting the logical formulas from the generated sequence.Source: §3.1 · p. 4
  • The prompts represent formulas in Python-like syntax and use comments, meaningful variable names, and descriptive text to improve translation fidelity.A postprocessing step converts the prompted formulas into solver input.Source: §3.1 · p. 4

3.2 Solving with a SAT Solver

  • A SAT problem is a triple P = (Φ, T, Q), consisting of formulas, an underlying theory, and a query.The query uses variables appearing in the formula set.Source: §3.2 · p. 5
  • Arithmetic, logical, symbolic, and regex tasks are formulated as SAT problems, using equations or encoded preconditions to represent constraints.The target expression identifies the quantity or statement to derive.Source: §3.2 · p. 5
  • Unlike task-specific solver pipelines, SATLM formulates all evaluated tasks as general SAT instances handled by a single solver.This provides a unified solving framework across task types.Source: §3.2 · p. 5
  • The system extracts constraints and a target from the generated specification, identifies the theory, and passes the resulting instance to an automated theorem prover.The implementation uses a solver such as Z3 SMT.Source: §3.2 · p. 5
  • Solver outcomes distinguish execution errors, unsatisfiable formulas, and ambiguous formulas with multiple feasible solutions.These outcomes arise from invalid formulas or timeouts, conflicting constraints, or insufficiently constraining formulas, respectively.Source: §3.2 · p. 5
  • Because SAT solvers detect UNSAT and AMBIG in addition to execution errors, SATLM can abstain from potentially incorrect predictions more effectively than PROGLM.This capability is used in the selective-prediction setting.Source: §3.2 · p. 5

4 Experiments

Experiments compare SATLM with prompting and executor-augmented baselines across eight datasets and four reasoning tasks. SATLM generally achieves stronger performance, while solver-backed declarative prompting also improves planning, selective prediction, and robustness across settings.

Setup

  • The evaluation covers eight datasets spanning arithmetic, logical, symbolic, and regex-synthesis tasks, using standard prompting, COT, and PROGLM as baselines.The experiments focus especially on arithmetic and logical reasoning.Source: §4.1 · pp. 5–6

Main results

  • SATLM outperforms COT and PROGLM across datasets, except for GSM with greedy decoding, where it is on par with PROGLM.All improvements over PROGLM are statistically significant with p < 0.05.Source: Table 1 · p. 6, §4.2 · p. 6
  • 37.4%: SATLM raises the LSAT state of the art from 30.9%, while 80.7% raises BOARDGAMEQA from 73.9%.SATLM also achieves the best performance on CLUTRR, PROOFWRITER, and COLOR under both decoding strategies.Source: §4.2 · p. 7
  • 44.0%: declarative prompting exceeds PROGLM’s 37.1% on regex synthesis with greedy decoding, and self-consistency surpasses the previous 55.6% state of the art.This result extends the comparison beyond arithmetic and logical reasoning.Source: §4.2 · p. 7

Ablations and analysis

  • The symbolic solver provides further gains by guaranteeing correct planning and execution, while declarative prompting alone improves over imperative COT by 7.9% on GSM-SYS and 8.1% on CLUTRR.SATLM can also abstain on unsatisfiable or ambiguous specifications, improving selective prediction; on GSM, self-consistency increases coverage and accuracy relative to PROGLM.Source: §4.3 · pp. 7–8, §4.4 · p. 8

5 Related Work

SATLM differs from prior tool-augmented reasoning work by parsing natural-language problems into declarative SAT formulations and delegating solving to a solver. Related approaches instead use imperative programs, PDDL planners, or arithmetic-specific solvers.

  • SATLM parses natural-language problems into declarative SAT problems and offloads the solving procedure to a SAT solver.Source: §5 · p. 10
  • Earlier approaches commonly generate imperative programs executed by Python, domain-specific, or other symbolic executors.Source: §5 · p. 10
  • Concurrent planning work parses problems into PDDL descriptions and uses a classical planner, whereas SATLM targets general reasoning tasks that PDDL cannot specify.Source: §5 · p. 10
  • Concurrent arithmetic work uses variables, equations, and a math-specific solver, while SATLM formulates tasks in first-order logic for a domain-agnostic approach.Source: §5 · p. 10

6 Conclusion & Limitations

The paper concludes that SATLM provides a unified framework for reasoning tasks, while identifying limits from task compatibility, solver cost, expressiveness, and its one-round design.

Conclusion

  • SATLM casts diverse reasoning tasks into SAT problems using an LLM for declarative parsing and a SAT solver for answer derivation.Source: §6 · p. 10
  • Evaluation on 8 datasets spanning 4 tasks shows SATLM is effective against program-aided language models.Source: §6 · p. 10

Limitations

  • SATLM may be less effective when a problem’s natural-language description is more compatible with imperative solving procedures.The authors give GSM as an example, where SATLM slightly lags PROGLM.Source: §6 · p. 10
  • SATLM inherits solver limitations, including computational cost for complex quantified or nonlinear formulas and restricted expressiveness of the underlying theory.Source: §6 · p. 10
  • The current pipeline parses, solves, and answers in one round rather than re-prompting after unsatisfiable or ambiguous specifications.Source: §6 · p. 10

A Detailed Statistics of Datasets

The appendix documents dataset construction, prompting choices, exemplar settings, and comparison procedures across the evaluated tasks. It also introduces GSM-SYS as a targeted arithmetic subset and reports prompt-set sensitivity.

Dataset construction

Prompting

  • The study adapts existing COT and PROGLM prompts where available and writes SATLM prompts for matching exemplar sets.Source: B Details of the Prompts · p. 16
  • For LSAT, the authors sample 8 exemplars and omit PROGLM because Python lacks native support for the formal-logic reasoning required by the task.Source: B Details of the Prompts · p. 16

Prompt sensitivity

D Extended Discussion on Concurrent Work

The concurrent-work discussion distinguishes SATLM from arithmetic-specific solver approaches by emphasizing a first-order-logic formulation that unifies multiple reasoning tasks. On ALGEBRA, SATLM outperforms the reported baselines by more than 20%.

E Detailed Performance on the BOARDGAMEQA Dataset

Table 11 reports BOARDGAMEQA performance by reasoning depth. SATLM substantially outperforms COT at depths 1–3, while every approach declines as depth increases.

Performance by depth

F Details of the SAT Specification

The SAT specification uses a z3py-like constraint syntax that is adapted for prompting and then transformed into executable z3py code. A parser performs this conversion before execution obtains the final answer.

Specification syntax

Postprocessing and execution

  • A simple parser transforms the prompted formulas into actual z3py specifications through string transformation.The transformed code can then be executed using z3py to obtain the final answer.Source: F Details of the SAT Specification · pp. 18–19

G Examples of Error Cases of SATLM

The examples show that SATLM can produce unsatisfiable, ambiguous, or incorrect-answer cases when the LLM misparses or omits constraints. Some incorrect formulas nevertheless yield non-ambiguous answers.

Example tasks

UNSAT cases

  • UNSAT formulas arise when the LLM misunderstands a problem and outputs conflicting constraints.The conflicting constraints are highlighted in the GSM examples.Source: Figure 6 · p. 20

AMBIG cases

  • AMBIG formulas are under-constrained because the LLM fails to encode constraints, producing multiple possible answers.For CLUTRR, ambiguity can also arise when the language description itself is highly ambiguous.Source: Figure 7 · p. 20, Figure 8 · p. 21

Incorrect answers

  • SATLM can return an incorrect answer even when the solver derives a non-ambiguous solution.These cases occur when the LLM outputs incorrect constraints, as illustrated for GSM and CLUTRR.Source: §G.2 · p. 22, Figure 9 · p. 22

H Examples of Execution Errors and Planning Errors Made by COTSOLVER

The COTSOLVER examples distinguish execution errors from planning errors. Interpreters can address arithmetic execution mistakes, but they do not resolve failures to manipulate symbols or construct valid reasoning chains.

Execution errors

Comparison with PROGLM

Planning errors

Prompts and task examples

  • The appendix provides prompts and example tasks spanning GSM, LSAT, BOARDGAMEQA, CLUTRR, PROOFWRITER, COLORED OBJECT, and STRUCTUREDREGEX.The prompt excerpts also include SATCOTSOLVER and comparison prompts for PROGLM.Source: Figure 13 · p. 26, Figure 14 · p. 27, Figure 15 · p. 28

Related papers

Loading 2305.09656v3…