SatLM: Satisfiability-Aided Language Models Using Declarative Prompting

Summary

This paper aims at improving reasoning with large language models (LLMs) by prompting them in a way that they parse the problem into a language that is understandable by a SAT solver, and then employ an off-the-shelf SAT solver to solve the problem. Empirical results on multiple datasets show the benefit of the proposed approach.

Strengths

* The idea of obviating the need for planning by employing a SAT solver is neat. * Empirical results are strong. * The approach works on various tasks/datasets. * The analysis in Table 5 is quite interesting.

Weaknesses

* I believe the benchmarks used in this work may slightly overestimate the performance of the proposed model and the approach may not work as well on more realistic use cases (see the limitations section for more detail) * It is not clear to me how some bodies of work can fit within the parse-plan-execute framework described on Page 4. Could you comment on how the approaches such as [1, 2] that use LLMs as a tool within a reasoning algorithm can be described in this framework? How about decomposition-based approaches such as [3, 4]? * [minor] The descriptions in Section 3 and, to some extent, Section 2 could be significantly shortened and some experimental details could be moved to the supplementary (e.g., decoding strategy, temperature, etc.). This makes room for a more elaborate description of different categories of related work (as opposed to putting everything into one category) and for moving some example failures from the appendix to the main text. [1] LAMBADA: Backward Chaining for Automated Reasoning in Natural Language [2] Selection-inference: Exploiting large language models for interpretable logical reasoning [3] Decomposed prompting: A modular approach for solving complex tasks [4] Least-to-most prompting enables complex reasoning in large language mod

Questions

* Could you comment on the applicability of the approach on more realistic use cases (see limitations section for detail)? * It has been shown in [1] that in the case of logical reasoning, dealing with “unknown” examples is difficult for CoT. How does SatLM deal with unknowns (e.g., for the ProofWriter dataset)? Could the “selective prediction” analysis be extended to deal with “unknown” labels? e.g., the UNSAT class. * Any intuition why SatLM works sub-par to ProgLM on the GSM dataset, but significantly outperforms it on the GSM-SYS subset?

Rating

7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

4 excellent

Presentation

3 good

Contribution

3 good

Limitations

Many of the current LLM reasoning datasets (including some of the benchmarks in this work) have been created by first generating a puzzle in a formal language and then turning it into text either using templates or using human annotators. Therefore, the performance of approaches that translate back to a formal language (including the current work) may be overestimated on these benchmarks. Could the authors comment on the applicability of their approach to more realistic applications in the following two cases as examples: 1- Consider a logical reasoning puzzle described below: Fiona assassinated the mayor. If somebody killed the mayor, they must go to prison. Should Fiona go to prison? My guess is that if you translate to a formal language, you will get something like this: assassinated(Fiona, mayor) killed(X, mayor) -> go(X, prison) go(Fiona, prison)? which makes the solver not be able to produce the correct answer. 2- Consider the mathematical puzzle below: Fiona has 10 apples, 15 dragon fruits, and 11 coconuts. How many tropical fruits does Fiona have?

Summary

This paper propose SATLM, which aims to solve the problem of planning error when using CoT and ProgramLM. Specifically, SATLM use a LLM to translate natural language problems into formal the language that is accepted by a solver and let the solver to do planning as well as calculation. The results on several reasoning datasets show the effectiveness of this method.

Strengths

1. The paper propose to translate a problem into a formal form and then directly call a SAT solver, which is a good idea. The experiment results in Table 1 shows the effectiveness of the method. 2. The structure of the paper is clear and the paper is easy to follow. Figure 1 is informative enough to decribe the proposed method. 3. I like the ablation studies in this paper, which makes it clear which parts are important to the performance gain.

Weaknesses

