PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Chinmay Mittal, Krishna Kartik, Mausam, Parag Singla

arXiv:2402.02611v3cs.AIcs.CLcs.LG

TL;DR

This paper asks whether LLMs can solve computationally intensive first-order combinatorial problems. It introduces FCoReBench and SymPro-LM, which combines LLM-generated programs with symbolic solvers. SymPro-LM outperforms few-shot prompting and Logic-LM on FCoReBench and performs well on additional logical-reasoning datasets.

  • Problem

    The paper investigates whether LLMs can solve computationally intensive first-order combinatorial problems, an area with limited work exploiting their varying-size problem structure.

    Source: §1 · pp. 1–2

  • Method

    SymPro-LM uses an LLM-generated program to translate any-size problem instances into solver constraints, obtain symbolic solutions, and format outputs without inference-time LLM calls.

    Source: §1 · p. 2, §5.1 · p. 7

  • Results

    On FCoReBench, SymPro-LM improves over few-shot prompting by 54.04% and Logic-LM with refinement by 44.86%, and outperforms baselines on two additional datasets while competitive on a third.

    Source: §1 · p. 2, §7 · p. 10

  • Takeaways & Limitations

    The results support integrating LLMs with symbolic solvers through programs for first-order combinatorial reasoning problems.

    Source: §1 · p. 2

    FCoReBench covers a limited set of problems, assumes fixed serialized input and output representations, and some solver-language encodings can be complicated.

    Source: §9 · p. 14

Abstract

from arXiv · show

Can the large language models (LLMs) solve challenging first-order combinatorial reasoning problems such as graph coloring, knapsack, and cryptarithmetic? By first-order, we mean these problems can be instantiated with potentially an infinite number of problem instances of varying sizes. They are also challenging being NP-hard and requiring several reasoning steps to reach a solution. While existing work has focused on coming up with datasets with hard benchmarks, there is limited work which exploits the first-order nature of the problem structure. To address this challenge, we present FCoReBench, a dataset of 40 such challenging problems, along with scripts to generate problem instances of varying sizes and automatically verify and generate their solutions. We first observe that LLMs, even when aided by symbolic solvers, perform rather poorly on our dataset, being unable to leverage the underlying structure of these problems. We specifically observe a drop in performance with increasing problem size. In response, we propose a new approach, SymPro-LM, which combines LLMs with both symbolic solvers and program interpreters, along with feedback from a few solved examples, to achieve huge performance gains. Our proposed approach is robust to changes in the problem size, and has the unique characteristic of not requiring any LLM call during inference time, unlike earlier approaches. As an additional experiment, we also demonstrate SymPro-LM's effectiveness on other logical reasoning benchmarks.

1 Introduction

The paper examines whether LLMs can solve computationally intensive, first-order combinatorial problems and introduces FCoReBench and SymPro-LM to study them. SymPro-LM combines LLM-generated programs with symbolic solvers and substantially outperforms prompting and tool-augmented baselines.

1 Introduction

  • The paper frames its evaluation around whether LLMs can solve computationally intensive combinatorial problems directly or with symbolic-AI assistance.Examples include Sudoku, knapsack, graph coloring, and cryptarithmetic.Source: §1 · pp. 1–2
  • FCoReBench contains 40 first-order combinatorial problems, with scripts to generate instances of varying sizes and verify or generate solutions.The evaluation includes 1,354 test instances and 596 smaller solved training instances; most problems are NP-hard and require extensive planning and search.Source: §1 · p. 2
  • SymPro-LM combines LLM-generated programs with symbolic solvers, and its generated program can handle new instances of any size without inference-time LLM calls.The program converts an instance into a symbolic representation, passes it to a solver, and formats the returned solution.Source: §1 · p. 2
  • SymPro-LM outperforms few-shot prompting by 21.61, PAL by 3.52, and Logic-LM by 16.83 percentage points on FCoReBench with GPT-4-Turbo.Four rounds of feedback from solved examples yield a further 21.02 percentage-point gain over SymPro-LM without feedback.Source: §1 · p. 2
  • The paper evaluates prompting techniques for first-order combinatorial problems and presents SymPro-LM as an approach effective on these problems and other datasets.Source: §1 · p. 3

2 Related Work

Prior work spans neuro-symbolic systems, LLM prompting and tool use, and logical-reasoning benchmarks. The paper distinguishes FCoReBench through its focus on computationally hard problems with multiple instances and varying sizes.

