SatLM: Satisfiability-Aided Language Models Using Declarative Prompting

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.

Summary Notes

Boosting Logical Reasoning in AI with the SAT LM Approach

Introduction

Understanding the SAT LM Approach

Parsing

• The process begins by translating natural language inputs into a formal specification, laying the groundwork for precise problem-solving.

Planning and Execution

• Using a SAT solver, the method finds solutions based on the formal specifications, achieving remarkable accuracy in navigating through problem complexities.

Evaluation

• SAT LM shows superior results across various datasets, especially in tasks that demand complex logical reasoning.

Methodology Explained

Declarative Prompting

• This involves transforming problem descriptions into logical constraints, facilitating the bridge from natural language to the solver's formal language.

Solving with a SAT Solver

• The solver then processes these constraints to find a solution that meets all requirements, significantly reducing common errors found in traditional models.

Experiments and Results

Datasets

• The approach was tested on tasks like arithmetic reasoning, logical reasoning, symbolic reasoning, and regex synthesis, offering a broad evaluation platform.

Performance

• SAT LM outdid traditional and chain-of-thought models, setting new performance standards in several domains.

In-depth Analysis

Error Analysis

• A key advantage of SAT LM is its ability to refrain from making predictions when faced with unsatisfiable or ambiguous inputs, boosting its accuracy.

Comparison with Previous Work

• Against imperative reasoning models, SAT LM shows a clear edge, handling a wide range of complex tasks with better effectiveness.

Advantages of SAT LM

• Reduction of Errors: By utilizing a SAT solver, SAT LM minimizes common errors in complex reasoning, improving LLM reliability.

• Superiority over Traditional Models: It shows marked improvements in handling complex logical tasks, making it a more effective choice.

Conclusion

Looking Ahead

Code and Data Availability

How Athina AI can help