Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning

In plain words

Language models read a logic puzzle written in English well, but they often make mistakes when they try to reason through it step by step in text. Logic-LM splits the work. The model only rewrites the puzzle into a strict formal notation: a list of facts, rules and a question. A classic logic engine then does the reasoning, and it gives the same answer every time. If the engine rejects the formal version because of a syntax or logic error, the error message goes back to the model, which fixes its rewrite and tries again.

The paper tests this on five sets of logic puzzles, mostly deduction questions: which statements follow from the given premises, or which assignment satisfies a set of constraints. Each kind of puzzle gets its own engine. The authors' idea is that translating a puzzle into formal notation is easier for a model than solving it in prose.

All results are the authors' own. The card below records where the paper's text, its tables and its released code disagree.

TL;DR

Logic-LM is a three-part pipeline: an LLM translates a natural-language problem into one of four formal languages §3.1 tab. 1, a deterministic solver (Pyke, Prover9, python-constraint or Z3) executes it §3.2, and failing programs can be rewritten using the solver's error message §3.3. With GPT-4 it beats standard prompting on all five datasets and chain-of-thought on four; PrOntoQA is the exception tab. 2. The released code differs from the paper in several places, including the fallback when no answer is produced. See Paper vs code.

Problem

Standard prompting and chain-of-thought (CoT) ask the LLM to reason in natural language. The paper argues that this flexibility brings unfaithful reasoning and hallucinations §2. Logic programming systems and program-generation methods such as PAL are not a good fit for non-linear logical reasoning, such as hypothesising, case analysis and elimination §2 §4.1.

The framework assumes the answer is faithful only "as long as the problem formulation is correct" §3. Its applicability is limited by what the chosen solver can express; not every problem fits first-order logic [Limitations].

Method

Inputs are a problem P in natural language and a goal G, either multiple choice or free-form §3. Three modules do the work: a Problem Formulator, a Symbolic Reasoner and a Result Interpreter fig. 1 §3. A Self-Refiner loops back from the reasoner to the formulator §3.3. The paper's argument is that the model then only has to represent the problem, not solve it §3.

Formalisms and solvers §3.1 §3.2 tab. 1 (table summarised by us):

Steps.

1. Problem Formulator §3.1. The LLM is given the grammar of the chosen language and few-shot demonstrations. It names the entities, facts and rules in the problem and writes them in that grammar. Demonstrations use the format symbolic_formula ::: NL_statement to tie each formula to its source sentence §3.1. Full prompts are in app. C.
2. Symbolic Reasoner §3.2. The solver runs the program. Pyke applies forward and backward chaining §3.2, LP System. Prover9 converts first-order formulas to conjunctive normal form and resolves them §3.2, FOL Prover. python-constraint searches for assignments §3.2, CSP Solver. Z3 checks satisfiability §3.2, SAT Solver.
3. Self-Refiner §3.3 fig. 3. If the solver returns an execution error, the LLM gets the faulty program, the solver's error message and demonstrations of common errors. This repeats until no error is returned or a revision limit is reached. The paper does not state the limit in the text; the figure shows zero to three rounds §4.4.
4. Result Interpreter §3.4 app. D. The solver's output is mapped back to an option. The paper says rule-based and LLM-based interpreters were both designed §3.4; its appendix describes rule-based mappings for all five datasets app. D.
5. Fallback §4.1. When the program cannot be executed, the paper uses chain-of-thought to predict the answer §4.1.

# Logic-LM inference for one problem  [§3]
# Input:  problem (text), goal (question and options)
# Output: option letter, or a fallback guess

def logic_lm(problem, goal, formulator, solver, max_revisions):
    # Pick the formal language from the problem type  [§3.1] [tab. 1]
    language = formalism_for(problem.kind)
    # Few-shot translation of problem and goal  [§3.1] [app. C]
    program = formulator.translate(problem, goal, language)
    # Run the deterministic solver  [§3.2]
    answer, error = solver.execute(program)
    for _ in range(max_revisions):
        if answer is not None:
            break
        # Rewrite the program using the solver's error message  [§3.3]
        program = formulator.refine(program, error)
        answer, error = solver.execute(program)
    if answer is None:
        # Paper: CoT fallback; released code: random guess  [§4.1]
        return fallback(problem, goal)
    # Map the solver's result onto an option letter  [§3.4] [app. D]
    return option_for(answer, goal)

Prover9 verdict for first-order logic, as implemented in the released code. The paper describes the same logic in prose §3.2 app. D:

