FCoReBench: Can Large Language Models Solve Challenging First-Order Combinatorial Reasoning Problems?

## Abstract

Abstract Recent works show that the largest of the large language models (LLMs) can solve many simple reasoning tasks expressed in natural language, without any/much supervision. But, can they also solve challenging first-order combinatorial reasoning problems, such as graph coloring, knapsack and cryptarithmetic?
To answer this question, we present PuzzleBench , a dataset of 31 31 31 31 such challenging problems along with a few solved instances for each problem. These problems are all first order, i.e., they can be instantiated with problem instances of varying sizes, and most of them are NP-hard, requiring several reasoning steps to reach the solution.
We first observe that LLMs, even when aided by symbolic solvers, perform rather poorly on our dataset. In response, we propose a new approach, Puzzle-LM , which combines LLMs with both symbolic solvers and program interpreters, along with feedback from solved examples, to achieve huge performance gains. Our extensive experimentation and analyses offer new insights into the reasoning abilities and limitations of present-day LLMs.

## 1 Introduction

Figure: Figure 1: Illustrative Examples of problems in PuzzleBench.
Refer to caption: extracted/5425328/Images/puzzle-bench.png

Recent works have shown that large language models (LLMs) such as GPT4 OpenAI () can reason like humans Wei et al. (), and solve diverse natural language reasoning tasks, without the need for any fine-tuning Wei et al. (); Kojima et al. (); Zhou et al. (); Zheng et al. (). We note that, while impressive, most of the tasks studied are simple reasoning problems, generally requiring only a handful of reasoning steps to reach a solution.

We are motivated by the goal of assessing the reasoning limits of modern-day LLMs. In this paper, we study the computationally intensive, first-order combinatorial problems posed in natural language.
These problems (e.g., sudoku, knapsack, graph coloring, cryptarithmetic) have long served as important testbeds to assess the intelligence of AI systems Russell and Norvig (), and strong traditional AI methods have been developed for them. Can LLMs solve these directly? If not, can they solve these with the help of symbolic AI systems like SMT solvers?

To answer these questions, we release a dataset named PuzzleBench, consisting of $31$ such problems along with a few solved instances of each problem (see Figure 1).
We refer to such problems as *puzzles* / *fcore* (first-order combinatorial reasoning) problems. *Fcore* problems can be instantiated with instances of varying sizes, e.g., 9$\times$9 and 16$\times$16 sudoku. Most of the problems in PuzzleBench are NP-hard and solving them will require extensive planning and search over a large number of combinations. Not surprisingly, our initial experiments reveal that the best of LLMs can only solve less than a third of these problems.

We then turn to recent approaches that augment LLMs with tools for better reasoning. Program-aided Language models (PAL) Gao et al. () uses LLMs to generate programs, offloading execution to a program interpreter.
Logic-LM Pan et al. () and SAT-LM Ye et al. () use LLMs to convert questions to symbolic representations, and external symbolic solvers perform the actual reasoning.
Our experiments show that, by themselves, their performances are not that strong on PuzzleBench.
At the same time, both these methods demonstrate complementary strengths – PAL can handle first-order structures well, whereas Logic-LM is better at complex reasoning.

In response, we propose a new approach named Puzzle-LM, which combines the powers of *both* PAL and symbolic solvers with LLMs. In particular, the LLM generates an instance-agnostic program for an *fcore* problem that converts any problem instance to a symbolic (in our case, SMT) representation. This program passes this representation to a symbolic SMT solver, Z3 De Moura and Bjørner (), which returns a solution back to the program. The program then converts the symbolic solution to the desired output representation, as per the natural language instruction. Interestingly, in contrast to LLMs with symbolic solvers, once this program is generated, inference on new *fcore* instances can be done *without* any LLM calls.

Puzzle-LM outperforms few-shot prompting by $29.98$, PAL by $11.97$ and Logic-LM by $23.14$ percent points on PuzzleBench, with GPT-4-Turbo as the LLM. Given the structured nature of *fcore* problems, we also show how solved examples of small sizes can help improve the overall reasoning. Utilizing feedback from solved examples for just four rounds yields a further $20.5$ percent points gain for Puzzle-LM. We perform additional analyses to understand the impact of other hyperparameters, and also describe the errors made by Puzzle-LM.
We release the dataset and code for further research.

## 2 Related Work

Neuro-Symbolic AI: Our work falls in the broad category of neuro-symbolic AI Yu et al. () which builds models leveraging the complementary strengths of neural and symbolic methods. Several prior works build neuro-symbolic models for solving combinatorial reasoning problems Palm et al. (); Wang et al. (); Paulus et al. (); Nandwani et al. (, ). These develop specialized problem-specific modules (that are typically not size-invariant), which are trained over large training datasets. In contrast, Puzzle-LM uses LLMs and bypasses problem-specific architectures, generalizes to problems of varying sizes and is trained with very few solved instances.

Reasoning with Language Models: The previous paradigm to reasoning was fine-tuning of LLMs Clark et al. (); Tafjord et al. (); Yang et al. (), but as LLMs scaled, they are found to reason well, when provided with in-context examples without any fine-tuning Brown et al. (); Wei et al. (). Since then, many prompting approaches have been developed that leverage in-context learning. Prominent ones include Chain of Thought (CoT) prompting Wei et al. (); Kojima et al. (), Least-To-Most prompting Zhou et al. (), Progressive-Hint prompting Zheng et al. () and Tree-of-Thoughts (ToT) prompting Yao et al. (). These works generally study relatively simple reasoning tasks.

Tool Augmented Language Models: Augmenting LLMs with external tools has emerged as a way to solve complex reasoning problems Schick et al. (); Paranjape et al. (). The idea is to offload a part of the task to specialized external tools, thereby reducing error rates. Program-aided Language models Gao et al. () invoke a Python interpreter over a program generated by an LLM. Logic-LM Pan et al. () and SAT-LM Ye et al. () integrate reasoning of symbolic solvers with LLMs, which convert the natural language problem into a symbolic representation. Puzzle-LM falls in this category, but combines *both* PAL and symbolic solvers in a specific way to solve *fcore* problems.

Answer Verification: Several existing works verify the correctness of LLM’s answers via an external validation, such as via symbolic solvers Zhang and Callison-Burch (), or external databases Peng et al. ().
In the same spirit, Puzzle-LM utilizes solved examples in training set for verifying LLM’s output, and provide feedback to LLMs, in case of errors.

Logical Reasoning Benchmarks: There are several natural language reasoning benchmarks in literature, such as LogiQA Liu et al. () and ReClor Yu et al. () for mixed reasoning, GSM8K Cobbe et al. () for arithmetic reasoning, FOLIO Han et al. () for first-order logic, PrOntoQA Saparov and He () and ProofWriter Tafjord et al. () for deductive reasoning, and AR-LSAT Zhong et al. () for analytical reasoning. We propose PuzzleBench, which substantially extends the complexity of these benchmarks by investigating computationally hard, first-order combinatorial reasoning problems.

## 3 Problem Setup

A first-order combinatorial reasoning problem $\mathcal{P}$ has three components: a space of legal input problem instances ($\mathcal{X}$), a space of legal outputs ($\mathcal{Y}$), and a set of constraints ($\mathcal{C}$) that every input-output pair must satisfy. Example, for sudoku, input space is the space of grids with $n\times n$ cells ($n$ being a perfect square), with cells partially filled with numbers from $1$ to $n$. Output space is a fully-filled grid of the same size. And, constraints comprise row, column, and box *alldiff* constraints, along with input cell persistence.

To communicate a structured problem instance (or its output) to an NLP system, it must be serialized in text. We overload $\mathcal{X}$ and $\mathcal{Y}$ to denote the *formats* for these serialized input and output instances. Two instances of serialized inputs/outputs for sudoku are shown in Figure 2 (grey box). We are also provided (serialized) training data of input-output instance pairs, $\mathcal{D}_{\mathcal{P}}$ $=\{(x^{(i)},y^{(i)})\}_{i=1}^{N}$, where $x^{(i)}\in\mathcal{X},y^{(i)}\in\mathcal{Y}$, such that $(x^{(i)},y^{(i)})$ honors all constraints in $\mathcal{C}$.

