LLMs have significantly improved natural language processing, achieving strong performance on a variety of tasks using few-shot learning (?). However, LLMs remain weak at tasks that involve complex reasoning (?; ?), and scaling model size alone is not enough to achieve good performance (?). It has been shown that various prompting methods improve accuracy on reasoning tasks (?; ?; ?). ? (?) present a dual-system model which uses an LLM as a semantic parser and couples it with a custom symbolic module to achieve performance gains on reasoning tasks. This framework combines the strengths of LLMs for parsing complex natural language and symbolic logic for handling complex reasoning. However, the authors had to use hand-engineered set of constraints for the latter part. To our knowledge, our work is the first to use LLMs to generate logic rules to solve complex reasoning tasks.

Works focused on solving logic puzzles typically involve a mapping from natural language to logic formalism. This process often includes problem simplification techniques, such as tailoring the puzzle to a specific domain, restricting natural language input to a certain form, or assuming additional inputs like enumerated types. ? (?) employ a specialized automated multi-stage parsing process to convert natural language text into an intermediate form called Semantic Logic, which is then converted into First Order Logic to finally evaluate on law school admissions tests (LSAT) and the Graduate Records Examination (GRE). ? (?) manually encodes the “Jobs Puzzle” in a few different logical formalisms and compare them. Puzzler (?) uses a general link parser to translate puzzles into to the Alloy language for solving, primarily through an automated process, albeit with assumed types. LogicSolver (?) follows a similar approach to Puzzler but replaces Alloy with a custom solver and conducts a more comprehensive evaluation.

Several works utilize translations into the language of answer set programming (ASP) (?; ?). ? (?) addresses the “Jobs Puzzle” by representing the problem using controlled natural language (?), which can be further turned into ASP. ? (?) employ a $\lambda$-calculus-based approach and trains a model that converts a manually simplified version of natural language clues into ASP rules for solving Zebra puzzle-type logic puzzles. ? (?) train a maximum entropy-based model to extract relations for each clue, which are then converted into a common ASP rule format, where a stable model corresponds to the puzzle solution. LGPSolver (?) uses DistilBERT, a transformer-based model, as a classifier that can distinguish between representative rule types. With the clue classification, the authors use a hand-crafted clue to Prolog translation (as opposed to ASP) and compute the solution. The works mentioned involve some combination of manual processing and/or brittle problem-specific translations. Our work distinguishes itself by being both fully automated and featuring a general pipeline, leveraging the extensive translation capacity available from LLMs.

ASP programs are typically written following the Generate-Define-Test structure, which generates potential solutions (Generate) and eliminates invalid ones based on certain constraints (Test). The Generate portion usually includes choice rules, while the Test portion consists of a set of constraints that prune out invalid solutions. An additional part of the program, the Define portion, includes necessary auxiliary predicates that are used in the Test portion.

The first step in the pipeline is to extract constants or entities from the given story along with their corresponding categories. To accomplish this, we invoke GPT-3 using Prompt C, which consists of three parts: instruction, examples, and a query.

Line 1 provides a general instruction for the task of extracting objects and directing GPT-3 to generate them in the form of “category: constant₁; …; constant_n.” Then, two examples follow: Lines 6-8 for Problem 1 specified in Lines 3-4, and Lines 17-20 for Problem 2 specified in Lines 10-15. By replacing Line 23 ($\langle$story$\rangle$) with a new example story and invoking GPT-3 with the above prompt, a new list of categories and constants for that story is generated, as with the previous two examples.

The above two examples are chosen to cover two cases of object extraction. For the N-Queens problem, the constants $1,\dots,8$ are not described in the Problem 1 statement (Line 4) but can be inferred. For the second puzzle, however, all constants in Lines 18-20 are mentioned in the example story provided in Lines 11-15.

The second puzzle is also intentionally selected to give an example for GPT-3 so that certain constants (e.g., $225) can be turned into valid integers (e.g., 225) so that arithmetic can be applied correctly later when generating rules later on, while others should be surrounded by double quotes. We experimented with various prompts to instruct GPT-3 to generate all non-numeric constants in lowercase and replace special characters with underscores. However, GPT-3 was unable to strictly adhere to these instructions and consequently made more errors.

The next step in the pipeline is to generate predicates $p$ that describe the relations among the extracted constants. We use GPT-3 on the Prompt P below.

Line 1 is a general instruction describing the task of predicate generation, and that the generated predicates should follow the form of “predicate(X₁, …, X_n)” where each X_i is a distinct variable that represents a category of constants.

Again, the two examples follow. Lines 3–4 are a copy of the first example in Lines 3–8 of Prompt C (where we omit Lines 4–8 from Prompt C to reduce the space). Lines 6–9 continue the first example, where it now generates the predicates with variables as arguments following the instruction. It also contains two comments (starting with symbol %). The first comment in Line 7 recalls the categories of constants and assigns a different variable to each category. The second comment in Line 8 gives the English reading of the predicate and variables, and emphasizes the link between each variable and a category of constants. Similarly, Lines 11–17 present the second example.

Next, the story and constants are given for the third problem and GPT-3 is prompted to generate the predicate for that example, given the general instruction and the preceding two examples.

Given the extracted constants $c$ and generated predicates $p$, the next step in the pipeline is to generate ASP rules $\Pi$, consisting of the Generate part and the Define&Test part.

The Generate part of an ASP program defines all possible mappings of constants from different categories. This is done by choice rules. In this step, an ASP program $\Pi_{generate}$ is obtained by calling GPT-3 with Prompt R1.

