Logic.py: Bridging the Gap between LLMs and Constraint Solvers
Authors: Pascal Kesseli
Peter O'Hearn
Ricardo Silveira Cabral
Venue: NeurIPS 2025 poster ()
Keywords: formal reasoning
machine learning
large language models
constraint solvers
Primary area: reinforcement_learning
TL;DR: Using Formal Reasoning Tools in RL and at Inference Time to improve Reasoning Capability

Abstract: We present a novel approach to formalise and solve search-based problems using large language models, which significantly improves upon previous state-of-the-art results. We demonstrate the efficacy of this approach on benchmarks like the logic puzzles tasks in ZebraLogicBench. Instead of letting the LLM attempt to directly solve the puzzles, our method prompts the model to formalise the problem in a logic-focused, human-readable domain-specific language (DSL) called Logic.py. This formalised representation is then solved using a constraint solver, leveraging the strengths of both the language model and the solver. Our approach achieves a remarkable 65% absolute improvement over the baseline performance of Llama 3.1 70B on ZebraLogicBench, setting a new state-of-the-art with an accuracy of over 90%. This significant advancement demonstrates the potential of combining language models with domain-specific languages and auxiliary tools on traditionally challenging tasks for LLMs.

Logic.py: Bridging the Gap between LLMs and Constraint Solvers
Pascal Kesseli
Peter O'Hearn
Ricardo Silveira Cabral
Meta pkesseli@meta. com
Meta peterohSmeta.com
Meta rdsc@meta.com com
Abstract
We present a novel approach to formalise and solve search-based problems using large language models, which significantly improves upon previous state-of-the- art results. We demonstrate the efficacy of this approach on benchmarks like the logic puzzles tasks in ZebraLogicBencch Instead of letting the LLM attempt to directly solve the puzzles, our method prompts the model to formalise the problem in logic-focused, called Logic.py. This formalised representation is then solved using a constraint solver, leveraging the strengths of both the language model and the solver. Our approach achieves a remarkable 65% absolute improvement over the baseline performance of Llama 3.1 70B ZebraLogicBBench, increasing its accuracy over 90%. This significant advancement demonstrates the potential of combining language models with domain-specific languages and auxiliary tools traditionally challenging tasks for LLMss.
domain-specine language (DSL)
Introduction
Large language models have revolutionised the field natural language processing, achieving state- of-the-art results in various tasks such language translation, text summarisation, and question answering. However, despite their impressive performance, LLMs have historically struggled with certain tasks that require deeper understanding of mathematical and logical concepts. For instance, Kambhampati et al. (2024) demonstrated that LLMs are unable to plan and reason about complex problems, highlighting the need for further research in this area. In this paper, focus improving the performance of LLMS in solving Logic Grid Puzzles, which we explain in more detail in Sec. T.2 well first order logic tasks. We present the following research contributions:
1. Logic.py: We introduce domain-speciff human-readable language called Logic.py, which facilitates expressing logic and search-based problems by LLMs, and simplifies human annotation processes for fine-tuning.
2. Polymath Logic Agent:
We implement an agentic solver engine called polymath which accepts search-based based, informal problem statements, formalises them in Logic.py and solves them using a constraint sovler.
3. Beic and FOLIO Evaluation: We evaluate the efficacy of this approach on the logic puzzle benchmark ZebraLogicBenchh Lin el al. (0244 and the first order logic benchmark FOLIO Han et al. 2022].
The general case for DSL is not unlike that for intermediate languages in compilation. Given a new programming language it is "obvious" from the Church- language exists, but is not necessarily obvious a mapping with good efficiency properties (say) exists, and the compilation research community has found it helpful to intermediate languages
thesis that a mapping to assembly
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