# FOL verdict with Prover9  [§3.2] [app. D]
# Input:  premises (list of FOL formulas), conclusion (FOL formula)
# Output: 'True', 'False' or 'Unknown'
# [code: models/symbolic_solvers/fol_solver/prover9_solver.py#L55-L70]

def fol_verdict(premises, conclusion):
    # Try to prove the conclusion from the premises
    if prove(premises, conclusion):
        return 'True'
    # Otherwise try to prove the negated conclusion
    if prove(premises, negate(conclusion)):
        return 'False'
    # Neither was proved
    return 'Unknown'

Constraint-satisfaction option check, as implemented in the released code. The paper says the option value must be "in the generated array" app. D:

# CSP option check  [app. D]
# Input:  all solutions (list of dicts), variable name, option value
# Output: True if the option holds in every solution
# [code: models/symbolic_solvers/csp_solver/csp_solver.py#L114-L137]

def option_holds(solutions, variable, value):
    # Collect the values the variable takes across all solutions
    seen = {solution[variable] for solution in solutions}
    # Accept only when that set is exactly the option's value
    return seen == {value}

Hyperparameters

Results

Author-reported. Setup: accuracy on the test set of each dataset, with each base LLM under three settings: standard prompting, chain-of-thought, and Logic-LM without self-refinement §4 tab. 2.

Source: tab. 2. "davinci-003" is text-davinci-003, and "ChatGPT" is gpt-3.5-turbo.

Execution analysis with and without self-refinement, for GPT-3.5 and GPT-4. The table header says only "GPT-3.5" tab. 3 §4.2 §4.4. Exe_Rate is the share of programs the solver executes; Exe_Acc is accuracy on those programs:

Source: tab. 3. The paper reports a mean Exe_Rate gain of 5.01 points from self-refinement §4.4; the ten Exe_Rate differences in the table average to that figure.

Robustness on ProofWriter §4.3 fig. 2: Logic-LM outperforms CoT by 7.1%, 5.0%, 12.7%, 20.0% and 39.4% on the five depth subsets. The paper does not say whether these are percentage points or relative gains.