In the above prompt, $\langle$constants$\rangle$ and $\langle$predicates$\rangle$ are to be replaced for a new example. GPT-3 generates facts and choice rules following the last line of the prompt.

The task in this step is to write facts and choice rules based on the generated constants and predicates. Since this step doesn’t require the details of the story, we omit the story from the prompt to avoid unnecessary noisy information being included in the prompt. Each example only consists of constants, predicates, and ASP rules to be generated, i.e., facts and choice rules.

Similar to the previous prompts, Line 1 is a general instruction, Lines 3–20 provide an example, and Lines 22–28 are for the queried example. The example ASP rules in Lines 14–20 contain comments (Lines 14 and 19), which will also be generated for the queried example and help to gather semantic information before generating a rule.

The Define&Test part of an ASP program contains constraints that “weed out” the stable models that do not correspond to valid answers. This step takes as input the puzzle story $q$, constants $c$, and predicates $p$: semantically, the ASP rules represent the content in story $q$ while, syntactically, the ASP rules must be formed by the extracted constants $c$ and generated predicates $p$. The ASP program $\Pi_{define\_test}$ is obtained by calling GPT-3 with Prompt R2.

Lines 1–8 are a general instruction describing the task of $\Pi_{define\_test}$ generation and provides two rule forms for the target ASP rules. The first rule form

says that “$C_{1}$ or … or $C_{m}$ is true if $L_{1}$ and … and $L_{n}$ are true.” Here, each $L_{i}$ is a literal and each $C_{i}$ is a comparison in the input language of clingo, e.g., $A>B$, $A=B+3$, etc. The second rule form

additionally restricts that “exactly $k$ of $\{C_{1},\dots,C_{m}\}$ must be true.” In principle, the first rule form is enough to represent various constraints. However, since the second rule form is syntactically closer to certain complex sentences related to cardinality, e.g., “either … or …”, “neither … nor …”, or “no … is …”, etc, we found that GPT-3 works much better when we also include the second rule form.

In the Constant Extraction step (Section 3.1), GPT-3 may extract the names of the objects as they appear in the puzzle story, such as $225, Sue Simpson, and 8:30 AM, which do not conform to the syntax of the input language of answer set solver clingo. Also, GPT-3 applies arithmetic computations (e.g., L1=L2+3) to constants surrounded by double quotes (e.g., L2 is constant "9 inches") instead of constants that are integers (e.g., L2 is constant 9).

A rule-based post-processing could be applied to turn them into the right syntax, but alternatively, we employ GPT-3 to generate syntactically correct forms. We found that this method requires significantly less efforts and is more general because GPT-3 applies the constant formatting correctly even for unforeseen formats using some “common sense,” which is lacking in the rule-based approach. We use the following prompt for this.

The Constant Formatting step is done by calling GPT-3 with the following prompt, where $\langle$constants$\rangle$ at the end of the prompt is replaced by the original (extracted) constants $c$ obtained by the Constant Extraction step (Section 3.1). The GPT-3 response in this step is the updated constants $c$, serving as an input to other steps in the pipeline.

Sometimes sentences may need to be paraphrased before an LLM can correctly generate rules from them. The Sentence Paraphrasing step provides the opportunity to not only simplify or formalize the sentences from the original question but also add the hidden information assumed to underlie the question. For example, the following sentence

is one clue in the example question in Section 3. The correct translation requires an LLM to turn the above sentence into at least 3 ASP rules, which would be hard for the current LLMs (e.g., GPT-3). Instead, we can ask GPT-3 to first paraphrase such kind of sentence into simpler ones below.

The Sentence Paraphrasing step is done by calling GPT-3 with the following prompt, where $\langle$sentences$\rangle$ at the end of the prompt is replaced by the numbered sentences in the queried puzzle story $q$, and the GPT-3 response in text is used to replace the original sentences in $q$. This prompt is dedicated to the logic puzzles from Puzzle Baron and only paraphrases one kind of sentence in the form “of A and B, one is C and the other is D.”

If we describe Sudoku problem with the following story $q$

our pipeline generates the following ASP program $\Pi$.

This ASP program $\Pi$ is almost correct except that the red part in Line 16 of $\Pi$ should be

since the row and column indices start from 1. This formula seems too difficult for GPT-3 to notice and generate unless some examples are provided . On the other hand, if we slightly adjust Lines 7–8 of Prompt C (Section 3.1) to make the indices start from 0, then the generated ASP program $\Pi$ becomes correct as Lines 2–3 of $\Pi$ are changed to the following facts.

GPT-4 also fails to generate the last rule correctly, although it makes a different mistake.

The Jobs Puzzle studied in (?) asks one to assign 8 different jobs to 4 people while satisfying the given constraints. The full puzzle $q$ is shown below.

This puzzle was considered a challenge for logical expressibility and automated reasoning (?).

To apply our method to the Jobs Puzzle, some paraphrasing was needed before the Define&Test part of rule generation. We manually paraphrased the above puzzle to the following

by turning clues 1–4 as background story, clarifying clues 6, 8, and 9, and adding a few hidden clues numbered 10.X at the end.

As for the prompts, we only need to update Line 1 of Prompt R1 to the following to allow for {...}=k in a rule.

Finally, GPT-3 generates the following ASP program:

which is almost correct with a single mistake in translating clue 10.1. If we just replace this constraint (in red) with

the corrected ASP program has exactly one stable model, which is the correct solution to the Jobs Puzzle.

Similarly, GPT-4 also failed to generate a completely correct ASP program. It also couldn’t generate a correct rule for constraint 10.1, and furthermore failed to produce the gender category in constant extraction step Prompt C), missing “gender: "male"; "female".”