to structure the design of compilers. Here, it might seem likely that constraint solvers (automatic theorem provers) could be helpful approach logic problems stated in natural language, but just how helpful or the best way to do so is not priori obvious: like in compilation, our thesis is that DSLs can help. similar analogy the relation between SQL. and first-order logic; SQI. provides facilities that make for briefer or more direct human expression than their expansions into FOL. A
similar example for Lo is presented in Section 3.1
Our results support the case that this DSL can be helpful in structuring the mapping from natural language that of a solver. In particular, [Brrmn et al. [2024] evaluate their approach against benchmark set of 14 Zebra puzzles. Their multi-agent system has a more sophisticated translation process which includes a refinement loop. but this approach raises the puzzle accuracy of GPT-4 from 23.7% to 55.3%, compared to our improvement from 24.9% to 91.4%.
1.1 Related Work
1.1.1 Formal Reasoning and Theorem Provers
Prior research has explored techniques to enhance the ability of LLMS in these central reasoning tasks, such chain-of-thought prompting and introducing symbolic representations. However, according to [Berman et al. [2024], these frameworks often struggle with complex logical problems like Zebra puzzles, partly due to the inherent difficulty of translating natural language clues into logical statements. They propose integrating LLMs with theorem provers to tackle such challenges, demonstrating significant improvements in puzzle-solving capabilities. Our approach significantly outperforms the gains of 10-15% reported in their work.
Logic-IM is framework that combines LLMs with symbolic solvers to enhance logical reason- ing capabilities, demonstrating substantial performance improvements over traditional L.-M-based approaches Pan et al.] [2023]. Ye et al. [2023] introduce Satisfiabilit--idee Language Modeling (SatLM), method that combines large language models with automated theorem provers to enhance reasoning capabilities, demonstrating state-of-the-arr performance on multiple datasets. Our approach again compares favorably to their results, and we also focus on deriving human-readable constraints that can be easily debugged and applied in human annotations for training.
1,1.2 Neuro-Symbolic Approaches
Al-Negheimish e/ al.
2023 highlight that the challenge of numerical reasoning in machine reading comprehension has been addressed by various prompting strategies for LLMs. However, these ap- proaches often struggle to provide robust and interpretable reasoning. They contrast these techniques against their neuro-symbolic approach, which has shown promising results by decomposing complex questions into simpler ones and using symbolic learning methods to learn rules for recomposing partial answers. Our work focuses on logical rather than numerical reasoning, but the two techniques are ultimately orthogonal and could perhaps even be combined.
1.1.3 Augmenting L.MSs with External Knowledge
The ALM--Agmentt system, proposed by Peng et al. [2023), addresses the limitations of LLMs in real-world applications by augmenting them with aadg-add--aay modules that ground responses in ex- ternal knowledge and iteratively revise prompts to improve factuality. Similarly, the Logic-Enhanee Language Model Agents (LELMA) framework, proposed by Mensfelt al. (2024), integrates L.MSs with symbolic AI to enhance the trustworthiness of social simulations, addressing issues such as hallucinations and logical inconsistencies through logical verification and self-refinement. Our ap- proach is agentic as well, but focuses on making formal reasoning tools as accessible as possible to the model.
1.1.4 Improving Mathematical Reasoning
Imani er al. [2023] propose technique to improve the performance of LLMs on arithmetic problems by generating muitiple algebraic expressions or Python functions to solve the same math problem in different ways, thereby increasing confidence in the output results. Similarly, Fedoseev el al. [2024 propose a method to enhance L.LMs mathematical problem-solving capabilities by fine-tuning them on dataset of synthetic problems and solutions generated using Satisfiability Modulo Theories

---

(SMT) solvers, specifically the Z3 API. Both approaches are focussed on mathematical reasoning, whereas our engine focuses on logical reasoning in propositional formulas.
1.2 Logic Grid Puzzles
We evaluate the effectiveness of approach the ZebraLogicBench benchmark presented in Lin et al. (2024). ZebraLogicBench Zebra Puzzles. These puzzles consist of series of clues about features of entities in described environment, In order to solve the puzzle, one has to guess the correct features of all entities, while respecting all the information provided in the cluses. We provide full example of such Zebra puzzle, including the expected solution, in the technical appendix in Fig. and Tab. l respectively.
dataset of 1000 Logic Grid Puzzles, also referred to as
2 Preliminaries
In this section, we provide an overview of the formal reasoning engines that serve as the foundation for our approach. Specifically, focus their key properties and capabilities that are erucial the success of our implementation.
2.1 Constraint Solvers
Constraint solvers are computational tools that enable the efficient solution of complex constraint satisfaction problems. In the context of formal reasoning, constraint solvers play crucial role in automating logical deductions and verifying the correctness of systems. At their core, constraint solvers explore possible assignments of unknown nondeterministic variables in order to satisfy set of constraints a formula. Boolean satisfiability (SAT) solvers are among the most well-known types of solvers in computer science, where the solver is allowed assign free boolcan variables truth value in order to satisfy the clauses in the formula. While SAT solvers can solve NP-complete problems, mapping problems directly to SAT can be challenging. In this paper we instead use higher level solvers and APIs that provide support for more complex domains as well as other built-in features.
2.2
SMT solvers
SAT solvers are incredibly powerful for solving propositional logic formulas, but they provide limited supports when reasoning over complex domains that involve arithmetic, arrays, or other data structures. In essence, all these domains need to be mapped to boolean formulas when using SAT solvers, such as mapping finite integer types in programming languages vector of boolean variables, one for each bit of the finite integer type.
Satisfiability Modulo Theories solvers extend the capability of SAT solvers by incorporating additional theories, allowing them to reason about richer domains. An SMT solver allows users to express constraints not just using boolean variables, but also variables of numerical, string, array, data structure types. Additionally, SMT solvers add support for explicit quantifiers, allowing users to express quantifier alternations (e.g. "for each there exists Y such that...)). This is also a key feature why we use SMT solvers as one possible reasoning back-end for Logic.py, specifically for the first-order logic problems in FOLIO Han et al. 2022].
2.3 CBMC Bounded Model Checker for and C++ programs
CBMC Clarke al. 2004 is static analysis tool designed for C and C++ programs. It operates by mapping programs to formulas in a back-end solver, typically SAT or SMT, which are satisfiable if and only if the mapped program exhibits specific property. This capability enables CBMC to effectively check programs for bugs or other properties of interest. Notably, CBMC is powered by the underlying CPROVER static analysis engine, which also supports other language front-ends, such as the JBMC Cordeiro et al. (2018) Java front-end.
Since CBMC implements mapping between programs and SAT or SMT formulas, it can serve as a convenient front-end for such constraint sovlers, exposing an API that allows expressing SAT or SMT formulas C programs with free input variables. Expressing formulas in this fashion makes
3

---

many constraint solver tasks more accessible for human developers, and it is core hypothesis of this paper that it equally simplifies the use of constraint solvers for LLMs. We describe this DSL that we expose to the LLM in more detail in Sec.
3 The Logic.py language
Our goal in designing Logic-py to provide streamlined API language that allows LLM to efficiently express search-based problems and leverage a constraint solver. We optimised for the folowing criteria:
Logic.py should be human-readable, so that it can be interpreted by any 1. programmer with Python experience. This faciliates debugging as well as annotation of training data for fine-tuning to improve the performance of models when using Logic.py.
2. Robustness: The language should minimise the surface area for syntax enrors.
3. Conciseness:
The model should able to express the necessary constraints solve search- based problem without boilerplate or needing to worry about unrelated implementation details of the programming language.
4. Expressiveness: While common constraints, such as uniqueness of a property, should be easy to express in DSL, the language must not be restricted to just these common cases. Instead, it must allow the LLM to express arbitrary constraints in the underlying constraint solver framework if necessary.
To provide good basis for our DSL in terms of robustness and conciseness, we decided to not start with CBMC's native C as a base language for Logic.py but instead, as its name suggests, we selected Python for this purpose. We use libCST" transform Logic.py to C for analysis by CBMC, as explained in more detail Sec. [ Python allows the model introduce new variables without the need for explicit, typed declarations, and similarly, these variables can be reused for other values later on without needing to worry about type compatiblity.
3.1 Type Decorators
In order to further improve the conciseness of Logic.py. we borrow well-known language features from existing languages and combine them in our DSL. As an example, expressing uniqueness of property SMT directy requries code similar the example Fig.
(forall ((x T) (y T)) (=> (distinet y)
id INT UNIQUE
(not (= (id x) (id ))))) (id
Figure 2: Uniqueness constraint in SQL
Figure 1: Uniqueness constraint in SMT
The snippet in Fig. 1 states that two distinct objects of type T should not have the same id property. Compare this to expressing the same constraint in the Data Definition Language (DDL) of the Structured Query Language (SQL) in Fig. 2 Motivated by this example, we introduced a set of custom type decorators Logic.py which allow express common property constraints in much shorter, less error-prone way. We provide the full list of Logic.py type decorators in Tab.
3.2 Free Variables, Assumptions, and Assertions
key concept in using constraint solvers are free variables. By default, any variable which is not explicitly initialised in Lygic.py is assumed to be free variable. Consequently. the constraint solver is allowed to assign it any value in order to find a satisfying assignment for all the specified constraints. We also say that such variable has nondeterministe value.
hbunss//sthhb.coommsstrrraaLLLLt

---

Feature Uninitialised variables
Description
Decorator Unique[T]
Description
Unimitialised variables receive a nondeterminis tic value. When solving search-based problems, the solution is automaically marked nondeter- ministic by our engine and the model can con- straint the solution according to its requirements. Constrains search paths for solutions to only the values where pred is true.
Equivalent to type T, but no two ob- jects of the same class have the same value for a property marked Unique. The behaviour is equiva- lent to the SQL UNIQUE keyword. Restricts the possible values of the property of type T to the values in D. where is either sequence of values, numerical range. This a more concise way of expressing value domains in the CPROVER framework using assumptions. Creates fixed-size list of element type 'T" and size 'S', This is equiva- lent to fixed size arrays in ANSI C.
assume(pred)
Domain T, DJ
assert pred
In static analysis verification scenarios, asser- tions must be true for all possible inputs satisfy- ing assumptions. In our search- problem harness, they are equivalent to assumptions.
nondet
Returns nondeterministic but valid clement from list. This can be used in combination with assumptions to find elements in list that satisfy a predicate, then express additional constraints about them.
list[T,
Table 1: Logic.py type decorators
Table 2: Logic.py nondet features
The CPROVER framework further allows users to specify assumptions and assertions. These two features work in tandem: Assumptions act preconditions, usually expressed over free variables, to constrain the solver's search to valid or interesting inputs. Assertions, on the other hand, represent safety properties, for which the solver tries find falsifying assignment in order prove the presence of a bug. Both of these features are exposed in Logic.py via the assume(...) function and the assert... statement, respectively.
In Lygdd the polymath engine, these two are actually treated interchangeably. That means we interpret assertions specified by the model not safety properties to be checked for violations, but instead as requirements on a valid solution. Interpreting assertions as assumptions and passing only a single reachability assertion to the constraint solver common pattern in program synthesis use cases David et al. [2018). We will explain the structure constraints we produce at CPROVER intermediate representation level in more detail in Sec. 5 All rondeterminism-related Logic.py features are summarised in Tab.
4 Search Problem Formalisation
After reviewing the features of Logic.py in Sec. 3 we now review how we prompt the model to express search problems in this language. We provide the full prompts in our open source agent project polymath? Note that all our prompts are zero-shot in that we do not provide any full Zebra puzzles as examples to the model. Instead, we only explain Logic.py and how to use its extended features to express generic search-based problems.
4.1 Solver backends
At the time of writing, polymath supports two solver back-ends: CBMC for SAT and Z3 for SMT problems. CBMC also has an SMT solver engine, but has limited support for quantifiers, which is why we implemented dedicated mapping from Logic.py to SMT. The CBMC back-end intended for the ZebraLogeBench benchmark in our experiments, whereas the Z3 back-end is used for the first order logic tasks in FOLIO. Note that while the Logic.pylanguage remains fundamentally the same irrespective of the back-end, the 73 back-end allows us to reason more easily over unconstrained lists using universal quantifiers. The running examples in the following sections will focus on a ZebraLogicbench example and the CBMC back-end.
5

---

4.2 Describing a Result Data Structure
Before attempting convert the clues the natural language puzzle description to solver constraints, we first prompt the model to simply define data structure that can best represent valid solution. We ask the model define this data structure in Logic.py and be as precise as possible with respect to type annotations. This allows us to constrain the search space for valid solutions purely based on the domain of the problem, irrespective of explicit clues and constraints. Fig. provides an example of the kind of data structure the LLM will generate.
class House:
Unique [Domain [int, range 7)]] name: Unique [Domain [str, "Alice", "Eric", ...]]
class PuzzleSolution: houses: list [House,
6]
Figure Model Output Example: Result Data Structure
4.3 Constraining Correct Solution
Once the data structure is defined, we prompt the model to generate validation function that accepts an argument of this type and asserts that it is the correct solution we searching for. In the case of Zebra puzzles, this leads to the model adding assertions corresponding to the clues in the puzzle. This approach transforms the challenge for the LLM fundamentally: Instead of searching the solution space for configurations that satisfy the clues stated in the puzzle, it just needs to be able to reason about the clues themselves. Fig. shows a few example clues and how they can be formalised in Logic.py data strucutre chosen by the model.
def validate (solution: PuzzleSolution) -> None Clue 1: Bob is the person who uses Xiaomi Mi 11. bob = nondet (solution, houses)
assume (bob. name "Bob") assert bob phone == "xiaomiumiul1"
Clue 3: The Dragonfruit smoothie lover is somewhere to the left of the person in a ranch-style home. nondet (solution. houses) assume (d. smoothie nondet (solutiio. houses)
"dragonfruit")
assume (r. house_style assert d. hohhoueeenubrr < wchouse_numee
"ranch")
Figure 4: Model Output Example: Solution Constraints
5 Logic Agent Architecture
Fig. 5 illustrates the full implementation architecture of our solver engine, starting with the formal- isation steps outlined in Sec. Our engine converts these Logic.py constraints into an equivalent, lower-level C representation using a libCST transformer. During this process, the type decorators introduced in Sec. 3.1 are mapped matching initialisation helpers in CBMC's IR. An example of this mapping is illustrated in the technical appendinx Fig. Z
The validation function containing the constraints derived from the Zebra Logic clues is equally converted into a C representation, and embedded into a search harness. this harness, a nonde- terministic instance of the result data structure proposed by the model is initialised using the type

---

Generate Data Structure
Generate Con-
Puzzle
Puzzle
straints
Expected
Data Structure
Output
Python Con-
Format
Ambiguous
UNSAT
Python Syntax Error
straints
Solution
Generate Solution
C Constraints
Convert Python Hareess to C
using CBMC
Solution as struct
LLM Steps
Convert to Expected Output Format
Constraint Solver / Compiler Steps
Figure 5: Logic Agent Architecture
decorator information, then constrained using the converted validation function. All assertions in the validation function are converted into assumptions, and we add a single reachabilty assertion prompt the constraint solver find an assignment for the nondeterministe puzzle solution such that it satisifes all constraints. We provide an example of a CBMC ANSI-C harness in the technical appendix in Fig.
5.1 Error Recovery
Due to the heuristic nature of the formalisation and constraint solver steps, our solver engine can fail various steps along the pipeline. The model might produce invalid Logic.py code to begin with, leading to syntax errors in libCST. These errоrs are caught during the C harness generation, in which case we revert to the original data structure generation step and start the process from scratch. We currently do not provide any information about the syntax error to the model or ask it to fix its prior mistakes, and such approaches could be explored in future work.
Our solver back-ends can also detect that a formalisation has no solution, i.e. unsatisfiable, or whether there are multiple solutions, i.e. the constraints are ambiguous. In general, logic problems provided as user input may indeed be inherently contradictory, or might allow for multiple independent solutions. Thus it cannot automatically be concluded that unsatisfiable ambigous constraints formalisation mistake by the L.M. However, if is known beforehand that the problem must have a solution, must have exactly one solution, it can of course only improve outcomes treat UNSAT or ambiguous constraints as errors and restart.
For example, for ZebraLogicBench in our experimental evaluation, it is known beforehand that each sample must have exactly one solution. For this reason we implemented restarting on UNSAT, but did not yet implement restarting ambiguity. For this particular benchmark, we did not observe any significant difference in score in our experimental evaluation Sec. 6 whether we restart on UNSAT not, since UNSAT results explore how well models can predict based on the input puzzle whether multiple valid solutions or no valid solutions are plausible.
extremely rare in experimental runs. Future work should also
Experimental Evaluation
To evaluate the effectiveness our approach, we conducted experiments on Beinaeh,gi,Bench,
benchmark suite consisting of 1000 logic grid tasks. In order to run the evaluation independently, researchers must request access to private dataset hosted huggingface.co. We implemented benchmark runner that accepts this dataset its input, which we share in open source project
7

---

Puzzle Accuracy
Cell Ac-
Model
All
Small
Medium
Large
XL
curacy
grok---minn--aas--boahhhggg
92.6
98.75
96.43
93.5
76.5
94.63
91.7
99.69
97.14
87.5
75.5
95.7
Polymath Meta--llama-33--00B--
90.7
93.75
93.21
90
83
92.56
88.9
99.69
97.86
88
60
90.41
o1-2024-12-17
81
97.19
92.14
78
42.5
78.74
mook-3-mini-fast-btt--oo
80.7
98.75
96.43
77
33.5
84.22
deepseek-RI
78.7
98.44
95.71
73.5
28.5
80.54
Polymath gpt-4o
77.8
91.88
79.64
75.5
55
76.34
Polymath chaude=3---snnne222244000
76.9
85.31
78.57
76
62
80.58
74.8
99.38
91.07
64.5
23
72.6
ol 01-preview-22024-09-122
71.4
98.12
88.21
59.5
17
75.14
chnde-335-somnee222241022
36.2
84.69
28.93
4
54.27
32.6
81,25
22.5
1.5
45.8
gpt-4o-2024-08-066
31.7
80
19.64
2.5
0.5
50.34
semini-L.5-pro-ex--00777
30.5
75.31
20.71
3
0
50.84
Mistral-Large-2
29
75.94
15
2.5
47.64
Qwen2.5-72B-Instruct
26.6
72.5
12.14
0
40.92
MetteLlama-31--0BBnnsttuu
24.9
67.81
10.36
1.5
27.98
Table 3: ZebraLogicBench Puzzle Accuracy Results
polymath. The output result of the benchmark runner is evaluated using the ZeroEval evaluation suite provided by the benchmark authors.
Due to resource and time constraints, only evaluated the effect of polymath on the models Llama 3.1 70B, GPT-4o, and Claude 3.5 Sonnet. We run the logic agent implementation on a developer server with 56 cores and 114GB RAM. We self-hosted Llama 3.1 70B clust wither 700 GPUs. In this environment, running 100 tasks concurrently, full benchmark run takes approximatley 15 minutes. We evaluted only our polymath agent implementation using this setup. All other results listed were taken directly from the Zebral Tebral.ogicBench leaderboard Lin et al. [2024). All experiments performed these off-the-sher models without additional fine-tunging.
Tab. Billustrates that using polymath boosts the performance of all three models. Most notably, Llama 3.1 70B previously attained new SOTA using our agent, with 91.4% accuracy, achieving a 20% margin over OpenAl ol -previi... However, 03-mini and grok---miii-faat-beee--e this result by 1% and 1.9% respectively. However, our implementation still solves the most puzzles in the hardest XL puzzle category, where consistently provides the highest gains across models. This demonstrates that polymath support models particularly on challenging reasoning problems.
since exceeded
As mentioned Sec. referror-recoveryy our experimental setup includes restarting on UNSAT, but not on ambiguity. Removing this restart UNSAT logic did not lead to any measurable decrease in score across our experimental evaluation runs. In general, we restart most five times in case of formalisation syntax errors UNSAT results before aborting. Independently, we also retry at most five times if we receive an HTTP error from our LLM inference API, e.g. due to throttling. In our final ZebraLogieBBench benchmark run of 1000 samples, observe 51 occurrences of unsatisfiable constraints across all attempts and tasks, and 70 occurrences of syntax errors Logic.py. Of the 9.3% of puzzles where approach did not produce entirely correct solution, in 2.9% of cases we were not able to produce a solution at all five attempts, due to the aforementioned syntax or unsatisfiability errors. In the remaining 6.4% of cases, polymath produced valid, but incorrect constraint and thus produced an incorrect or only partially correct solution.
Overall, our performance gain is particularly striking when compared to how our base model, LLama 3.1 70B Instruct, performs without the help of constraint solver. On average, it reached 24,9 9 accuracy across all puzzles, compared to 91.4% accuracy with the constraint solver. We were unable to evaluate the effect polymath on grok-3 and o3-mini due to time and resource constraints.
8

---

Model
Accuracy
Polymath clade->35someet22241000
81.28
Logic-LM Pan el al.
2023
78.92
Logic-LM Han et al.
2022
78.1
Polymath gpt
57.64
Polymath
56.65
Table 4: FOLIO Accuracy Results
We further evaluated our secondary Z3 back-end the FOLIO benchmark using the same three models. As illustratd in Tab. [ Claude 3.5 benefited the most from polymath support, and again compares favorably to prior approaches.
7 Threats to Validity
While we believe we made a convincing case in Sec. that auxiliary tools can significantly boost the performance of state-of-the-art LLMS challenging tasks, we would like to address potential threats to the validity of our results. Firstly, we evaluated our engine thus far only against logic grid and first-order logic puzzles. Our technique may prove less impactful when applied to other search-based problems formalised by an LLM. This may be due to the fact that our Logic.py prototype is currently incomplete and does not yet support some common Python language and standard library features, or more fundamentally, that the formalisation of other search-based problems may not prove as tractable for state-of- tattee-ff-hhe- the-an LLMs as logic grid puzzles.
Furthermore, while our approach of using a tailored DSL to allow the LLM to operate an auxil- iary tool yielded promising results, further experiments will have to show whether this approach can be generalised to other categories of auxiliary tools and problem domains, such as numerical computational programming languages or algebraic modeling languages.
8 Conclusions and Future Work
In this paper, we presented a novel approach to solving search-based problems using large language models. By introducing the domain-specifit language Logic.py and implementing an agentic solver engine polymath, we demonstrated significant improvements in performance on ZebraLogicBenct and FOLIO benchmarks. Our results show that combining the strengths of LLMs with those of constraint solvers can lead to remarkable advancements in solving traditionally challenging tasks.
The success of this approach highlights the potential for further research in this area. Some potential directions for future work include:
Fine-Tuning for Logic.py: So far, we only used off-the-shelf models to power our polymath engine. We plan to fine-tune models to better use Logic.py and further increase accuracy.
2. Extending Logic.py: Developing a more comprehensive and expressive version of Logic.py could enable the formalisation of wider range of search-based problems.
3. Improving the Logic Agent: Enhancing the agentic solver engine to better handle complex problem statements and iterate on its mistakes (e.g. syntax errors) could lead to further performance gains.
4. Applying the approach to other domains: Exploring the application of our method to other, such optimisation or mathematical rasoning, could reveal new opportunities for improvement.
5. Investigating the role of LLMs in problem formalisation: Further research into the capabilities and limitations of LLMs in formalising search-bases problems could provide valuable insights into the design of more effective problem-solving systems.
6. Teaching neural nets to search like solvers: Our translations leverage powerful aspects of constraint solvers: proof checking and search. It would be possible to decompose these strengths. Solvers like have evolved subtle heuristies for approaching computationally intractable problems that are NP-hard and more, and if we train nets in way that learns

---

these heuristics they might provide benefit more broadly than as the targets of translation- based work. this context, work such as this could provide baselines or targets for what we would want out of the training.
7. Reinforcement Learning using Logic.py constraints: During our experimental evaluation, we noticed that interpreting even single clue out of n incorrectly can lead to a result table where zero columns match the expected value, e.g. because the order shifted. He have started a reinforement learning project where we score model answers not using Logic.py constraints in give the model semantic feedback (e.g. number of clues respected), rather than syntactic feedback (e.g. number of correct cells in result table). This already shows promising improvements in the model's reasoning and coding capabilities.
Building on this project, our broader research aims to further explore the potential of combining large language models with specialized reasoning tools. By pursuing these avenues of research, we believe that it possible to develop even more powerful and efficient problem-solving systems.
9 Funding Transparency Statement
9.1 Funding
Funding in direct support of this work: GPU compute provided by Meta.
9.2
Competing Interests
Additional revenues related to this work: Employment with Meta.
References
Hadeel Al- Al-hegheimish, Pranava Madhyastha, and Alessandra Russo. Augmenting large language models with symbolic rule learning for robust numerical reasoning. In The 3rd Workshop on Mathematical Reasoning and Al at NeurIPS'23, 2023.
Shmuel Berman, Kathleen McKeown, and Baishakhi Ray. Solving zebra puzzles using constraint- guided multi-agent systems, 2024.
Edmund Clarke, Daniel Kroening, and Flavio Lerda. tool for checking ANSI-C programs. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), volume 2988 of Lecture Notes in Computer Science, pages 168 176. Springer, 2004.
Lucas Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel, and Marek Trtik. JBMC: A bounded model checking tool for verifying Java bytecode. In Computer Aided Verification (CAV), volume 10981 of LNCS, pages 183-190. Springer, 2018
Cristina David, Pascal Kesseli, Daniel Kroening, and Matt Lewis. Program synthesis for program analysis. ACM Transactions on Programming Languages and Systems, 40:1-45, 05 2018.
Timofey Fedoseev, Dimitar Iliev Dimitrov, Timon Gehr, and Martin Vechev. LLM training data synthesis for more effective problem solving using satisfiability modulo theories. In The 4th Workshop on Mathematical Reasoning and Al at NeurlPS'24 24, 2024.
Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Luke Benson, Lucy Sun, Ekaterina Zubova, Yujie Qiao, Matthew Burtell, David Peng, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, Ansong Ni, Linyong Nan, Jungo Kasai, Tao Yu, Rui Zhang, Shafiq Joty, Alexander R. Fabbri, Wojeiech Kryscinski, Xi Victoria Lin, Caiming Xiong, and Dragomir Radev. Folio: Natural language reasoning with first-order logic. arXiv preprint MwXiv:2209.004444 2022.
Shima Imani, Liang Du, and Harsh Shrivastava. Mathprompter: Mathematical reasoning using large language models, 2023.
10

---

Subbarao Kambhampati, Karthik Valmeckam, Lin Guan, Mudit Verma, Kaya Stechly, Siddhant Bhambri, Lucas Saldyt, and Anil Murthy. Lims can't plan, but can help planning in llm- mmmmoodulo frameworks, 2024.
Bill Yuchen Lin, Ronan Le Bras, Peter Clark, and Yejin Choi. Zebralogic: Benchmarking the logical reasoning ability of language models, 2024.
Agnieszka Mensfelt, Kostas Stathis, and Vince Trencsenyi. Logic-enhanced language model agents for trustworthy social simulations, 2024.
Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Houda Bouamor, Juan Pino, and Kalika Bali, editors, Findings of the Association for Computational Linguistics: EMNLP 2023, pages
Singapore, December 2023. Association for Computational Linguistics.
Baolin Peng, Michel Galley, Pengcheng He, Hao Cheng, Yujia Xie, Yu Hu, Qiuyuan Huang, Lars Liden, Zhou Yu, Weizhu Chen, and Jianfeng Gao. Check your facts and try again: Improving large language models with external knowledge and automated feedback, 2023.
Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. Satlm: Satisfiability aided language models using declarative prompting, 2023.

---

NeurIPS Paper Checklist
1. Claims
Question:
Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope?
Answer: [Yes]
Justification: The claims in the abstract are based on the experimental section. We since added an additional benchmark, FOLIO, but this does not affect the claims in the abstract.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings.
It is fine to include aspirational goals as motivation as long as is clear that these goals attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: We address limitations in the section "Threats to Validity". We also discuss experiment configurations we were not able to carry out due to budget and time constraints in the section 'Experimental Evaluation".
Guidelines:
The answer NA means that the paper has limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors are encouraged to create separate "Limmtations" section in their paper.
The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect the scope of the claims made, e.g., if the approach was only tested on a few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't 't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
3. Theory assumptions and prool's
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
12

---

Answer: [NA]
Justification:
The paper does not make theoretical claims and does not introduce theorems.
Guidelines:
The answer NA means that the paper does not include theoretical results.
All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
This project was open sourced and was forked by users already. To guarantee anonimity, we provide a ZIP file of the repository. The paper contains instructions of how to attach polymath to new inference service, since ours is bespoke to our company resources.
Justification:
Guidelines:
The answer NA means that the paper does not include experiments.
If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is novel architecture, describing the architecture fully might suffice, or if the contribution a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way accomplish this, but reproducibility instructions for how to replicate the results, access to a hosted model (e.g.. in the case of large language model), releasing of a model checkpoint, other means that appropriate to the research performed.
also be provided via detailed
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
(a) If the contribution is primarily a new algorithm, the paper should make it clear how to reproduce that algorithm.
(b) the contribution is primarily new model architecture, the paper should describe the architecture clearly and fully.
(c) If the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers have some path reproducing or verifying the results.
cases, in which
5. Open access to data and code
13

---

Question: Does the paper provide open access to the data and code, with sufficient instruc- tions faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
The project was open sourced and provide ZIP file of the repository for anonimity. The datasets are publicly available on HuggingFace, and the repository contains script download them.
Justification:
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (https://nips... cc/
mublic/guides CoodeSummissioooolle..
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurlPS code and data submission guidelines (https
/ //nips.conicc http:cppppwpcpcceeeeeeeeeeep
for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data,
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary understand the results?
Answer: [NA]
Justification: We did not fine-tune or train model in this project. We only used test data sets to evaluate the approach.
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented in the core of the paper to a level of detail that is necessary to appreciate the results and make sense of them.
The full details can be provided either with the code, in appendix, or as supplemental material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined other appropriate information about the statistical significance of the experiments?
Question:
Answer: [No]
Justification: The evaluation suite in experimental evaluation is provided by third party, and we only provide the data as yielded by this suite. We repeated this evaluation multiple times before initial and camera-ready submission confirm results, but otherwise reported the results as output by this third-party suite.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by emror bars, confi- dence intervals, or statistical significance tests, least for the experiments that support the main claims of the paper.
14

---

The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for caleulating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (c.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation or the standard error of the mean.
is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful not to show in tables or figures symmetric error bars that would yield results that are out range (e.g. negative еπτог rates).
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures or tables text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information the com- puter resources (type of compute workers, memory, time of execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
Justification: We documented the hardware we used to run our experiments, apart from GPU resources used in external third party services.
Guidelines:
The answer NA means that the paper does not include experiments.
The paper should indicate the type of compute workers CPU GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental runs well estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics / http://wwwppp..ccou.......accaaa
Answer: [Ye]]
Justification: To the best of knowledge, none of the concerns in the guidelines violated in our work.
Guidelines:
The answer NA means that the authors have reviewed the NeurIPS Code of Ethics.
If the authors answer No, they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make to preserve anonymity (e.g., .., if there is special consid- eration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [NA]
Justification:
The research performed does not directly expose such societal impacts.
Guidelines:
The answer NA means that there is no societal impact of the work performed.
15

---

If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), faimess considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of ML).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Justification: We did not release a model. The paper only concerns itself with improving the performance of existing models on logic tasks.
Guidelines:
The answer NA means that the paper poses no such risks.
Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Answer: [Yes]
Justification:
All licenses are respected and all data is properly cited.
Guidelines:
The answer NA means that the paper does
existing assets.
The authors should cite the original paper that produced the code package or dataset.
The authors should state which version of the asset used and, possible, include a URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset. For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
16

---

If assets are released, the license, copyright information, and terms of use in the thcode. has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
package should be provided. For popular datasets, paperswi
latasets.paperssi
For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided.
If this information not available online, the authors are encouraged to reach out to the asset's s creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
Justification:
All newly created artifacts are documented in detail.
Guidelines:
The answer NA means that the paper does not release new assets.
Researchers should communicate the details of the dataset/code/mmodl as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent obtained from people whose asset used.
At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file.
14. Crowdsoureing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification:
No crowdsourcing research with human subjects was involved.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then as much detail as possible should be included in the main paper.
According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or equivalent approval/review based the requirements of your country institution) were obtained?
Answer: [NA]
Justification:
The paper does not involve crowdsourcing nor research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing research with human subjects.
Depending the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
17

---

We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
16. Declaration of LLM usage
Does the paper describe the usage of LLMs if it is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, formatting purposes and does not impact the core methodology, scientific rigorousness, or originality of the research, declaration is not required.
Question:
Answer: [NA]
Justification:
The core method development in this research did not involve LLMs.
Guidelines:
The answer NA means that the method development in this research does not involve LLMs as any important, original, or non-standard components.
Please refer to our LLM policy pettts://neurre https///eccoooeeeeee//////////// for what should or should be described.
18

---

A Zebra Puzzle examples
There are 4 houses, numbered 1 to from left to right, as seen from across the street. Each house is occupied by a different person. Each house has unique attribute for each the following characteristies:
Each person has unique name: Alice, Eric, Arold, Peter
Each person has occupation: artist, engineer, teacher, doctor
People have unique favorite book genres: fantasy, science fiction, mystery, romance
People use unique phone models: google pixel 6, iphone 13, oneplus 9, samsung galaxy s21
Clues:
1. The person who an engineer is directly left of the person who Samsung Galaxy S21.
2. The person who loves fantasy books is in the second house.
3. Alice is not in the second house.
4. Eric is the person who a teacher.
5. The person who uses a Samsung Galaxy S21 is the person who loves fantasy books.
6. The person who uses an iPhone 13 the person who loves science fiction books.
7. The person who loves science fiction books is somewhere left of the person who uses OnePlus 9.
8. The person who uses OnePlus 9 is Arnold.
9. The person who is a doctor is the person who loves mystery books.
10. The person who uses an iPhone 13 the person who is teacher.
Figure Example Zebra logic puzzle
House
Name
Occupation
BookGenre
PhoneModel
Alice
Engineer
Romance
Pixel 6
2
Peter
Artist
Fantasy
Galaxy S21
Eric
Teacher
SciFi
iPhone 13
4
Arnold
Doctor
Mystery
OnePlus 9
Table Zebra Puzzle Example Solution
B CBMC C constraint examples
In this section we provide ANSI-C constraint examples for our running example in the paper suitable for consumption by the CBMC constraint solver.
19

---

struct House { int house_number: const char name; const char * smoothie;
};
static int Youse_house_nue []
{1, 2, 3, 4, 5, 6); static bool House_ pase_house_nunte used [6]; static const char {"Alice", "Eric", "Peter", ...;;
namse_name []
static bool House_ name_ used [6]; //
#define SPPROER__niqqe__ce field, dield_domain_arpg \
size_t t index; \ ePPROVER_assuee (index
(sizeof (feeefffffilldddmmmi..aaa.) /
sizeof afaatdcfiil..dmmnnnarrrr/a////// [0])));
CPROVER_assune
fiold_domain.arryy#t_ssdddd [inde] [index] \
true;
field = field_domain_ [index]; A
//
static void init_House
struct House instance) {
CeROVER_unique_domiii
-hosse -
House_house_number
); __CFROVER_uniqu_ddomeee
instance->name
house_name
/1
Figure 7: CBMC Data Structure Example
20

---

static void validate( struct PuzzleSolution solution) {
bob DeRROVER_nonee__leee
colution.housee
_CPROVER_assume (bob. name == "Bob");
_CPROVER_ (bob. phone
"xiaomiimiul1"".
}
//
int main (void) {
struct PuzzleSolution solution; init Pniit.uuzlesolutiinn (ksolution); validatte
_PROVER_ ("solution",
solution);
--CPROVER CcsRet assert (false, "");
Figure 8: CBMC Search Constraint Example
21


Reviews:
[{"review_id": "r4aZ0Ym5P7", "reviewer": "Reviewer_SiJ2", "summary": "The paper presents Logic.py, a domain-specific language (DSL), and the Polymath agent to bridge LLMs with constraint solvers (e.g., CBMC, Z3) for logical reasoning tasks. Instead of direct LLM problem-solving, the approach prompts LLMs to formalize problems in Logic.py, which is then solved by solvers. Experiments on ZebraLogicBench and FOLIO show significant accuracy gains (e.g., Llama 3.1 70B improves from 24.9% to 91.4% on ZebraLogicBench).", "questions": "- The paper acknowledges Logic.py lacks support for complex Python features. Can you specify which features are missing (e.g., classes, generators) and how their absence limits problem formalization?\n- How does the pipeline's latency compare to direct LLM inference (e.g., time per puzzle for Polymath vs. Llama 3.1 alone)? Does the solver integration introduce bottlenecks for real-time applications?", "limitations": "yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n- The paper demonstrates significant performance gains (up to 65% absolute improvement) on two distinct benchmarks (ZebraLogicBench and FOLIO), using well-known models (Llama 3.1, GPT-4o, Claude 3.5). Results are compared against multiple baselines, including state-of-the-art methods, providing robust evidence of the approach’s efficacy.\n- The paper follows a clear narrative and easy to read\n- The approach addresses a critical limitation of LLMs (logical reasoning) with tangible improvements (e.g., Llama 3.1 accuracy from 24.9% to 91.4%), enabling more reliable automation of logic-intensive tasks (e.g., puzzle-solving, formal verification).\n- The \"LLM+DSL+solver\" paradigm introduces a new framework for combining neural and symbolic AI, which could inspire similar approaches in math reasoning, program synthesis, or planning.\n\nWeakness:\n- While the integration is novel, the idea of combining LLMs with solvers is not entirely new (e.g., Logic-LM, SatLM). The originality lies in the DSL-mediated approach, but the core concept builds on existing neuro-symbolic research.\n- The paper hypothesizes that DSLs can bridge LLMs and solvers (analogous to compilation), but this hypothesis is tested only in logic tasks, leaving its validity in other domains unsubstantiated.\n-  Experiments focus solely on logic puzzles and first-order logic, leaving broader applicability (e.g., numerical \ncomputational programming languages or algebraic modeling languages) untested. The \"Threats to Validity\" section acknowledges this, but empirical validation in other domains is missing.", "was_revised": true, "final_justification": "My concerns about the paper have been addressed by the author's response. As my initial score was positive already, I just kept it for the final score.", "rebuttal": "- At the Python language level, Polymath’s implementation is fairly complete and supports rich features like methods, classes, and inheritance, thanks to its being based on libCST. However, comprehensions and lambdas in particular are currently not implemented in our mapping to the back-end engines. Using these features will lead to spurious errors and restarts in Polymath, and we try to guide for this in the system prompt.\\\n\\\nAt a library level, we do not attempt to map native Python library code to our back-end engines, safe for a few critical utility methods. Related work describes methods to derive such constraints from mixed-language environments, e.g. Gopan, D., Reps, T. (2007): Low-Level Library Analysis and Summarization; Nastaran Shafiei and Franck van Breugel (2013): Automatic Handling of Native Methods in Java PathFinder.\n\n- The Z3 and CBMC (SAT) engines themselves do not introduce measurable bottlenecks. The formulas produced for our two benchmark sets are orders of magnitude smaller than what these engines are optimised for. The formalisation by the model into Logic.py is actually more impactful here, since Logic.py is not optimised for brevity, but human readability. The average task formalisation (including restarts in case of failure) only takes 20-30s on our inference infrastructure, so this was not a concern in our experiments. However, real-time applications may want to hone their choice of DSL with this in mind."}, {"review_id": "7w4gh7PjUq", "reviewer": "Reviewer_Jewb", "summary": "This paper presents Logic.py, a domain-specific language designed to power LLMs with constraint solvers. The proposed approach is a form of neuro-symbolic integration that is designed to target solving logic puzzles and search algorithm problems for which LLMs are known to be weak. \n\nMore concretely, the proposed approach first prompts LLMs to formalize problems in Logic.py --- a Python-based, human-readable DSL. This formalized representation is then solved using constraint solvers like CBMC or Z3.\n\nThis paper also presents a novel Polymath Agent Architecture that converts Logic.py code to C using libCST transformation and also includes error recovery mechanisms for syntax errors and unsatisfiable constraints.\n\nExperimental Results look strong, particularly on ZebraLogicBench, when comparing against the base LLMs performance, e.g., Llama 3.1 70B improved from 24.9% to 90.7% accuracy, while GPT-4o improved from 31.7% to 77.8% and Claude 3.5 Sonnet improved from 36.2% to 76.9%. On the other hand, if compared against other SOTA models, then the final results are not as strong as them.", "questions": "- regarding the error recovery process, the paper states that \"We currently do not provide any information about the syntax error to the model\". It's not clear to me why this design choice was made.\n\n-tThe restart process isn't clearly defined - how many retries? What's the fallback?\n\n- this paper has a lot of typos, e.g., \"constraint sovlers\", \"satisifes\", \"ZebraLogcBench\", \"translation315 based work\", just to list a few", "limitations": "yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths:\n- The idea of symbolic system integration is neat and makes sense for logic problems that require constraint satisfaction. \n- The proposed language logic.py and the agentic system Polymath both seem interesting.\n- strong empirical results over the same size, same class base LLMs.\n\nWeaknesses:\n- the applicability of logic.py seems relatively narrow.\n- not SOTA results compared to other prior works.", "was_revised": false, "final_justification": "", "rebuttal": "- We share the reviewer’s opinion that providing generative error feedback to the model might further improve performance. We did not address this in this project, since we wanted to evaluate the fundamental impact of auto-formalisation on its own, and decided to leave generative feedback and other code repair strategies for future work.\n- If we encounter a recoverable error, we attempt to restart at most five times. We also explored fallback options like forwarding the original problem to the model in the case of a formalisation failure. However, in order to assess the impact of our formalisation, we did not apply any such fallback during our experimental evaluation.\n- Thank you for pointing out these typos, we already addressed them in our paper."}, {"review_id": "37mBGzOwQX", "reviewer": "Reviewer_ReaH", "summary": "This paper makes an attempt to address the lack of reasoning exhibited\nby large language models (LLMs) in the context of a particular kind of\nlogic task. The task is given a list of facts about K objects and\ntheir properties, the model must determine which of the K objects\nmatches which of the facts and properties. For this task, the authors\ndevelop a Python-like domain-specific language (DSL) Logic.py that\ndescribes the problem, which an LLM model is supposed to produce given\nthe input problem description in a natural language. The Logic.py\nformulation is then translated either into C, which is handed either\nto a CBMC solver, or into an satisfiability modulo theories (SMT)\nformula to feed a generic SMT solver. Finally, either CBMC or an SMT\nsolver produce a solution to the problem. This approach may require\nmultiple iterations if the LLM fails to produce a correct Logic.py\ncode. Experimental results obtained on the widely used set of\nbenchmarks ZebraLogicBench (containing exactly the above kind of logic\npuzzles) demonstrate a significant performance boost for a few LLMs,\nincluding Llama 3.1 70B, GPT-4o, and Claude 3.5 Sonnet, when compared\nto the baseline LLMs without the Logic.py functionality.", "questions": "1. How can you generalise your approach to other types of logic\npuzzles? I am mostly interested in a general approach that would be\nable to handle a wide class of logic problems with a large variety of\nconstraints.\n\n2. What can you say about the number of iterations your approach takes\nfor the considered benchmarks (min, max, avg) if an LLM fails to\nproduce reasonable Logic.py code?\n\n3. How do you plan to address the issue of unsatisfiability, i.e., if\nthe problem has no solution? How do you plan to explain it to the\nuser?", "limitations": "Yes", "rating": 4, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 3, "significance": 1, "originality": 2, "strengths_and_weaknesses": "I would say the main strength of the paper is that it is well written.\nThe motivation is reasonable and the flow is quite easy to follow.\nAnother upside is the experimental results demonstrating a significant\nperformance boost for the target class of logic tasks. The approach\ntackles the problem of the lack of reasoning in LLMs in an effective\nway by delegating the entire reasoning task to a dedicated solver,\nwhich is known to be effective for the considered class of problems.\n\nAmong the weaknesses is the simplicity of the proposed approach and\nits somewhat \"hard-coded\" nature. Indeed, the language Logic.py in its\ncurrent form is very specific to the considered class of problems.\nNote that both CBMC and SMT are known to be effective for this really\nsimple reasoning problems. In fact, this matching problem with a bunch\nof \"all-different constraints\" is trivial for them unless the size of\nthe problem is huge. And so what is left is a simple translation of\nthe problem into a DSL compilable to C or SMT, which I guess can be\ncalled the main technical contribution of the paper that makes the\napproach work.\n\nWhat is somewhat disappointing is that the authors do not address the\nobvious issue of potential errors occurring here and there in the\ntranslation process. It is clear that no LLM is capable ot producing a\ncorrect Logic.py code *all the time*, and what the authors do in case\nof a failure is running the LLM multiple times from scratch until it\nproduces correct code.\n\nAnother limitation of the approach is that it does not only target one\nparticular type of problem but cannot work for this same type of\nproblem if it does not have a solution. This is because in the case of\nunsatisfiability reported either by CBMC or SMT, the authors again\nrestart the process from scratch, which is not very helpful if there\nis no solution at all.\n\nSome more-or-less minor issues include the lack of benchmark\ndescription in terms of size and complexity, the lack of discussion on\nthe scalability of the approach (in terms of the number of iterations\ntaken from scratch till a solution gets produced), and a large number\nof typos in the text.", "was_revised": true, "final_justification": "While some of my concerns have been addressed by the authors in their rebuttal and the follow-up discussion, the major limitation of the approach in terms of its inability to handle problems with no solutions should be explicitly discussed in the paper and will perhaps require further significant efforts.", "rebuttal": "1. The reviewer's observation regarding the inherent limitations of relying on formal reasoning engines is accurate. Firstly, our approach is constrained by the problem domain of these solvers - for example, SAT solvers operate within NP-complete problems. Secondly, even within this domain, the complexity and size of the constraints necessary for a puzzle or game may well exceed what the model can realistically express in Logic.py.\\\n\\\nNevertheless, the SAT domain supported by CBMC encompasses a wide range of games and puzzles. And importantly, our method is not tailored specifically to Zebra Logic puzzles. We do not provide system prompts unique to Zebra puzzles; instead, we instruct the model to generate a generic \"data structure\" capable of representing the solution to a given logic puzzle. This data structure may include entities in search puzzles like Zebra Logic, or steps and moves in game-based puzzles. Similarly, the model is only tasked to express the \"constraints or rules\" that define a correct solution to the puzzle or game.\\\n\\\nWe selected FOLIO as a second benchmark primarily to demonstrate that our engine can scale to different types of solvers as well. In particular, quantifier alternations could not be easily mapped to CBMC’s SAT domain. However, FOLIO also serves as an example of how this “data structure and constraint”-based approach can generalize to a substantially different type of puzzle.\\\n\\\nRegarding scalability to new solvers and domains, our DSL acts as an intermediate protocol that facilitates the integration of new reasoning engines into the agent. For instance, an internal team is already employing a Polymath-like agent for a real-world support use case, leveraging a solver optimized for process flow constraints.\\\n\\\nOf course, decision problems beyond NP remain challenging in both formal and informal contexts. But overall, these points highlight the flexibility and extensibility of our approach beyond any single puzzle type or solver domain.\n2. In our experiments we limit Polymath to at most 5 restarts per problem. We observe that the vast majority of problems in our benchmark set can be solved in 1-3 attempts. Most easy and medium puzzles are solved in a single attempt, and in 2.9% of cases we cannot produce a syntactically valid formalisation even after 5 attempts.\n3. Unsatisfiability (no valid solutions according to the model’s constraints) and ambiguity (multiple valid solutions according to the model’s constraints) are two signals that both our SAT and SMT engine implementations can provide for any puzzle. Both may be valuable information to relay back to the model for refinement, or ultimately as an answer to the user. The reviewer is correct in pointing out that we did not address leveraging UNSAT as a signal in this work, simply because it is not a valid outcome for the particular benchmarks we evaluated against.\\\n\\\nHowever, we did discuss in the paper how ambiguity feedback could be leveraged, and the strategy presented can be applied to unsatisfiability as well. Our current suggestion for ambiguity is to inform the model that the current constraints allow for multiple options, and let it decide in an agentic manner based on the input puzzle whether this is an acceptable or likely outcome. If yes, this is treated like any other result and reported to the user, otherwise it is grounds for a refinement / restart step.\\\n\\\nFundamentally, we delegate to the model the responsibility of defining the problem’s domain via a Python data structure. For a production grade agent handling real-world use cases, we expect that developers may choose to either explicitly configure whether UNSAT is an option, or delegate this decision to the model as a part of the domain description process."}, {"review_id": "X6aozM39dZ", "reviewer": "Reviewer_ZzMd", "summary": "This paper introduces logic.py, a domain-specific language designed to bridge the gap between large language models (LLMs) and constraint solvers. Specifically, LLMs are prompted to formalize problems into logic.py, which are then solved by constraint solvers. The introduction of this intermediary language marks a significant advancement, as demonstrated by benchmarks on ZebraLogicBench.", "questions": "- The existing LLMs could be familiar with the Z3 API, z3py. What is the performance like when using z3py as a \"DSL\"?\n- More details regarding the evaluation are needed. For instance, what is the number of generations for each problem?\n- Have the authors analyzed the errors of the proposed framework on the benchmark? Specifically, how many problems failed due to syntax issues, and how many were due to incorrect formalization?", "limitations": "Yes", "rating": 4, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 2, "clarity": 2, "significance": 3, "originality": 3, "strengths_and_weaknesses": "### Strengths\n- Exploring the necessity of a domain-specific language (DSL) can be quite intriguing, as it offers a new perspective for bridging large language models (LLMs) and constraint solvers.\n- The summarized criteria for defining a DSL are well-founded and can inspire future research.\n- The empirical results seem to show potential when compared to the baselines.\n\n### Weaknesses\n- Sections 1 and 2 of the paper lack a clear structure, making it difficult to follow the subsections and connect them to the problem being addressed.\n- The current framework does not adequately resolve error feedback. Additionally, further exploration is needed on how to interact with the model to fix these errors.\n- The evaluation is insufficient. Including more benchmarks and more baselines (e.g., [1, 2]) would be beneficial for better illustrating the performance of the proposed method.\n\n[1] Faith and fate: Limits of transformers on compositionality. Nouha Dziri et al. NeurIPS 2023.\n\n[2] Step-by-Step Reasoning to Solve Grid Puzzles: Where do LLMs Falter? Nemika Tyagi et al. EMNLP 2024.", "was_revised": true, "final_justification": "My rating for this paper is a borderline accept. Although the paper successfully proves the effectiveness of symbolic system integration for logic problems, it would be significantly strengthened by a more comprehensive comparison with prior work.", "rebuttal": "- Z3py is a Python wrapper that maps closely to SMT2 statements, but provides operator overloads that allow expressing certain constraints in a more Pythonic fashion. However, the formulas created are fundamentally still expressed over Z3’s domain, meaning that important Python features that Logic.py provides, like classes or even just repeated assignments to the same variable, are unavailable to the model. We would thus expect that without significant extensions in this regard, z3py as a DSL would not match Logic.py’s performance.\n- We limit the number of generations to at most 5 per problem. We collected data about restarts and observed that most problems can be solved in 1-3 attempts.\n- In our ZebraLogicBench benchmark run of 1000 samples, we observe 51 occurrences of unsatisfiable constraints across all attempts and tasks, and 70 occurrences of syntax errors in Logic.py. Of the 9.3% of puzzles where our approach did not produce an (entirely) correct solution, in 2.9% of cases we were not able to produce a solution at all in five attempts, due to the aforementioned syntax or unsatisfiability errors. In the remaining 6.4% of cases, Polymath produced a valid, but incorrect constraint and thus produced an incorrect solution."}]

Author rebuttal:

Meta-review: The reviewers believe the paper has value and presents an original approach for solving formal problems by formalizing them using an LLM and then solving the problem. The authors defended their position well.
Decision: Accept (poster)