Headline averages. The abstract gives 39.2% over standard prompting and 18.4% over CoT. Section 4.1 attributes the 39.2% to GPT-3.5 alone §4.1. Our recomputation from Table 2 (our arithmetic, not the paper's) is that the abstract figures equal the mean, across the three base LLMs, of the per-dataset relative gain of Logic-LM over each baseline. For GPT-3.5 alone the same calculation gives 45.2% (ChatGPT) and 47.5% (text-davinci-003) over standard, and 25.1% and 19.6% over CoT. The GPT-4 figures in §4.1 reproduce with this method: 24.98% over standard and 10.44% over CoT §4.1 tab. 2.

Paper vs code

Repository: https://github.com/teacherpeterpan/Logic-LLM at commit d29f1e5e7203e8826cb9c41ba3003e43dc0b9d34, MIT LICENSE. The paper links this repository in its abstract [abstract].

• Fallback when no answer. The paper falls back to CoT §4.1. The code's default is a random guess logic_inference.py backup_answer_generation.py. CoT is used only with --backup_strategy LLM, which loads saved baseline results README.md. Which strategy produced Table 2 is not stated.
• What triggers refinement. The paper refines on execution errors §3.3. The code also refines on parsing errors, passing the message "Parsing Error" self_refinement.py. Errors with the message "No Output" are not refined self_refinement.py.
• Which datasets can be refined. The code supports refinement only for FOLIO and AR-LSAT self_refinement.py. The code raises a KeyError for any other dataset at construction self_refinement.py. The "with" rows of Table 3 for PrOntoQA, ProofWriter and LogicalDeduction therefore cannot have come from this release tab. 3.
• Refinement LLM. The paper does not name the model. The code always uses gpt-4 for refinement, whatever model generated the program self_refinement.py.
• Revision count. The paper says "the maximum number of allowable revisions" without a value §3.3. The code runs up to three rounds, each reading the previous round's file self_refinement.py self_refinement.py.
• Result interpreter. The paper says rule-based and LLM-based interpreters were both designed §3.4, but its appendix describes only rule-based mappings app. D. The released code has no LLM-based interpreter; the solver wrappers map answers in answer_mapping logic_inference.py.
• ProntoQA unknowns. The paper says Pyke returns "Unknown" when it cannot decide app. D. For ProntoQA the code maps anything other than a proved value to option B, which is False pyke_solver.py. ProofWriter maps unknown to C pyke_solver.py.
• Constraint-satisfaction rule. The paper says an option is checked for membership in the generated array app. D. The code accepts an option only when its variable takes exactly that one value in every solution csp_solver.py. This is a stricter entailment test.
• AR-LSAT prompt. For gpt-4 the code uses a separate, longer AR-LSAT prompt logic_program.py. The paper does not mention a second prompt.
• Split. The paper reports test-set results §4. The README's commands default to the dev split README.md README.md README.md. The released ProntoQA folder holds only dev.json dev.json, so which split the paper's 500 examples come from is not stated.
• Consistent. Temperature 0 matches the paper §4 utils.py. The FOLIO and AR-LSAT refinement loops follow the paper's description in outline §3.3 self_refinement.py.

Pitfalls

• Solver failure has three shapes. A program can fail to parse (flag == False, backup), fail during execution (an exception, a timeout or "No Output", which give a backup and a refinement message), or run cleanly and map to no option (CSP, which gets no backup) logic_inference.py. Count them separately when you reproduce the paper; the paper does not report the split.
• Unknown answers are not all treated alike. Pyke returns no value when it cannot prove the query, and the ProntoQA mapping turns that into B pyke_solver.py. Prover9 needs both proof attempts to fail before answering Unknown prover9_solver.py. The code does not separate a timeout from a failed proof; a timeout therefore probably counts as Unknown. We did not verify this against the solver library.
• Timeouts are short and unreported. The Z3 call allows 1.0 second, including Python start-up sat_problem_solver.py. On a loaded machine that may time out and force a backup. Prover9 allows 10 seconds prover9_solver.py and python-constraint 20 seconds csp_solver.py.
• Silent drops in program generation. The generator catches every exception and skips that example logic_program.py logic_program.py. Check that the output has one entry per test item before you score it.
• Parts of the output are dropped silently. The Pyke wrapper drops any fact that contains $x pyke_solver.py. The Prover9 wrapper uses only the first conclusion line prover9_solver.py. The Pyke flag ends up True whenever the two files are written, so the validation result does not reject a program pyke_solver.py pyke_solver.py.
• Some errors abort the whole run. The CSP option lookup assumes each option starts with a label followed by ) csp_solver.py. The Z3 mapping raises KeyError on unexpected output sat_problem_solver.py. Both are called outside any try block in the driver logic_inference.py, so one bad program stops the run.
• Empty CSP answers are scored as wrong, not backed up. If no option is entailed, the mapped answer is None but the status is still "success" csp_solver.py logic_inference.py. The evaluator scores None as incorrect evaluation.py evaluation.py.
• Shared cache directories. Pyke writes fact and rule files to a cache directory inside the package pyke_solver.py pyke_solver.py. The Z3 wrapper writes tmp.py to a similar directory sat_problem_solver.py. Parallel runs in one checkout can overwrite each other's files. Several paths are relative, so run from the repository root prover9_solver.py.
• Bundled Prover9 has its own licence. The repository ships Prover9 sources under GPL-2.0 COPYING. This card quotes nothing from them. Check that licence before you redistribute the binary.
• Refinement costs an extra model. Each refinement round calls gpt-4 for each failing program, up to three rounds self_refinement.py self_refinement.py.
• Depth labels disagree in the robustness section. The text lists subsets as 0, at most 1, at most 2, at most 3 and at most 5 hops §4.3. The result sentence names them depth-0, depth-1, depth-2, depth-4 and depth-5 §4.3.
• Dataset sizes disagree. AR-LSAT has 231 questions in §4 and 230 in the appendix table and the README §4 tab. 5 README.md.
• Some §4.1 claims could not be reproduced. The Logic-LM over CoT gains of +21.85% (FOLIO), +45.67% (LogicalDeduction) and +24.14% (AR-LSAT) do not follow from Table 2 by the averaging method above. The three CoT-over-standard figures (11.75%, 9.41%, −3.2%) do follow from it, as the mean across the three base LLMs.

Lineage

• Builds on: the SAT grammar is taken from SatLM §3.1; Prolog-style logic programming §3.1; the refinement idea extends code-debugging work that teaches LLMs to fix their own programs with few-shot demonstrations, namely self-debugging and self-refine §3.3.
• Compared against: standard in-context prompting and chain-of-thought prompting §4.
• Superseded by: not known from content in this wiki.