Further, we verbalize all three components – input/output formats and constraints – in natural language instructions. We denote these instructions by
$NL(\mathcal{X})$, $NL(\mathcal{Y})$, and $NL(\mathcal{C})$, respectively. Figure 2 illustrates these for our running example.

With this notation, we summarize our setup as follows. For an abstract *fcore* problem $\mathcal{P}=\langle\mathcal{X},\mathcal{Y},\mathcal{C}\rangle$, we are provided $NL(\mathcal{X})$, $NL(\mathcal{Y})$, $NL(\mathcal{C})$ and training data $\mathcal{D}_{\mathcal{P}}$, and our goal is to learn a function $\mathcal{F}$, which maps any (serialized) $x\in\mathcal{X}$ to its corresponding (serialized) solution $y\in\mathcal{Y}$ such that $(x,y)$ honors all constraints in $\mathcal{C}$.

Figure: Figure 2: PuzzleBench Example: Filling a $n\times n$ Sudoku board along with its rules, input-output format and a couple of sample input-output pairs.
Refer to caption: extracted/5425328/Images/puzzle-bench-example-sudoku.png

## 4 PuzzleBench : Dataset Construction

First, we shortlist computationally challenging problems. For that we manually scan Wikipedia for diverse puzzles and NP-hard algorithmic problems. We also find puzzles from other publishing houses (e.g., Nikoli).(^1^11https://www.nikoli.co.jp/en/puzzles/) From this set, we select
problems (1) whose rules are easy to describe in words, (2) for whom it is easy to create a serialized input/output format, (3) for whom, the training and test datasets can be created with a reasonable programming effort, and (4) whose constraints have an SMT 2.0 encoding. This manual process led to identification of $31$ *fcore* problems (see Table 5 for a complete list), of which 24 are known to be NP-hard and others have unknown complexity. 10 problems are graph-based (e.g., graph coloring), 15 are grid based (e.g., sudoku), and 5 are set-based (e.g., knapsack).

We then create natural language instructions for each problem. We first develop input-output formats and create instructions for them ($NL(\mathcal{X})$, $NL(\mathcal{Y})$). Second, we rewrite all constraints/rules of the problem in our own words ($NL(\mathcal{C})$). This is done so that an LLM cannot easily invoke its prior knowledge about the same problem. For the same reason, we hide the name of the puzzle. Appendices A.2 and A.3 have detailed examples of rules and formats, respectively.

Next, we create train/test data for each problem. These instances are generated synthetically when possible or else hand-crafted by human experts. A single problem instance can potentially have multiple correct solutions Nandwani et al. () – all solutions are provided for each training input. The instances in the test set are typically larger in size than those in training. Because of their size, test instances may have
too many solutions, and computing all of them can be expensive. Instead, we provide a verification script for each problem, which outputs the correctness of a candidate solution for any test instance. We construct 15 training instances per *fcore* problem, and 20-50 test instances.

## 5 Puzzle-LM

### 5.1 Preliminaries and Background

Preliminaries: In the following, we assume that we have access to an LLM $\mathcal{L}$, which can work with various prompting strategies, a program interpreter $\mathcal{I}$, which can execute programs written in its programming language and a symbolic solver $\mathcal{S}$, which takes as input a pair of the form $(E,V)$, where $E$ is set of equations (constraints) specified in the language of $\mathcal{S}$, and $V$ is a set of (free) variables in $E$, and produces an assignment $\mathcal{A}$ to the variables in $V$ that satisfies the set of equations in $E$. Given the an *fcore* problem $\mathcal{P}=\langle\mathcal{X},\mathcal{Y},\mathcal{C}\rangle$ described by $NL(\mathcal{C})$, $NL(\mathcal{X})$, $NL(\mathcal{Y})$ and $\mathcal{D_{\mathcal{P}}}$, we would like to make effective use of $\mathcal{L}$, $\mathcal{I}$ and $\mathcal{S}$, to learn the $\mathcal{F}$, which takes any input $x\in\mathcal{X}$, and maps it to $y\in\mathcal{Y}$, such that $(x,y)$ honors the constraints in $\mathcal{C}$.
Background:
We consider the following possible representations for $\mathcal{F}$ which cover existing work.

- •
Exclusively LLM: Many prompting strategies Wei et al. (); Zhou et al. (); Zheng et al. () make exclusive use of $\mathcal{L}$ (potentially multiple times) to represent $\mathcal{F}$, i.e., $\mathcal{L}$ is supplied with a prompt consisting of the description of $\mathcal{P}$ in the natural language, via $NL(\mathcal{C})$, $NL(\mathcal{X})$, $NL(\mathcal{Y})$, the input $x$, along with specific instructions on how to solve the problem and asked to output $y$ directly. This puts the entire burden of discovering the mapping $\mathcal{F}$ on $\mathcal{L}$, ignoring $\mathcal{S}$ and $\mathcal{I}$.
- •
LLM $\rightarrow$ Program:
In a variation of this strategy, the LLM is prompted to instead output a program which then is interpreted by $\mathcal{I}$ on the input $x$ to produce the output $y$. This is the approach taken by methods such as PAL  Gao et al. ()
- •
LLM + Solver: This strategy makes use of both the LLM $\mathcal{L}$ and the symbolic solver $\mathcal{S}$. Whereas the primary goal of $\mathcal{L}$ is to to act as interface for translating the problem description for $\mathcal{P}$ and the input $x$, to the language of the solver $\mathcal{S}$, and the primary burden of solving the problem is on $\mathcal{S}$, whose output is then parsed as $y$. This is the approach taken by works such as Logic-LM  Pan et al. () and Sat-LM  Ye et al. ().

### 5.2 Our Approach

Our approach can be seen as a combination of LLM$\rightarrow$Program and LLM+Solver strategies described above. While the primary role of the LLM is to do the interfacing between the natural language description of the problem $\mathcal{P}$, the task of solving the actual problem is delegated to the solver $\mathcal{S}$ as in LLM+Solver strategy. But unlike them, where the LLM directly calls the solver, we now prompt it to write an input agnostic program, $\psi$, which can work with any given input $x\in\mathcal{X}$. This allows us to get rid of the LLM calls at inference time, resulting in a "lifted" implementation. The program $\psi$ internally represents the specification of the problem. It takes as argument an input $x$, and then converts it according to the inferred specification of the problem to a set of equations $(E_{x},V_{x})$ in the language of the solver $\mathcal{S}$ to get the solution to the original problem. The solver $S$ then ouptuts an assignment $A_{x}$ in its own representation, which is then passed back to the program $\psi$ which converts it back to the desired output format specified by $\mathcal{Y}$ and produces output $\hat{y}$. Broadly, our pipeline consists of the 3 components which we describe next in detail.

- •
Prompting LLMs: The LLM is prompted with $NL(\mathcal{C})$, $NL(\mathcal{X})$, $NL(\mathcal{Y})$ to generate an input-agnostic Python program $\psi$. The LLM is instructed to write $\psi$ to read an input from a file, convert it to a symbolic representation according to the inferred specification of the problem, pass the symbolic representation to the solver and then use the solution from the solver to generate the output in the desired format and write it to another file. The LLM is also prompted with information about the solver and its the underlying language in which the symbolic representation is to be generated. Optionally we can also provide the LLM with a subset of $\mathcal{D}_{\mathcal{P}}$.
- •
Symbolic Solver: $\psi$ can convert any input instance $x$ to $(E_{x},V_{x})$ which it passes to the symbolic solver. The solver is agnostic to how the representation $(E_{x},V_{x})$ was created and tries to find an assignment $A_{x}$ to $V_{x}$ which satisfies $E_{x}$ which is passed back to $\psi$.
- •
Generating the Final Output:
$\psi$ then uses $\mathcal{A}_{x}$ to generate the predicted output $\hat{y}$. This step is need because the symbolic representation was created by $\psi$ and it must recover the desired output representation from $\mathcal{A}_{x}$ which might not be straightforward for all problem representations.

### 5.3 Verification from Solved Examples

We make use of $\mathcal{D}_{\mathcal{P}}$ to verify and correct (if needed) $\psi$. For each $(x,y)\in\mathcal{D}_{\mathcal{P}}$ (solved input-output pair), we run $\psi$ on $x$ to generate the prediction $\hat{y}$, during which the following can happen: 1) Errors during execution of $\psi$; 2) The solver is unable to find $\mathcal{A}_{x}$ under a certain time limit; 3) $\hat{y}\neq y$ i.e. the predicted output is incorrect; 4) $\hat{y}=y$ i.e. the predicted output is correct. If for any training input one of the first three cases occur we provide feedback to the LLM through prompts to improve and generate a new program. This process is repeated till all training examples are solved correctly or till a maximum number of feedback rounds is reached. The feedback is simple in nature and includes the nature of the error, the actual error from the interpreter/symbolic solver and the input instance on which the error was generated. For example, in the case where the output doesn’t match the gold output we prompt the LLM with the solved example it got wrong and the expected solution. In the case where the solver is not able to solve for the constraints in the time limit, we prompt the LLM to optimize the programs. Appendix B contains details of feedback prompts.

