Source-linked AI summary
SatLM: Satisfiability-Aided Language Models Using Declarative Prompting
Xi Ye, Qiaochu Chen, Isil Dillig, Greg Durrett
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.
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.
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.
Takeaways & Limitations
Delegating planning and execution to a solver addresses planning errors while enabling solver-based abstention on unsatisfiable or ambiguous specifications.
Takeaways & Limitations
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.
Abstract
from arXiv · showhide
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.
- 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.
- 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.
- Results: 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.
- 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.
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.
- 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.
- 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.
- Solver reasoning: 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.
- 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.
- 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.
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.
- 3.1 Declarative Prompting: 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.
- 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.
- 3.2 Solving with a SAT Solver: 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.
- 3.2 Solving with a SAT Solver: 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.
- 3.2 Solving with a SAT Solver: 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.
- 3.2 Solving with a SAT Solver: 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.
- 3.2 Solving with a SAT Solver: 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.
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.
- 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.
- Main results: 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.
- Main results: 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.
- 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.
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.
- Earlier approaches commonly generate imperative programs executed by Python, domain-specific, or other symbolic executors.
- Concurrent planning work parses problems into PDDL descriptions and uses a classical planner, whereas SATLM targets general reasoning tasks that PDDL cannot specify.
- Concurrent arithmetic work uses variables, equations, and a math-specific solver, while SATLM formulates tasks in first-order logic for a domain-agnostic approach.
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.
- Conclusion: Evaluation on 8 datasets spanning 4 tasks shows SATLM is effective against program-aided language models.
- 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.
- Limitations: SATLM inherits solver limitations, including computational cost for complex quantified or nonlinear formulas and restricted expressiveness of the underlying theory.
- Limitations: The current pipeline parses, solves, and answers in one round rather than re-prompting after unsatisfiable or ambiguous specifications.
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: CLUTRR uses exemplars requiring 2–3 reasoning steps and tests generalization to examples requiring up to 10 steps.
- Dataset construction: PROOFWRITER evaluation samples 1,000 depth-5 test examples, while STREGEX combines its test and test-E splits into 996 examples.
- Dataset construction: GSM-SYS contains 547 GSM examples whose human-annotated solutions involve systems of equations.The subset was created by filtering for equation-related patterns and manually inspecting 10% of examples.
- Prompting: The study adapts existing COT and PROGLM prompts where available and writes SATLM prompts for matching exemplar sets.
- Prompting: For LSAT, the authors sample 8 exemplars and omit PROGLM because Python lacks native support for the formal-logic reasoning required by the task.
- Prompt sensitivity: Adapting exemplar sets improves COT and PROGLM on GSM-SYS, while SATLM still outperforms both by a large margin on GSM.
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%.
- Unlike arithmetic-specific solver work, SATLM uses first-order logical formulas to unify a wider range of reasoning tasks.
- ALGEBRA contains 222 examples from algebra textbooks and is described as more challenging than GSM.
- More than 20%: SATLM outperforms PROGLM and COT on ALGEBRA.
- Results on ALGEBRA and MATHSYM are not directly comparable because the datasets use different exemplar sets.
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: SATLM outperforms COT by a substantial margin across BOARDGAMEQA depths 1–3.The performance breakdown is reported in Table 11.
- Performance by depth: Performance decreases for all approaches as BOARDGAMEQA reasoning depth increases.
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: SATLM uses a specification syntax that largely follows and simplifies z3py constraint syntax.The design leverages LLM knowledge acquired from pretraining on code.
- Specification syntax: Figure 5 demonstrates syntax for different types of statements in the SAT specification.The formulas are close to actual z3py formulas but are slightly modified to improve prompting.
- 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.
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: The examples include GSM arithmetic questions and a CLUTRR relationship question.The GSM examples include rectangle, number-sum, and bell-counting problems; the CLUTRR example asks about a family relationship.
- UNSAT cases: UNSAT formulas arise when the LLM misunderstands a problem and outputs conflicting constraints.The conflicting constraints are highlighted in the GSM examples.
- 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.
- 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.
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: Execution errors occur when COTSOLVER makes mistakes while applying arithmetic operators or CLUTRR transitivity rules.For CLUTRR, the relevant atomic function infers a relation between two entities from two given relations.
- Comparison with PROGLM: PROGLM can help fix execution errors by introducing an interpreter, but it is not effective for the planning errors shown in the examples.
- Planning errors: Planning errors involve failing to arrange symbolic operations into a chain of equations leading to the correct answer.Examples include failing to flip a sign, dropping an occurrence of a variable, applying an incorrect transitivity rule, or inventing an incorrect procedure.
- 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.