2 Related Work

  • Prior neuro-symbolic approaches use specialized, typically non-size-invariant modules trained on large datasets, whereas SymPro-LM generalizes across sizes with few solved instances.Source: §2 · p. 3
  • The related work situates SymPro-LM among prompting and tool-augmented methods, including approaches that use interpreters or symbolic solvers.It describes PAL as interpreter-based and Logic-LM and SAT-LM as solver-integrating methods.Source: §2 · p. 3
  • Existing logical-reasoning datasets generally provide a single instance per problem, while FCoReBench covers computationally hard first-order combinatorial problems.NLGraph covers graph problems with eight problems, and NPHardEval has ten; all NP-hard problems in those datasets also appear in FCoReBench.Source: §2 · p. 4

3 Problem Setup: Natural Language First-order Combinatorial Reasoning

The setup represents a first-order combinatorial problem through legal input and output spaces and constraints on valid pairs. Natural-language descriptions and serialized examples define the task of mapping an input to a valid output.

3 Problem Setup: Natural Language First-order Combinatorial Reasoning

  • A first-order combinatorial problem is specified by legal input instances, legal outputs, and constraints that each input-output pair must satisfy.For Sudoku, the inputs are partially filled grids, outputs are completed grids, and constraints include row, column, and box rules plus persistence of input cells.Source: §3 · p. 4
  • The problem components and examples are communicated to the language model through natural-language descriptions and serialized input-output data.The Sudoku illustration shows rules, input-output formats, and sample pairs.Source: §3 · p. 4, Figure 2 · p. 4
  • The task is to learn a function that maps any serialized input to a serialized solution satisfying the problem constraints.Source: §3 · p. 5

4 FCoReBench: Dataset Construction

FCoReBench comprises 40 problems selected for natural-language describability and feasible instance generation. The authors created and checked problem descriptions and scripts, then released varying-size training and test instances.

4 FCoReBench: Dataset Construction

  • The authors selected 40 computationally challenging problems that could be described in natural language and whose datasets could be created with reasonable programming effort.Thirty are known NP-hard; the set includes graph-, grid-, set-, real-world, and miscellaneous problems.Source: §4 · p. 5
  • Two authors wrote and verified natural-language instructions, checking that rewritten rules preserved meaning and were unambiguous.A third annotator solved all training instances correctly, providing a human-comprehension check for the descriptions.Source: §4 · p. 5
  • The authors generated instances programmatically and developed solver and verification scripts, which were checked by another author and tested on manually curated cases.Source: §4 · pp. 5–6
  • FCoReBench provides 596 smaller solved training instances and 1,354 test instances, with scripts for generating and verifying instances of varying complexity.The scripts verify candidate solutions, avoiding the need to compute all solutions for large test instances.Source: §4 · p. 6

5 SymPro-LM

SymPro-LM has an LLM generate an input-agnostic program that translates instances into solver constraints and converts solver assignments back into outputs. It refines that program with solved examples and can restart generation to select the best candidate.

5.1 Our Approach

  • SymPro-LM combines program generation with symbolic solving: an LLM writes an input-agnostic program that translates any-sized inputs into solver constraints and formats the solver’s assignment as the output.Unlike direct LLM-to-solver approaches, the program mediates both the conversion to solver representation and recovery of the requested output format.Source: §5.1 · p. 7
  • Solved examples trigger feedback when execution fails, the solver times out, or the predicted output is wrong; the LLM uses the error and example to revise the program.The process repeats until the training examples are solved correctly or a maximum number of feedback rounds is reached.Source: §5.1 · pp. 7–8
  • Because one feedback run may not solve every training example, SymPro-LM restarts generation and selects the program with the highest training-set accuracy.Each restart generates a new program and continues its own feedback process.Source: §5.1 · p. 8
  • For non-first-order datasets, SymPro-LM generates a separate program per test instance, forgoing solved-example feedback and correcting only syntactic mistakes.The program extracts facts or rules, passes them to a symbolic solver, and formats the solver’s answer.Source: §5.1 · p. 8

6 Experimental Setup

The experiments compare SymPro-LM with LLM-based baselines across FCoReBench and three other logical-reasoning datasets, examining feedback, multiple runs, and error patterns. They use three LLMs and evaluate verified solution accuracy.

6 Experimental Setup

  • The experiments compare SymPro-LM with prompting, PAL, Logic-LM, and Tree-of-Thoughts; ToT is evaluated separately on a subset because it requires substantial prompt engineering and is estimated to cost 2–3 orders of magnitude more.The study uses Z3 for Logic-LM and SymPro-LM and Python for PAL.Source: §6 · p. 8
  • For PAL and SymPro-LM, refinement uses five runs with four rounds of solved-example feedback per problem; Logic-LM receives four rounds of feedback for syntactic constraint errors.SAT-LM is omitted because the authors consider it conceptually similar to concurrently proposed Logic-LM.Source: §6 · p. 9
  • The evaluation uses GPT-4-Turbo, GPT-3.5-Turbo, and Mixtral 8x7B, with prompts containing each problem’s rules, input-output format, and two solved examples.Few-shot prompting and Logic-LM use temperature 0; PAL and SymPro-LM use 0.7 to sample runs.Source: §6 · p. 9
  • Solutions are checked by problem-specific verification scripts, and FCoReBench performance is the macro-average of test-instance accuracy across problems.Each test instance receives binary marking: correct or incorrect.Source: §6 · p. 9
  • The study also evaluates LogicalDeduction, ProofWriter, and PrOntoQA, where methods run separately on each test instance because these datasets are not first-order.Chain-of-Thought prompting is included as a baseline for these datasets.Source: §6 · p. 9