It is possible that a single run of Puzzle-LM does not generate the correct solution for all training examples. Puzzle-LM is run multiple times for a given problem. Given the probabilistic nature of LLMs a new program is generated each time and a new feedback process continues. For the final program, we pick the best program generated during these runs, as judged by the accuracy on the training set. Figure  3 describes our entire approach diagrammatically.

Figure: Figure 3: Puzzle-LM: Solid lines indicate the main flow and dotted lines indicate feedback pathways.
Refer to caption: extracted/5425328/Images/puzzle-lm.png

**Table 1: Main Results for PuzzleBench and Puzzle-LM. - and + indicate results before and after *refinement*.**
|  | Random Guessing | Few-Shot Prompting | PAL | Logic-LM | Puzzle-LM |  |  |  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- |
| Model |  |  | - | + | - | + | - | + |
| Mixtral 8x7B |  | 23.6% | 16.1% | 37.92% | 0.0% | 1.61% | 10.77% | 36.72% |
| GPT-3.5-Turbo | 17.91% | 25.4% | 35.82% | 53.4% | 6.87% | 7.41% | 30.74% | 56.86% |
| GPT-4-Turbo |  | 30.5% | 48.51% | 66.45% | 37.34% | 39.91% | 60.48% | 93.55% |

## 6 Experimental Setup

Our experiments answer these research questions:

- 1.
How well do LLMs perform on PuzzleBench?
- 2.
How does Puzzle-LM compare with other tool-augmented LLMs on *fcore* problems?
- 3.
How useful is using feedback from solved examples and multiple runs for *fcore* problems?

Baselines: We compare our method with 3 baselines: 1) *Standard LLM prompting*, which leverages in-context learning to directly answer the questions; 2) *Program-aided Language Models*, which use imperative programs for reasoning and offload the solution step to a program interpreter; 3) *Logic-LM*, which offloads the reasoning to a symbolic solver. We use Z3 De Moura and Bjørner () an efficient SMT solver for experiments with Logic-LM and Puzzle-LM. We use the Python interpreter for experiments with PAL and Puzzle-LM. We also evaluate *refinement* for PAL and Puzzle-LM by using 4 rounds of feedback on solved examples and 5 runs for each problem. We evaluate *refinement* for Logic-LM by providing 4 rounds of feedback to correct syntactic errors in constraints (if any) for each problem instance.

Models: For each method, we experiment with 3 LLMs: GPT-4-Turbo (gpt-4-0125-preview) OpenAI () which is a SOTA LLM by OpenAI, GPT-3.5-Turbo (gpt-3.5-turbo-0125), a relatively smaller LLM by OpenAI and Mixtral 8x7B (mistral-small) Jiang et al. (), an open-source mixture-of-experts model developed by Mistral AI. For experiments with few-shot prompting and Logic-LM, we set the temperature to 0 0 for reproducible results. For experiments with PAL and Puzzle-LM we use a temperature of $0.7$ to sample several runs, each with a potentially different feedback cycle.

Prompting LLMs: For each method the prompt contains the natural language description of the rules of the problem and the input-output format. It also contains two solved examples – pairs of input and one its corresponding outputs – in the prompt. No additional intermediate supervision (e.g., SMT or Python program) is given in the prompt.
For few-shot prompting we directly prompt the LLM to solve test set instances (each tested separately). For PAL we prompt the LLM to write an input-agnostic Python program which reads the input from a file, reasons to solve the input and then writes the solution to another file, the program generated is run on each testing set instance. For Logic-LM for each test set instance we prompt the LLM to convert it into its symbolic representation which is then fed to a symbolic solver, the prompt additionally contains the description of the language of the solver. We then prompt the LLM with the solution from the solver and ask it to generate the output in the desired format. Details for Puzzle-LM can be found in Section 5.1. Prompt templates can be found in Appendix B and other experimental details can be found in Appendix C.

Metrics: For each problem we use the verification script to check if the candidate solution generated for each test set instance is correct. We use this script to compute the accuracy, i.e. fraction of test set instances solved correctly for each problem using binary marking i.e. 0 for incorrect solution and 1 for a correct solution. It is possible that no solution is generated or the solution generated is not in the output-format specified, we consider these to be incorrect and assign a score of 0. We use the macro-average of test set accuracies of all problems in PuzzleBench as our metric.

## 7 Results

Table 1 describes the main results for Puzzle-LM and other baselines on PuzzleBench. GPT-4-Turbo is significantly better than other models across all methods. Mixtral 8x7B struggles on our benchmark indicating that smaller LLMs (even with mixture of experts) are not as effective at complex reasoning tasks. Mixtral’s performance with few-shot prompting is slightly better than random guessing and with other methods (without *refinement*) is even worse than random guessing. PAL and Puzzle-LM tend to perform better than other baselines benefiting from the vast pre-training of LLMs on code Brown et al. (); Chen et al. (). Logic-LM performs rather poorly with smaller LLMs indicating that they struggle to invoke symbolic solvers directly. Hereafter, we focus on just GPT-4-Turbo’s performance, since it is far superior to other models.

Figure: (a) Effect of Feedback
Refer to caption: extracted/5425328/Images/feedback-effect.png

### 7.1 Puzzle-LM vs Baselines

Puzzle-LM outperforms few-shot prompting and Logic-LM across all problems in PuzzleBench. On average with GPT-4-Turbo the improvements are by an impressive $63.05\%$ against few-shot prompting and by $53.64\%$ against Logic-LM on PuzzleBench (with *refinement*). Few-shot prompting struggles, solving less than a third of the problems even with GPT-4-Turbo indicating the need for augmenting LLMs with tools for complicated reasoning. While Logic-LM performs better, it still struggles indicating that combining LLMs with symbolic solvers is not enough for structured reasoning problems.

Our results indicate that few-shot prompting and Logic-LM are unable to leverage the structure of *fcore* problems. As problem instance size grows, Logic-LM tends to make syntactic mistakes in the generated constraints with smaller LLMs (Table 2). With larger LLMs syntax mistakes in the constraints reduce, but they still remain semantically incorrect and could not be corrected through feedback. In contrast, Puzzle-LM exploits the first order structure of these problems by generating instance-agnostic programs during training that can then be corrected through feedback from solved examples. They can then be used independently at inference to solve any input instance, highlighting the importance of using program interpreters along with symbolic solvers.

**Table 2: Logic-LM’s performance on PuzzleBench evaluated with feedback to fix syntactic mistakes.**
| Outcome | GPT-3.5-Turbo | GPT-4-Turbo |
| --- | --- | --- |
| Correct Output | 7.41% | 39.91% |
| Incorrect Output | 46.32% | 37.90% |
| Inefficient Solution | 2.90% | 2.90% |
| Syntactic Errors | 25.62% | 6.36% |
| Errors in Converting Symbolic Output to Text | 17.73% | 12.93% |