1. My main concern is the method may only perform well on simpler tasks such as GSM (I think it's GSM8K?) or Proofwriter. The question in Proofwriter is nearly in the format of formal reasoning, which only requires line-by-line translation, which in turn makes the accuracy to be as high as 99.7%. On more complicated tasks such as MathQA and MATH, I think (1) the problems might not be able to expressed in first-order logic and (2) even they can, it's not easy to do the translation. 2. There are other works that combine symbolic solver with LLMs in a similar or different way. The authors have mentioned some in the related work part. However, none of them is empirically compared in this paper, and only listing the difference from them is not enough.

Questions

See weaknesses. I don't have any further questions.

Rating

5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.

Confidence

3: You are fairly confident in your assessment. It is possible that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.

Soundness

3 good

Presentation

4 excellent

Contribution

3 good

Limitations

The paper has discussion of limitations in section 6, which I think is enough.

Summary

This paper presents a framework to augment LLMs with symbolic solvers to compensate known flaws in LLMs' reasoning (e.g., planning and arithmetic). The main novelty of this paper is that LLMs is prompted to generate declarative specifications (rather programs) so that off-the-shelf automatic theorem provers like Z3 can be deployed to solve the symbolic problems.

Strengths

Augmenting LLMs with symbolic solvers is a super valuable direction to explore. Upgrading the symbolic solver from a programming language interpreter to an automatic theorem prover surely will benefit LLMs further. This paper is well motivated, nicely structured and has compelling experiments.

Weaknesses

The main weakness to me is that SatLM does not differentiate itself enough from the previous [Faithful CoT paper](https://github.com/veronica320/Faithful-COT) as a framework. Besides parsing sub-problems into a programming language like Python, Faithful CoT can also put those problems into Planning Domain Definition Language (PDDL), which is, in a sense, specification.

Questions

- line 101, [Maieutic Prompting](https://arxiv.org/abs/2205.11822) appears to be relevant here. - line 118, I know that authors decided to use Python rather than a specialized DSL here, but it would be great if the authors can elaborate on the syntax of the specification. - Table 1, it would be interesting to see results on more advanced models like gpt-3.5-turbo and gpt-4, as the performance of [Faithful CoT](https://github.com/veronica320/Faithful-COT) increased quite a bit on these models. Minor: - Figure 1, 'an NL input' - line 318, did you miss a citation here?

Rating

6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

3 good

Presentation

3 good

Contribution

2 fair

Limitations

The authors have adequately addressed the limitations.

Summary

This work looks at using an LLM to generate a declarative task specification from a natural language specification for reasoning tasks and leverage an automated SAT solver to solve the problem. They showcase that SATLM performs better than using Chain of thought or ProgramLM (which converts natural language into python programs) in various reasoning tasks.

Strengths

The paper is well-written, the experiments are thorough.

Weaknesses

The main contribution of this work seems to be about using LLMs as a semantic parser (for mostly short-context problems) which essentially maps a problem from NL specification to a formal specification (SAT problem specification here). This is a well-known problem in NLP for which LLMs (particularly LLMs which are trained on text and code) are known to perform comparably to the supervised neural semantic parsers [1,2]. The results of this work essentially indicate whether LLMs can perform NL-to-SAT semantic parsing given that once the parsing is done correctly, the SAT solver solves it. This makes the comparison between SATLM and ProgLM/CoT a bit unfair as the core ability that has to be compared is the parsing ability and not the planning/execution ability and these are intertwined in the latter. Comparisons between SATLM and other semantic parsers (other LLMs as done in Section 4.5 and other neural task-specific semantic parsers) for NL-to-SAT semantic parsing has to be highlighted in my opinion. [1] Shin, R., & Van Durme, B. (2022, July). Few-Shot Semantic Parsing with Language Models Trained on Code. In Proceedings of the 2022 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (pp. 5417-5425). [2] Zhuo, T. Y., Li, Z., Huang, Y., Li, Y. F., Wang, W., Haffari, G., & Shiri, F. (2023). On robustness of prompt-based semantic parsing with large pre-trained language model: An empirical study on codex. arXiv preprint arXiv:2301.12868.

Questions

1. Is the LLM producing anything that is semantically new and not present in the natural language specification? 2. Shouldn’t COT also be tested with text models as opposed to code models given that code models are optimized for more formal representations? 3. Just for clarification, in Table 5, does “Answered” for ProgLM mean that the program was executable without runtime errors (but it need not return the right answer)?

Rating

5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.

Confidence

4: You are confident in your assessment, but not absolutely certain. It is unlikely, but not impossible, that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work.

Soundness

3 good

Presentation

3 good

Contribution

2 fair

Limitations

I have provided the limitations of the work in the weaknesses section. The authors do address important limitations such as problems being less suitable to declarative prompting, limitations of SAT solvers when dealing with complex formulas and potential future work on re-prompting the LLM with the SAT solver feedback.

Summary

This paper describes a new approach to solving NL reasoning tasks using large language models (LLMs). Specifically, the key idea is to combine LLMs with SAT solving, where LLMs are only used in the first parsing step. The authors of the paper call this approach satisfiability-aided language modeling (SATLM). The authors also point out that by SAT, they mean all kinds of tools for automated reasoning, including traditional SAT solvers, SMT, and first-order theorem provers. The idea is that the declarative specification that is generated as output from prompting is closer and more accurate compared to more imperative problem formulation. The work is evaluated on several data sets with standard prompting, chain-of-thought (COT) prompting, and executor-augmented LLMs (PROGLM).

Strengths

- The paper is relatively easy to read and strikes a good balance between formality and accessibility. - The main idea of the paper is clear, and it seems to be a new direction of how to encode NL tasks using LLMs. - The paper contains relevant related work and contains relevant benchmarks

Weaknesses

- There is an interesting discussion on how the proposed approach can catch errors better than PROGLM (see e.g., the paragraph starting on line 166). This is good, but there is no discussion on how this kind of error can be handled. How easy is it to debug such errors? How can a user generate a fix or solution if such an error occurs? - The results are not always that easy to interpret. For instance, in table 2, if an answer is incorrect, does it then include both incorrect because of parse error, or just incorrect because of the SAT solver generating the wrong answer? This is much clearer in table 5. - The level of detail of how the approach has actually been implemented could be improved. More specifically, how are the different tools chained together, are all steps automated etc.

Questions

How do we know that SatLM generated a correct SAT problem? Can we get guarantees? If not, how can we debug the program? On lines 127-127, you explain that you use Python instead of a declarative DSL. Please provide more details on what the target language looks like for the SAT problem specification. In what ways does it differ for traditional SAT solvers, SMT, and first-order theorem provers? It would be useful to get a deeper understanding of the benchmarks. In the cases where there is a pure SAT problem (true or false), what is then the distribution of TRUE and FALSE answers? If the distribution is 50/50, would not then a random generator with uniform distribution perform better than many of the solutions that are compared?

Rating

5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.

Confidence

3: You are fairly confident in your assessment. It is possible that you did not understand some parts of the submission or that you are unfamiliar with some pieces of related work. Math/other details were not carefully checked.

Soundness

2 fair

Presentation

3 good

Contribution

2 fair

Limitations

There is a clear paragraph on the limitations of the approach at the end of the paper.

Reviewer Response

Thanks for your responses and for providing the model outputs for the examples I provided. The fact that both of them were effectively solved using your fewshots for other tasks is quite exciting. Accordingly, I have increased my score. One final recommendation: To strengthen the argument regarding the performance of the proposed model on datasets with incomplete information, I encourage the authors to consider providing results on one such dataset. One possibility is the no-conflict subset of the BoardgameQA dataset (the dataset was seemingly made public only recently, so my score will not be affected if the authors don't incorporate it).

Thanks a lot for the clarification

I appreciate the detailed response from the authors. > A: SatLM uses SAT specifications that can encode a wide range of reasoning problems spanning arithmetic reasoning, logical reasoning, and symbolic reasoning, which are further solved with a unified solver. In contrast, the PPDL specification and planner used in Faithful-CoT or LLM+P is specifically designed for planning problems. I admit that there are subtle differences between planning and SMT solving, but I don't think they are drastically different in the benchmarking scenarios in this paper. As a specification language, both PPDL and SMT-LIB (I assume you are calling Z3 through this interface) are heavily underutilized here. I understand that the authors want to emphasise that SatLM uses a unified solver (for the symbolic tasks), but I still yet to see the clear advantage of using just one solver against various symbolic solvers including programming language interpreters (e.g., Python) and PPDL solvers (which again can be a SMT solver like Z3).