7 Results

On FCoReBench, SymPro-LM outperforms the reported prompting and solver baselines, while feedback, multiple runs, and programmatic handling help address errors and changing instance sizes. It also performs well on two additional reasoning benchmarks, with a different pattern on PrOntoQA.

7 Results

  • 54.04% average improvement over few-shot prompting and 44.86% over Logic-LM (with refinement) are reported for SymPro-LM on FCoReBench.The comparison is for GPT-4-Turbo; few-shot prompting solves less than a third of the problems.Source: Table 1 · p. 10, §7 · p. 10
  • As instance size grows, smaller Logic-LM models make more syntactic mistakes; larger models make fewer, but their constraints can remain semantically incorrect despite feedback.The passage describes Logic-LM’s performance on FCoReBench with refinement.Source: Table 2 · p. 10, §7 · p. 10
  • 16.97%: SymPro-LM outperforms PAL on FCoReBench with refinement; PAL’s generated brute-force programs can be incorrect or slow, and the authors hypothesize declarative programs are easier to correct.The authors also report larger feedback and rerun gains for SymPro-LM than PAL.Source: §7 · pp. 10–11, Table 4 · p. 11
  • As instance size increases, SymPro-LM and PAL are relatively robust while few-shot prompting and Logic-LM decline sharply; programmatic loops and conditionals support size-invariant solving without inference-time LLM calls.PAL may lose performance when its programs are too inefficient to find a solution within the time limit.Source: §7 · pp. 10, 12, Figure 4 · p. 11
  • 21.02% improvement follows four feedback rounds; five runs add 11.41%, while gains from adding solved examples tend to saturate at seven.The authors report that additional examples beyond seven uncover no new errors to correct.Source: Figure 5 · p. 12, §7 · p. 12

7.1 Results on Other Datasets

  • On ProofWriter and LogicalDeduction, SymPro-LM outperforms the other baselines, while PAL and CoT are marginally better on PrOntoQA, whose forward-chaining style aligns with their reasoning.The authors report that symbolic solvers are less useful for PrOntoQA, though SymPro-LM remains competitive.Source: Table 6 · p. 12, §7.1 · pp. 12–13, Figure 6 · p. 13

8 Discussion

SymPro-LM’s results fall into three groups: problems solved directly, problems solved after feedback, and problems where feedback does not reach perfect accuracy. The groups distinguish straightforward rule-to-code translation from harder constraint encoding.

8 Discussion

  • 8 of 40 problems reached 100% accuracy without feedback, where translating rules directly into solver constraints is sufficient.Examples include vertex-cover and latin-square.Source: §8 · p. 13
  • 20 problems reached 100% accuracy after feedback, typically requiring reasoning to encode rules that do not map directly to code.Auxiliary variables or combinations of primitives can be needed; feedback helped GPT-4-Turbo correct missed or incorrectly encoded constraints.Source: §8 · pp. 13–14
  • For 12 problems, accuracy remained below 100% despite feedback or multiple runs, often because natural-language constraints were difficult to encode in SMT.Number-link and hamiltonian path are examples; GPT-4-Turbo struggled to encode path existence as SMT constraints.Source: §8 · p. 14

9 Conclusion and Limitations

This section summarizes SymPro-LM’s reported performance and limitations, and describes prompts that guide search by proposing board moves and estimating solution reachability for pruning.

9 Conclusion and Limitations

  • SymPro-LM combines LLM-generated executable code, program interpreters, and symbolic solvers, and achieves superior performance on FCoReBench and existing benchmarks.The paper also reports that existing tool-augmented techniques such as Logic-LM and PAL fare poorly.Source: §9 · p. 14
  • SymPro-LM struggles when conversion to symbolic representation is not straightforward, and simple feedback strategies do not improve reasoning in these cases.Exploring ways to alleviate these difficulties is identified as future work.Source: §9 · p. 14
  • The authors identify expanding FCoReBench, addressing fixed serialized representations and difficult solver-language encodings, and evaluating vision-language models on image inputs as future work.The method relies on LLM pre-training to encode problems without training or fine-tuning.Source: §9 · p. 14