Table 3 compares the effect of feedback and multiple runs on PAL and Puzzle-LM. Puzzle-LM outperforms PAL by $27.1\%$ on PuzzleBench (with *refinement*). This highlights the benefits of offloading the reasoning to a symbolic solver. When LLMs are forced to perform complicated reasoning while writing programs, they tend to produce brute-force solutions which are either often incorrect or extremely slow (see Table-6 in the appendix). Puzzle-LM tends to be much more efficient in terms of inference-time given that the solver can exploit the nature of the input instance while performing the reasoning unlike brute-force programs. Interestingly, feedback from solved examples and re-runs are more effective in improving performance for Puzzle-LM as indicated by the larger gains with increasing number of feedback rounds and runs. We attribute this to the fact that the programs generated by Puzzle-LM are declarative in nature, while PAL produces imperative programs which are difficult to correct.

### 7.2 Effect of Feedback on Solved Examples

Figure 4 describes the effect of multiple rounds of feedback for Puzzle-LM. Feedback helps performance significantly; utilizing 4 rounds of feedback improves reasoning abilities by $25.36\%$. Even the largest LLMs commit errors, making it important to verify and correct their work. But feedback on its own is not enough, a single run might end-up in a wrong reasoning path, which is not corrected by feedback making it important to utilize multiple runs for effective reasoning. Utilizing 5 runs improves the performance by additional $12.32\%$ after which the gains tend to saturate. Performance also increases with an increase in the number of solved examples (Table 4). Each solved example helps in detecting and correcting different errors. However, performance saturates at 7 solved examples and no new errors are discovered, even with additional training data.

**(a) Effect of number of rounds of feedback for a single run**
|  | Number of Rounds of Feedback |  |  |  |  |
| --- | --- | --- | --- | --- | --- |
|  | 0 | 1 | 2 | 3 | 4 |
| PAL | 48.51% | 54.52% | 57.83% | 58.98% | 59.80% |
| Puzzle-LM | 60.48% | 71.69% | 77.37% | 80.38% | 80.98% |
|  | $\uparrow$ 11.97 % | $\uparrow$ 17.17 % | $\uparrow$ 19.99 % | $\uparrow$ 21.4 % | $\uparrow$ 21.18 % |

**Table 4: Effect of number of solved examples (N) for feedback and number of feedback rounds for Puzzle-LM with GPT-4-Turbo on PuzzleBench for a single run.**
|  | Number of Feedback Rounds |  |  |  |  |
| --- | --- | --- | --- | --- | --- |
|  | 0 | 1 | 2 | 3 | 4 |
| N = 0 | 60.48% | 60.48% | 60.48% | 60.48% | 60.48% |
| N = 1 | 60.48% | 69.47% | 73.99% | 75.73% | 75.75% |
| N = 4 | 60.48% | 71.43% | 76.87% | 79.52% | 79.54% |
| N = 7 | 60.48% | 71.69% | 77.37% | 80.38% | 80.98% |
| N = 10 | 60.48% | 71.69% | 77.37% | 80.38% | 80.98% |

Figure: Figure 5: Effect of increasing problem instance size on baselines and Puzzle-LM for GPT-4-Turbo.
Refer to caption: extracted/5425328/Images/size-vs-algo.png

### 7.3 Effect of Problem Instance Size

We compare performance of Puzzle-LM and other baselines against varying problem instance sizes (see Figure 5) for 3 problems in PuzzleBench (sudoku, sujiko and magic-square). Increasing the problem instance size increases the number of variables, accompanying constraints and reasoning steps required to reach the solution. We observe that the performance of Puzzle-LM and PAL, which are programmatic approaches, is relatively robust against increase in size of input instances. In comparison, performance of Logic-LM and few-shot prompting declines sharply. Performance of PAL declines in some cases because of inefficient programs generated, which are unable to find a solution in the time limit.

## 8 Qualitative Analysis

We now discuss our insights on where Puzzle-LM excels and where the largest LLMs still struggle. Qualitatively, the problems in PuzzleBench can be broadly categorized into three categories:

1) Problems that our solved with 100% accuracy without any feedback from solved examples. 8 such problems exist out of the 31, including vertex-cover and latin-square. These problems have a one-to-one correspondence between the natural language description of the rules and the program for generating the constraints and the LLM essentially has to perform a pure translation task.

2) Problems that our solved with 100% accuracy but which need feedback from solved examples. There are 17 such problems. They typically do not have a one-to-one correspondence between rule descriptions and code, thus requiring some reasoning to encode the problem in the solver’s language. GPT-4-Turbo initially misses constraints or encodes the problem incorrectly, but with feedback, it can spot its mistakes and corrects its programs. Examples include k-clique and binairo. In binairo, for example, GPT-4-Turbo incorrectly encodes the constraints for ensuring all columns and rows are distinct. In k-clique, it interprets the problem incorrectly and adds an extra constraint to ensure that if a vertex is part of a clique, then all its neighbours are also a part of the clique.

3) Problems with performance below 100% which are not corrected through feedback or utilizing multiple runs. For these 6 problems, LLM finds it difficult to encode some natural language constraint into SMT. Examples include number-link and hamiltonian path, where GPT-4-Turbo is not able to figure out how to encode existence of paths as SMT constraints. In our opinion, these conversions are peculiar, and may be hard even for average computer science students.

## 9 Conclusion and Future Work

We explore the reasoning abilities of LLMs on challenging first-order combinatorial reasoning problems. We present PuzzleBench, a novel benchmark of 31 such problems and find that existing tool-augmented techniques fair poorly. In response, we present Puzzle-LM a new technique to aid LLMs with both program interpreters and symbolic solvers. Our extensive experiments show Puzzle-LM’s superior performance on our dataset. We also find that solved examples provide useful feedback to improve LLM reasoning. Further analyis reveals that Puzzle-LM struggles for a certain class of problems where conversion to symbolic representation is not straightforward. In such cases simple feedback strategies do not improve reasoning; exploring methods to alleviate such problems is a promising direction for future work. We release our code and data for further research.

## 10 Limitations

Dataset contamination is a big problem in the era of pretrained language models which have been trained on large web corpora. Therefore, its really hard to determine if a dataset has been seen as part of the training data. Determining the extent of contamination is also not easy. Since PuzzleBench does contain some standard problems from Computer Science literature, there is possibility of contamination. Usage of LLMs for reasoning on text is also limited by availability of large compute resources.
Our approach is also limited by the nature of the symbolic solver used. Some problems cannot be encoded in the symbolic language used by the solver, although our approach remains flexible enough to include several such solvers. Even in the case that a problem can be encoded in the symbolic language used by the solver, this encoding can potentially be complicated. Our method relies on the in-context learning ability of LLMs to achieve this. Additionally we assume that input instances and their outputs have a fixed pre-defined (serialized) representation.

## 11 Ethics Statement

Strubell et al. () show that the financial and environmental costs that are associated with the training of LLMs lead to significant contribution to global warming. We don’t train the model from scratch and leverage in context learning, so the energy footprint of our work is less. The large language models whose API we use for inference, especially GPT-4, consume significant energy.

## Acknowledgements

Mausam is supported by grants from Google, Huawei, and Jai Gupta Chair Professorship from IIT Delhi. Parag was supported by the DARPA Explainable Artificial Intelligence (XAI) Program (#N66001-17-2-4032). Mausam and Parag are also supported by IBM SUR awards. Any opinions, findings, conclusions, or recommendations expressed here are those of the authors and do not necessarily reflect the views or official policies, either expressed or implied, of the funding agencies. We also acknowledge the Microsoft Accelerate Foundation Models Research Program for GPT4 access.

## Appendix A PuzzleBench

### A.1 Dataset Details and Statistics

Our dataset namely PuzzleBench has $31$ different *fcore* problems that have been collected from various sources. Some of these problems have been collected from [Nikoli](https://www.nikoli.co.jp/en/) and other problems are well-known computational problems from Computer Science literature such as hamiltonian path and minimum-dominating set. Table 5 gives the details of all problems in our dataset. To create our training and test sets, we synthetically generate problem instances when possible and we handcraft problem instances otherwise. Each problem has some solved training instances and a separate set of testing instances. Each problem also has a natural language description of its rules, and a natural language description of the input-format which specify how input problem instances and their solutions are represented in text. The next few sections give illustrative examples and other details.

### A.2 Natural Language Description of Rules

This section describes how we create the natural language description of rules for problems in PuzzleBench. We extract rules from Wikipedia/Nikoli pages of the corresponding problems. These rules are reworded by a human expert to reduce dataset contamination. Another human expert ensures that there are no ambiguities in the reworded description of the rules. The rules are generalized, when needed (for eg. from a $9\times 9$ Sudoku to a $n\times n$ Sudoku). The following sections provide few examples.

#### A.2.1 Example Problem: Survo

Figure: Figure 6: Conversion of an input survo problem instance to its solution.
Refer to caption: extracted/5425328/Images/survo-example.png

Survo (Figure 6) is an example problem from PuzzleBench. The task is to fill a $m\times n$ rectangular board with numbers from $1-m*n$ such that each row and column sums to an intended target. ([Survo-Wikipedia](https://en.wikipedia.org/wiki/Survo_puzzle)).
The box given below describes the rules of Survo more formally in natural language.
We are given a partially filled $m\times n$ rectangular board, intended row sums and column sums.
- Empty cells are to be filled with numbers
- Numbers in the solved board can range from $1$ to $m*n$
- Numbers present in filled cells on the input board cannot be removed
- Each number from 1 to m*n must appear exactly once on the solved board
- All the empty cells should be filled such that each row and each column of the solved board must sum to the respective row sum and column sum as specified in the input

#### A.2.2 Example Problem: Hamiltonian Path

Figure: Figure 7: A sample input graph instance and its solution to the hamiltonian-path problem. Vertices are represented by yellow circles and the hamiltonian path is represented by the red line.
Refer to caption: extracted/5425328/Images/hamiltonian-path-example.png

Hamiltonian path is a well-known problem in graph theory in which we have to find a path in an un-directed and an un-weighted graph such that each vertex is visited exactly once by the path. We consider the decision variant of this problem which is equally hard in terms of computational complexity. The box below shows the formal rules for this problem expressed in natural language.

#### A.2.3 Example Problem: Dosun Fuwari

Figure: Figure 8: Conversion of an input dosun fuwari problem instance to its solution.
Refer to caption: extracted/5425328/Images/dosun-fuwari-example.png

Dosun Fuwari [(Nikoli)](https://www.nikoli.co.jp/en/puzzles/dosun_fuwari/) as shown in Figure 8 is another example problem from PuzzleBench.
We are given a square board with regions (cells enclosed in bold lines) and we have to fill the board with balloons and iron balls such that one balloon and one iron ball is placed in each region. Balloons are light and float, so they must be placed in one of the cells at the top, in a cell right under a black cell (filled-in cell), or under other balloons. Iron balls are heavy and sink, so they must be placed in one of the cells at the bottom, or in a cell right over a black cell or over other iron balls. The box given below gives the more formal description of the rules of dosun fuwari in natural language.

### A.3 Natural Language Description of Input and Output format

For many problems we consider input-output instances are typically not represented in text. For each problem we describe a straightforward conversion of the input and output space to text in natural language. The following sections consider examples of a few problems from PuzzleBench.

#### A.3.1 Example Problem: Survo

Figure: Figure 9: Representation of input instances of survo as text.
Refer to caption: extracted/5425328/Images/survo-input-representation.png

Figure 9 represents the conversion of the inputs to survo, originally represented as grid images to text. Here empty cells are denoted by 0’s and the filled cells have corresponding values. For a given $m\times n$ board, each row has $m+1$ space separated integers with the first m integers representing the first row of the input board and the $(m+1)^{th}$ integer representing the row sum. The last row contains $n$ integers represent the column sums.
The box below describes this conversion more formally in natural language.

#### A.3.2 Example Problem: Dosun Fuwari

Figure: Figure 10: Representation of inputs instances to dosun-fuwari as text.
Refer to caption: extracted/5425328/Images/dosun-fuwari-input-representation.png

Figure 10 represents
conversion of the inputs to dosun fuwari, originally represented as grid images to text. Here the first few lines represent the input board followed by a string ’—–’ which acts as a separator following which each of the lines has space-separated integers representing the subgrids of the input board. Cells are numbered in row-major order starting from 0, and this numbering is used to represent cells in each of the lines describing the subgrids. In the first few lines representing the input board, 0’s represent the empty cells that must be filled. 1’s denote the blackened cell, 2s denote the balloons and 3’s denote the iron balls. The box below describes these rules more formally in natural language
Input-Format:
- The first few lines represent the input board, followed by a line containing --------, which acts as a separator, followed by several lines where each line represents one subgrid
- Each of the lines representing the input board will have space-separated integers ranging from 0 to 3
- 0 denotes empty cells, 1 denotes a filled cell (blackened cell), 2 denotes a cell with a balloon, 3 denotes a cell with an iron ball
- After the board, there is a separator line containing --------
- Each of the following lines has space-separated elements representing the subgrids on the input board
- Each of these lines has integers representing cells of a subgrid
- Cells are numbered in row-major order starting from 0, and this numbering is used to represent cells in each of the lines describing the subgrids
Sample-Input:
0 0 0 0
0 1 0 0
0 0 0 0
0 0 0 1
--------
0 1
2 3 6 10
4 8 12
5 9 13 14 15
7 11
Output Format:
- The output should contain as many lines as the size of the input board, each representing one row of the solved board
- Each row should have n space separate integers (ranging from 0-3) where n is the size of the input board
- Empty cells will be denoted by 0s, filled cells (blackened) by 1s, balloons by 2s and iron balls by 3s
Sample-Output:
2 3 0 2
2 1 0 2
0 2 3 3
3 0 3 1

#### A.3.3 Example Problem: Hamiltonian Path

Figure: Figure 11: Representation of input instances to hamiltonian-path as text.
Refer to caption: extracted/5425328/Images/hamiltonian-path-input-representation.png

Figure 11 represents the conversion of inputs to hamiltonian-path, originally represented as graph image to text. The first line denotes the number of vertices present in the graph followed by which each node of the graph will be numbered from 0 - N-1. Each of the subsequent lines represents an edge of the graph and will contain two space-separated integers (according to the numbering defined previously). The output is a single word (YES/NO) indicating if a hamiltonian path exists in the graph. The box below describes this more formally in natural language.
Input Format:
- The first line will contain a single integer N, the number of nodes in the graph
- The nodes of the graph will be numbered from 0 to N-1
- Each of the subsequent lines will represent an edge of the graph and will contain two space-separated integers (according to the numbering defined above)
Sample-Input:
5
0 1
1 2
2 3
3 4
Output Format:
- The output should contain a single line with a single word
- The word should be YES if a path exists in the input graph according to constraints specified above and NO otherwise
Sample Output:
YES

**Table 5: Names of problems in the PuzzleBench, number of samples in the training set, number of samples in the test set, average size of input instances in training set, average size of input instances in test set and computational complexity. The brackets in the 4th column describe how input instance sizes are measured. ? in the computational complexity column indicates that results are not available for the corresponding problem.**
| Problem Name | Training Set Size | Test Set Size | Average Size of Input Instances in Training Set | Average Size of Input Instances in Test Set | Computational Complexity |
| --- | --- | --- | --- | --- | --- |
| [3-Partition](https://en.wikipedia.org/wiki/3-partition_problem) (Non Decision) | 15 | 30 | 12 (array size) | 17.7 | NP-Hard |
| [3-Partition](https://en.wikipedia.org/wiki/3-partition_problem) (Decision) | 15 | 30 | 12 (array size) | 17.7 | NP-Complete |
| [Binario](https://www.puzzle-binairo.com/) | 15 | 50 | 4.0$\times$4.0 (grid size) | 6.96$\times$6.96 | NP-Hard De Biasi () |
| [Clique Cover](https://en.wikipedia.org/wiki/Clique_problem) | 15 | 30 | 6.26, 9.4 (# of nodes, # of edges) | 12.9, 31.4 | NP-Complete |
| [Cryptarithmetic](https://en.wikipedia.org/wiki/Verbal_arithmetic) | 15 | 25 | 4.32 (Average # of digits in the two operands ) | 3.26 | NP-Hard Epstein () |
| [Dosun Fuwari](https://www.nikoli.co.jp/en/puzzles/dosun_fuwari/) | 15 | 30 | 3.066$\times$3.066 (grid size) | 5.23$\times$5.23 | NP-Hard Iwamoto and Ibusuki () |
| [Futoshiki](https://en.wikipedia.org/wiki/Futoshiki) | 15 | 47 | 5$\times$5 (grid size) | 7.57$\times$7.57 | NP-Hard Lloyd et al. () |
| [Graph Coloring](https://en.wikipedia.org/wiki/Graph_coloring) | 15 | 30 | 5.13, 6.8 (# of nodes, # of edges) | 9, 21.06 | NP-Complete Gent et al. () |
| [Hamiltonian Path](https://en.wikipedia.org/wiki/Hamiltonian_path) | 15 | 30 | 5.93, 8.6 (# of nodes, # of edges) | 13.0, 19.77 | NP-Complete |
| [Hamiltonian Cycle](https://mathworld.wolfram.com/HamiltonianCycle.html) | 15 | 27 | 5.93, 8.6 (# of nodes, # of edges) | 11.07, 18.67 | NP-Complete |
| [Independent Set](https://en.wikipedia.org/wiki/Independent_set_(graph_theory)) | 12 | 30 | 5.83, 7.25 (# of nodes, # of edges) | 14.26, 29.8 | NP-Complete |
| [Inshi-No-Heya](https://en.wikipedia.org/wiki/Inshi_no_heya) | 15 | 49 | 5.0$\times$5.0 (grid size) | 6.5$\times$6.5 | ? |
| [K-Clique](https://en.wikipedia.org/wiki/Clique_problem) | 15 | 31 | 4.87, 7.67 (# of nodes, # of edges) | 8.84, 26.97 | NP-Complete |
| [Keisuke](https://en.wikipedia.org/wiki/Keisuke_(puzzle)) | 15 | 30 | 4.33$\times$4.33 (grid size) | 5.83$\times$5.83 | ? |
| [Ken Ken](https://en.wikipedia.org/wiki/KenKen) | 15 | 20 | 3.26$\times$3.26 (grid size) | 5.2$\times$5.2 | NP-Hard Haraguchi and Ono () |
| [Latin Square](https://en.wikipedia.org/wiki/Latin_square) | 15 | 50 | 6.0$\times$6.0 (grid size) | 14.3$\times$14.3 | NP-Hard Colbourn () |
| [Longest Path Problem](https://en.wikipedia.org/wiki/Longest_path_problem) | 15 | 30 | 6.2, 5.87 (# of nodes, # of edges) | 12.6, 16.3 | NP-Complete |
| [Magic Square](https://en.wikipedia.org/wiki/Magic_square) | 15 | 30 | 3.0$\times$3.0 (grid size) | 4.33$\times$4.33 | ? |
| [Minimum Dominating Set](https://en.wikipedia.org/wiki/Dominating_set) | 15 | 30 | 6.0, 17.73 (# of nodes, # of edges) | 14.53, 45.0 | NP-Complete |
| [Number Link](https://en.wikipedia.org/wiki/Inshi_no_heya) | 15 | 50 | 4$\times$4 (grid size) | 7.1$\times$7.1 | NP-Hard |
| [Partition Problem](https://en.wikipedia.org/wiki/Partition_problem) | 15 | 35 | 7.06 (array size) | 15 | NP-Complete |
| [Shinro](https://en.wikipedia.org/wiki/Shinro) | 15 | 25 | 5.13$\times$5.13 (grid size) | 9.2$\times$9.2 | ? |
| [Subset Sum](https://en.wikipedia.org/wiki/Subset_sum_problem) | 15 | 30 | 3.67 (array size) | 11.87 | NP-Complete |
| [Sudoku](https://en.wikipedia.org/wiki/Sudoku) | 15 | 50 | 4.0$\times$4.0 (grid size) | 13.3$\times$13.3 | NP-Hard YATO and SETA () |
| [Sujiko](https://en.wikipedia.org/wiki/Sujiko) | 15 | 45 | 3.0$\times$3.0 (grid size) | 4.0$\times$4.0 | ? |
| [Survo](https://en.wikipedia.org/wiki/Survo_puzzle) | 15 | 47 | 13.5 (area of grid) | 20.25 | ? |
| Symmetric Sudoku | 15 | 30 | 4$\times$4 (grid size) | 6.5$\times$6.5 | ? |
| [Vertex Cover](https://en.wikipedia.org/wiki/Vertex_cover) | 14 | 30 | 6.42,1 3.42 (# of nodes, # of edges) | 12.6, 40.47 | NP-Complete |
| [N-Queens](https://en.wikipedia.org/wiki/Eight_queens_puzzle) | 15 | 30 | 3.8$\times$3.8 (grid size) | 6.33$\times$6.33 | NP-Hard Gent et al. () |
| [Knapsack](https://en.wikipedia.org/wiki/Knapsack_problem) | 15 | 30 | 4.8 (array size) | 24.56 | NP-Hard |
| [K Metric Centre](https://en.wikipedia.org/wiki/Metric_k-center) | 15 | 30 | 4.5 (# of nodes) | 7 | NP-Hard |

## Appendix B Prompt Templates

In this section we provide prompt templates used for our experiments on PuzzleBench, including the templates for the baselines we experimented with, Puzzle-LM as well as prompt templates for providing feedback.

### B.1 Few-Shot Prompt Template

### B.2 PAL Prompt Template

The following box describes the base prompt template used for PAL experiments with PuzzleBench.
Write a Python program to solve the following problem:
Task:
<Description of the Rules of the problem>
Input-Format:
<Description of Textual Representation of Inputs>
Sample-Input:
<Sample Input from Feedback Set>
Output-Format:
<Description of Textual Representation of Outputs>
Sample-Output:
<Output of Sample Input from Feedback Set>
Don’t write anything apart from the Python program; use Python comments if needed.
The Python program is expected to read the input from input.txt and write the output to a file named output.txt.
The Python program must only use standard Python libraries.

### B.3 Puzzle-LM Template

#### B.3.1 Base Prompt

### B.4 Feedback Prompt Templates

These prompt templates are used to provide feedback in the case of Puzzle-LM or PAL.

#### B.4.1 Programming Errors

Your code is incorrect and produces the following runtime error:<RUN TIME ERROR> for the following input: <INPUT> rewrite your code and fix the mistake

#### B.4.2 Verification Error

Your code is incorrect, when run on the input: <INPUT> the output produced is <OUTPUT-GENERATED> which is incorrect whereas one of the correct output is <GOLD-OUTPUT>.
Rewrite your code and fix the mistake.

#### B.4.3 Timeout Error

Your code was inefficient and took more than <TIME-LIMIT> seconds to execute for the following input: <INPUT>.
Rewrite the code and optimize it.

### B.5 Logic-LM Prompt Template

The following box describes the prompt for Logic-LM experiments with PuzzleBench, the prompt is used to convert the input to its symbolic representation.
Task:
<Description of the Rules of the problem>
Input-Format:
<Description of Textual Representation of Inputs>
Sample-Input:
<Sample Input from Feedback Set>
Output-Format:
<Description of Textual Representation of Outputs>
Sample-Output:
<Output of Sample Input from Feedback Set>
Input problem to be solved:
<Puzzle from the Test Set>
The task is to declare variables and the corresponding constraints on them in SMT2 for the input mentioned above.
The variables and constraints should be such that once the variables are solved for, one can use the solution to the variables (which satisfies the constraints) to get to the output in the desired format for the above mentioned input.
Only Write the SMT2 code and nothing else.
Write the complete set of SMT2 variables and constraints.
Enclose SMT2 code in ‘‘‘smt2 ‘‘‘

## Appendix C Experimental Details

### C.1 PuzzleBench

All methods are evaluated zero-shot, meaning no in-context demonstrations for the task are provided to the LLM. We choose the zero-shot setting for PuzzleBench because of the structured nature of problems, making it unfair to provide demonstrations of highly related problems instances to the LLM. The LLM is only given a description of the rules of the problem and the task it has to perform. For PAL and Puzzle-LM we present results with 10 solved examples for feedback.

### C.2 Hardware Details

All experiments were conducted on an Intel(R) Xeon(R) Gold 6226R CPU @ 2.90GHz, 32 cores, 64-bit, with 512 KiB L1 cache, 16 MiB L2 cache, and 22 MiB L3 cache. We accessed GPT-4-Turbo and GPT-3.5-Turbo by invoking both models via the OpenAI API. Mixtral 8x7B was also accessed by using the Mistral AI API although the model weights are available publicly. We preferred the API, over running the model locally given the ease of setup because all our other experiments were with APIs.

## Appendix D Additional Results

### D.1 Inference Time

The following tables describes the average inference time for test set instances of a few illustrative problems in PuzzleBench.

**Table 6: Average inference time in seconds of Puzzle-LM and PAL for test set instances for selected problems in PuzzleBench**
| Problem | PAL | Puzzle-LM |
| --- | --- | --- |
| Sudoku | 2.01 | 0.215 |
| Latin Square | 5.46 | 0.2 |
| Cryptarithmetic | 0.83 | 0.73 |
| Independent Set | 1.438 | 0.106 |
| Minimum Dominating Set | 0.98 | 0.112 |
| Sujiko | 0.742 | 0.102 |
| Vertex Cover | 1.58 | 0.105 |

Puzzle-LM performs much better compared to PAL because PAL programs often tend to be brute force and inefficient whereas the solver can exploit the nature of the input-instance while performing the reasoning with Puzzle-LM.

## Appendix E Examples

### E.1 Puzzle-LM

This section includes example programs generated by Puzzle-LM for some illustrative problems in PuzzleBench. Each program reads the input from a file, generates the corresponding constraints, calls the solver internally and then uses the solution from the solver to write the output in the desired format to a file.

Figure: Figure 12: Puzzle-LM example: correct program for sudoku generated by GPT-4-Turbo.

Figure: Figure 13: Puzzle-LM example: correct program for keisuke generated by GPT-4-Turbo.

Figure: Figure 14: Puzzle-LM example: correct program for hamiltonian path generated by GPT-4-Turbo.

Figure: Figure 15: Puzzle-LM example: correct program for vertex-cover generated by GPT-4-Turbo.

Figure: Figure 16: Puzzle-LM example: snippet of incorrect program for binairo generated by GPT-4-Turbo and same snippet after correction by feedback.

Figure: Figure 17: Puzzle-LM example: correct program for subset-sum generated by GPT-4-Turbo.

### E.2 PAL

This section includes example programs generated by PAL for some illustrative problems in PuzzleBench. Each program reads the input from a file, performs the reasoning and writes the output to another text file.

Figure: Figure 18: PAL example: correct program for sudoku generated by GPT-4-Turbo.

Figure: Figure 19: PAL example: correct program for futoshiki generated by GPT-4-Turbo.

Figure: Figure 20: PAL example: correct program for hamiltonian path generated by GPT-4-Turbo.

Figure: Figure 21: PAL example: correct program for vertex cover generated by GPT-4-Turbo.

Figure: Figure 22: PAL example: correct program for subset sum generated by GPT-4-Turbo.

## Appendix F Logic-LM

This section describes example runs of Logic-LM for certain problems in PuzzleBench.

Figure: Figure 23: Logic-LM example: correct constraints for a sudoku instance generated by GPT-4-Turbo.

Figure: Figure 24: Logic-LM example: correct constraints for a subset sum instance generated by GPT-4-Turbo.

Figure: Figure 25: Logic-LM example: correct constraints for graph coloring instance generated by GPT-4-Turbo.

Figure: Figure 26: Logic-LM example: syntax error (highlighted by a comment) in constraints for sudoku instance generated by GPT-3.5-Turbo.

## Peer Reviews

confidence: 2
contribution: 2
initial_rating: 3
presentation: 1
questions: - I do not understand the sentence in page 3, line 122: "These dataset are not first-order i.e. each problem is accompanied with a single instance (despite the rules potentially being described in first-order logic)."
- In page 3 line 151, does the training data $\mathcal{D}_\mathcal{P}$ condition on the previous $\mathcal{C}$ given by different problems? In my understanding, different $(x, y)$ pair may have different $\mathcal{C}$.
- In page 4 line 179-181: "The rules were re-written to ensure that an LLM cannot easily invoke its prior knowledge about the same problem. For the same reason, the name of the problem was hidden." Why can't let LLM be aware of the given problem catagory?
- In page 4 line 191: "did not contain any formal specifications or mathematical formulas" I don't know why this rule is set.
- In the last paragraph of section 4, why does the instances in the test set are typically larger in size than those in training? Also, why does the number of instances in test dataset smaller than those in the train dataset?
- In section 5.1, what is the "training" object of SymPro-LM? More specifically, this framework does not need any nn training. What does it optimize during iterations?
- In page 6 line 318, why do you use different temperature on different solvers? Could you explain the detailed reason?
- In page 7 line 349, what is the "random" approach here?
- Some typos:
  - In page 3 line 149: "We are also provided" -> "We also provides"
  - In page 4 line 213: "which takes as input" -> "which takes input as"
  - In page 5 line 266: "This step is need" -> "This step is needed"
  - In page 10 line 504: "but after" -> "only after"
soundness: 2
strengths: - The problems covered in FCoReBench are relatively comprehensive, highlighting a valuable research direction. It would be interesting to see more generalized problems to be addressed once VLM are taken into consideration.
- A corresponding responce framework has been developed for the issue proposed, and the experimental results are promising.
- The experimental section in section 7 features thorough verification and comprehensive chart presentations.
- The discussion in section 8 is insightful. It would be benificial to list the problems in each situation in the appendix, and even better, to illustrated them with diagrams in the main text. This would help to elucidate the dataset's relevance to the central issue.
summary: This paper focuses on the problem-solving ability of LLM on first-order combinatorial problems in natural language form, arguing that no existing benchmark could reveal this challange properly. To stress the significance of this issue, this paper proposes a new benchmark, FCoReBench, which covers 40 challanging problems in varying sizes and correspounding solutions. In responding to the poor performance of current LLMs on FCoReBench, this paper further proposes a new framework, SymPro-LM, to push forward the potential capacity of language models by combining symbolic solvers, program interpreters and the LM backbone. The experimental results show a significant improvement in various aspects, indicating the valuable attempt of assembling different augmented modules.
weaknesses: - The construction part of the dataset issue in Section 4 requires manual labor, which is quite labor-intensive. Could it be automated using LLM?
- The current agent can only solve first-order logic. Higher-order logic requires individual generation, which is resource-intensive and difficult to scale.
- There is a lack of innovation in the proposed framework SymPro-LM, which merely combines existing symbolic solvers and program generation. It would be better to consider a more specific design.

Writing aspects:
- There are issues with the section layout and organization; the section titles are inconsistent and not uniformly formatted (e.g. section 5 and 5.1, section 7 and 7.1). The table layout on page 7 is also peculiar.
- The overall language used in writing is subpar, being rather colloquial and informal. E.g.:
  - In Section 3, as a problem definition, there should not be such an emphasis on the subject "We." The problem should be described objectively and rigorously from a third-party perspective.
  - In Section 4, the term "the author" should be used less frequently to avoid potential privacy issues. Instead, use "agent" or "process" to emphasize actions rather than the actors, which would be more formal. If necessary, flowcharts can also be used to represent the selection, polishing, and construction processes, which would greatly assist readers in understanding the overall procedures.
- This paper primarily focuses on the benchmark, as emphasized in the title; thus, the experimental section should mainly focus on verifying the performance of the benchmark in various aspects. The current writing approach is centered around SymPro-LM. If this focus is to be maintained, the emphasis of the entire article should be placed on SymPro-LM.

---

confidence: 3
contribution: 2
initial_rating: 3
presentation: 1
questions: Is there a possibility of data contamination, where the LLMs have seen these combinatorial optimization problems in their training data, and therefore know how to formulate them easily? 

Do you have further insights on why Logic-LM performance is so much worse in Table 1? It is also formulating the model and offloading the reasoning to a solver similar to the proposed framework.

Table 1: Considering the NP-Hard nature of the problems, how come random guess achieves over 20% accuracy? What are your expectations for the eventual performance of LLMs on this dataset?
soundness: 2
strengths: The proposed SymPro-LLM can work with different instances from the same first order combinatorial optimization problem without the need to re-evaluate using LLMs.

The proposed dataset is difficult for existing LLMs. The instances are based on combinatorial reasoning problems, which are mostly NP-Hard problems.

The proposed dataset is lifted such that unlimited new instances can be generated.
summary: Introduces FCoReBench which consists of generators and evaluators for 40 combinatorial optimization problems such as sudoku, graph coloring etc. Evaluates existing prompting approaches and LLM augmentation approaches on the dataset. Proposes a new framework SymPro-LLM which when given a problem, output a program that converts the problem to symbolic representation, which is then passed to a symbolic solver to get the solution.
weaknesses: While I find the proposed approach of using LLM to output program to formulate models interesting, I am not convinced the experimentations conducted provide enough insight to LLM reasoning abilities. From the examples shown in figure 2, NL(C), NL(X), NL(Y) seems to be pseudo code for formulating the problem. The task of the LLM therefore becomes translating the pseudo code to python, which does not require the same level of reasoning as solving the problems.

The paper does not evaluate enough existing models for the new proposed benchmark dataset. For example, the state-of-the-art GPT-4o and GPT-o1 are not evaluated. The paper also include limited analysis of why the existing approaches fail on the proposed dataset. 

The writing and presentation require more clarity and focus. For example, section 7 presents results across different LLM models, different frameworks/styles of prompting, different datasets/problem classes, and different experimental setups. It is unclear to me what the key takeaways from these results are.

---

confidence: 3
contribution: 3
initial_rating: 5
presentation: 3
questions: What is the difference between first-order and non-first-order problems?
soundness: 3
strengths: Using LLM to solve logic puzzles and combinatorial problems is a very important and interesting direction. This paper contributes a well-established dataset for this field which can be valuable to the research community. The paper also proposes a framework that combines extant solvers such as Z3 with LLMs. The experiment results seem convincing and promising.
summary: The paper introduces FCoReBench, a benchmark designed to evaluate the capabilities of LLMs in solving first-order combinatorial reasoning problems. The benchmarks include NP-hard problem instances like graph coloring and knapsack, with varying instance sizes. Current LLMs struggle with these tasks, particularly as the problem size increases. To address this limitation, this paper proposes SymPro-LM, a hybrid approach that combines LLMs with symbolic solvers, enhancing performance by leveraging the strengths of both methods. 

The proposed approach achieved a 21.61% improvement over few-shot prompting, a 3.52% improvement over Program-aided Language models (PAL), and a 16.83% enhancement over Logic-LM. Additionally, incorporating feedback from solved examples boosts SymPro-LM's performance by 21.02% after four rounds, compared to 12.5% for PAL. SymPro-LM also excels on three non-first-order logical reasoning benchmarks, outperforming existing baselines on two datasets and remaining competitive on the third, highlighting the effectiveness of integrating LLMs with symbolic solvers.
weaknesses: 1. The name "first order" is a bit confusing. Does it mean it is related to first-order logic? If so, it would be great to elaborate on this connection. Otherwise, a more detailed definition should be provided. It is not clear from the paper what the difference is between first-order problems and second-order ones.

2. Whether the level of contribution of this paper meets the standard of ICLR is questionable. It is not clear whether this paper proposed novel methodologies. The main contribution according to the paper seems to be the establishment of a dataset.

Minor: The fonts in Figure 4 should be larger.

---

confidence: 4
contribution: 2
initial_rating: 3
presentation: 2
questions: What is the criteria of problem selection?
What is the overlap and difference between your problem set and existing problem set?
Why does the paper restrict its scope within first-order combinatorial reasoning problems?
soundness: 2
strengths: The paper aims to address an important problem. The proposed approach is conceptually sound, and the experimental results indicate promising improvements in the reasoning capabilities of LLMs when using the technique.
summary: This paper introduces a problem set designed to assess LLMs' ability to solve first-order combinatorial reasoning problems. It argues that current symbolic-solver-aided LLMs perform poorly on this problem set and proposes a novel approach that combines a symbolic solver with a program interpreter to improve reasoning capabilities, demonstrating superior performance on the problems.
weaknesses: This paper has several critical issues that require the authors' attention:

1. Misalignment Between Title and Content: While the title suggests a focus on the proposed problem set, the main body primarily discusses the technique, SymPro-LM. After reviewing the entire paper, it appears more as a technique paper rather than a benchmark paper. I suggest revising the title and reorganizing the structure to more accurately reflect its focus on methodology.

2. Lack of Clarity on Incremental Contributions of the Problem Set: Although the problem set seems useful, the paper does not clearly articulate its unique contribution. Existing symbolic-solver-aided LLM approaches have already addressed similar reasoning problems, and some may have been tested on benchmarks containing first-order combinatorial reasoning problems. It is essential to compare the proposed problem set with these existing benchmarks, highlighting overlaps and differences. However, this paper provides limited detail on this aspect.

3. Scope Restriction and Generalizability of the Technique: While the paper narrows its focus to first-order combinatorial reasoning problems, conceptually, the proposed technique has broader applicability across various reasoning tasks. Given the absence of any domain-specific adaptations, I recommend either expanding the paper’s scope and conducting a more comprehensive evaluation across diverse reasoning problems, or explaining the reason of the scope restriction.

4. Use of an Outdated LLM in Evaluation: The LLM used in the evaluations appears a bit outdated. I suggest incorporating recent models, such as GPT-4o and o1, to provide a more relevant assessment.

5. Unclear Criteria for Problem Selection in the Problem Set: The criteria for including specific problems in the problem set are not well-defined. For example, while the paper includes problems from the industry track of SAT competitions, it does not explain the exclusion of others (e.g., the main track). Furthermore, recent SAT competitions no longer feature an industry track, making the rationale for this selection unclear.

Meta-review: This paper introduces a new benchmark, FCoReBench, consisting of 40 combinatorial optimization problems whose constraints, inputs, outputs, and examples are all stated in natural languages. Additionally, this paper also proposes a new framework, SymPro-LM, which outperforms existing prompting methods like few-shot prompting and program-aided prompting.  Introducing new datasets and prompting frameworks to improve the reasoning capability of LLMs are valuable contributions. However, several important concerns are not addressed properly. For instance, to what extent the 40 combinatorial problems are new compared to existing reasoning tasks? Although the problem is stated in natural language, the form is still rigid -- clear separations regarding constraints, I/O instructions, and examples have to be specified, making it not far from a piece of pseudo-code. Furthermore, the key motivation is not very clear; on one hand, it suggests the contribution of benchmark, the novelty of which is a bit questionable; on the other hand, the authors want to show the new framework, SymPro-LM, significantly outperforms existing techniques on a newly crafted benchmark. A more systematic comparison of existing benchmarks where baseline approaches were evaluated would be expected.

Decision: Reject