B.6.1 Propose Prompt

  • The propose prompt asks for up to three next steps, each on a new line, or only END if the board is full or no valid step exists.The board rules require replacing zeros with numbers from 1 to n, preserving existing nonzero entries, and placing each number exactly once in every row and column.Source: §B.6.1 · p. 31

B.6.2 Value Prompt

  • The value prompt evaluates each search node as sure, likely, or impossible to estimate whether it can reach a valid solution and prune the search tree.An empty board is labeled sure, while a partially filled board with no violated constraints is labeled likely.Source: §B.6.2 · pp. 31–32
  • The value prompt requests a two-line response containing reasoning followed by one of the labels Sure, Likely, or Impossible.It asks the model to judge the likelihood of reaching a valid solution from a partially filled board.Source: §B.6.2 · p. 32

B.4.1 Programming Errors

This block gives error-specific feedback prompts, describes the zero-shot evaluation setup for FCoReBench, and outlines the Tree of Thoughts search procedure used on three problems.

B.4.1 Programming Errors

  • Programming-error feedback asks the model to rewrite code after a runtime error, while verification-error feedback supplies the input, incorrect output, and a correct output.The verification prompt then asks the model to rewrite the code and fix the mistake.Source: §B.4.1 · p. 29, §B.4.2 · p. 29

B.4.3 Timeout Error

  • Timeout feedback asks the model to rewrite and optimize code when execution exceeds the time limit.Source: §B.4.3 · p. 29

C.1 FCoReBench

  • FCoReBench methods are evaluated zero-shot; PAL and SymPro-LM also receive 10 solved examples for feedback.The authors choose zero-shot because demonstrations of highly related instances would be unfair in these structured problems.Source: §C.1 · p. 32

C.1.1 ToT prompting

  • Tree of Thoughts uses breadth-first search with propose and value prompts on three problems, pruning each depth to five nodes and proposing at most three next steps.Search ends when a terminal node is among the best nodes or reaches the instance’s maximum search depth.Source: §C.1.1 · p. 33

C.2 Other Datasets

The block describes evaluation on three logical-reasoning datasets, inference-time comparisons, experimental hardware, and illustrative generated programs. SymPro-LM is reported to perform much better than PAL on inference time for selected FCoReBench problems.

C.2 Other Datasets

  • On three external datasets, SymPro-LM generates Python to parse inputs, set up solver constraints, call a solver, and produce answers; execution errors trigger a chain-of-thought fallback.Accuracy is the metric, and prompts and examples follow the Logic-LM evaluation where specified.Source: §C.2 · p. 33

C.2.1 PrOntoQA

  • PrOntoQA evaluation uses the hardest fictional-characters version and its 5-hop subset.The dataset tests whether a new fact is true or false.Source: §C.2.1 · p. 33

C.2.2 ProofWriter

  • ProofWriter evaluation uses the open-world-assumption depth-5 subset, with 600 test examples sampled to balance the labels PROVED, DISPROVED, and UNKNOWN.Source: §C.2.2 · p. 34

C.2.3 LogicalDeduction

  • LogicalDeduction evaluation uses the full test set of 300 examples, mostly requiring deduction of object order from a minimal set of conditions.Source: §C.2.3 · p. 34

C.3 Hardware Details

  • Experiments ran on a 32-core Xeon Gold 6226R CPU; GPT-4-Turbo, GPT-3.5-Turbo, and Mixtral 8x7B were accessed through APIs.Source: §C.3 · p. 35

D.1 Inference Time

  • SymPro-LM performs much better than PAL on inference time for selected FCoReBench problems.The table reports average inference time in seconds for test instances; the supplied passages do not give the individual values.Source: §D.1 · p. 35, Table 8 · p. 35

E.1.1 FCoReBench

E.1.2 Other Datasets

The appendices show SymPro-LM example programs for other logical-reasoning datasets and PAL programs for illustrative FCoReBench problems. The PAL examples include a subset-sum program that reads input from a file and recursively finds combinations matching a target.

E.1.2 Other Datasets

E.2 PAL

  • PAL example programs cover sudoku, futoshiki, Hamiltonian path, vertex cover, and subset sum.Source: Figure 22 · p. 44, Figure 23 · p. 45, Figure 24 · p. 46
  • The PAL subset-sum example reads an array and target from a file, then recursively builds combinations that sum to the target.The section says example programs read input from a file, perform reasoning, and write output to another text file.Source: §E.2 · pp. 44, 47

F Logic-LM

The Logic-LM appendix presents example runs on selected FCoReBench problems, including both correct constraint encodings and examples with errors.

F Logic-LM

Loading 2402.02611v3…