Logic.py: Bridging the Gap between LLMs and Constraint Solvers

• 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.
• 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.
• 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.

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.
   
   Nevertheless, 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.
   
   We 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.
   
   Regarding 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.
   
   Of 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.
2. 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.
3. 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.
   
   However, 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.
   
   Fundamentally, 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.

Thank you for the effort in clarifying on my earlier concerns. I respond to your comments below:

1. I am glad to see that you can (I guess) hard-code Polymath to support these additional types of puzzles. In either case, the toolkit will obviously still unable to handle any kind of reasoning problem despite your reference to 3-SAT's NP-hardness. The reductions to SAT often aren't trivial and require mathematical thinking, which is far beyond the reach of automated solutions. Although I am happy to accept that your propose an initial solution, to be extended with additional capabilities in the future, the point is that your work does not propose a way to reduce any kind or problem expressible in natural language to a logical formalism to be tackled by a reasoning engine. Currently, it is a simple translator that can deal with a particular type of puzzle (multiple puzzles if you implement the above). So, as I see it, the toolkit will always be limited by a "list of problems" it can handle.

Also, related to this, the question is whether we should accept your work based on its current (automated) capabilities to support one kind of puzzle, or its potential of further improvement (involving much more of extra engineering). The answer isn't obvious to me.

2. Thank you.
3. I don't think I understand. If you have a reasoning problem that does not have a solution, no matter what you try to do in a feedback loop, it still does not have a solution. So, unless you have a mechanism to detect it once and for all, you will keep iterating: the LLM produces a formulation and the reasoning engine reports UNSAT. You need to be able to detect that the original problem (not its particular LLM's reformulation) is unsatisfiable in order stop the process.

1. To illustrate how Polymath would generalise to other problems, we manually ran its prompts against an exemplary sequence puzzle and Sudoku puzzle. These were in image form, and the model used in our benchmarks is not multi-modal, so we asked a multi-modal model to convert these two puzzles to text such that a text-only model could understand them.

Here is the result for the Sudoku puzzle:

This is a partially filled 9x9 Sudoku puzzle:

9 _ _ 2 _ _ 5 _ _
_ 8 7 _ _  9 3 _ _
_ _ _ _ 3 6 1 _ 7
_ 4 _ _ _ _ 9 2 _
7 _ 6 4 9 _ 8 _ _
8 _ 1 5 6 2 4 7 3
4 _ _ 3 2 _ 6 _ 5
1 _ _ _ 8 _ _ _ _
_ 3 8 _ _ 7 _ 1 _

Fill out the blank `_` cells while adhering to the standard rules of Sudoku.

Running this text puzzle through the same Polymath prompt as used for Zebra Logic, we again first ask the model to define a data structure to hold the solution. The answer was:

class Cell:
  value: Domain[int, range(1, 10)]
class Row:
  cells: list[Cell, 9]
class Solution:
  rows: list[Row, 9]

Then Polymath asks to generate the constraints. In our running example, this was:

def validate(solution: Solution) -> None:
  # Enforce that each row contains unique values
  for i in range(9):
    cell1 = nondet(solution.rows[i].cells)
    cell2 = nondet(solution.rows[i].cells)
    assume(cell1 is not cell2)
    assert cell1.value != cell2.value
  # Enforce that each column contains unique values
  # ...
  # Enforce the given clues from the puzzle statement
  assert solution.rows[0].cells[0].value == 9
  assert solution.rows[0].cells[3].value == 2
  assert solution.rows[0].cells[6].value == 5
  # ...

The model used Python features in validate that we did not implement yet in our CBMC back-end, but we believe this demonstrates how such puzzles can be handled with Polymath.

Similarly, for the sequence puzzle:

This is an arithmetic sequence puzzle. Fill in the missing variables such that each line forms a sequence of numbers, where the arithmetic difference between two numbers in the same line is the same.

A, B, 21
A, 7, C, 15
D, C, E, 21

Data structure:

class Solution:
  A: Domain[int, range(1, 31)]
  B: Domain[int, range(1, 31)]
  C: Domain[int, range(1, 31)]
  D: Domain[int, range(1, 31)]
  E: Domain[int, range(1, 31)]

Constraints:

def validate(solution: Solution) -> None:
  # Line 1: A, B, 21 is an arithmetic sequence
  # The difference between B and A equals the difference between 21 and B
  assert (solution.B - solution.A) == (21 - solution.B)

  # Line 2: A, 7, C, 15 is an arithmetic sequence
  # The difference between 7 and A equals the difference between C and 7
  # The difference between C and 7 equals the difference between 15 and C
  assert (7 - solution.A) == (solution.C - 7)
  assert (solution.C - 7) == (15 - solution.C)

  # Line 3: D, C, E, 21 is an arithmetic sequence
  # The difference between C and D equals the difference between E and C
  # The difference between E and C equals the difference between 21 and E
  assert (solution.C - solution.D) == (solution.E - solution.C)
  assert (solution.E - solution.C) == (21 - solution.E)

The choice of domain (max value 31) is questionable for the solution data structure, but we believe this demonstrates how such puzzles are well within the capabilities of our approach. In fact, any problem in NP can be mapped to a 3-SAT formula, and our approach can of course represent 3-SAT problems:

class Solution:
  x1: bool
  x2: bool
  # ...

def validate(solution: Solution) -> None:
  assert (solution.x1 or solution.x2 or solution.x3) and (solution.x4 ...

We would of course not expect the model to produce correct 3-SAT formalisations - at least not for puzzles which are not already in that form. After all, the entire design intent behind Logic.py is to give the model a more expressive and less error-prone API to describe problems in NP.

2. Thanks for the feedback, we will add these details to the experimental section. We were also surprised by these results and how coding capabilities seem to translate to a strong formalisation performance, given a safe DSL that leverages and reinforces these strengths.

3. The observation that we cannot identify valid but incorrect formalisations is accurate. This is true irrespective of unsatisfiability. If the model creates a valid but incorrect formalisation, we will get an incorrect solution. This incorrect solution might be an incorrect assignment, or it might be an incorrect UNSAT response. We restart on UNSAT in our agent implementation because UNSAT is outside the codomain of valid responses for both our benchmarks. We could choose to make UNSAT always part of the codomain, or we could delegate that choice to the model, since the model decides the codomain anyway. We suggest something similar for ambiguity. Across all ZebraLogicBench puzzles and attempts, we only observed 51 instances of unsatisfiable formulas, so this would affect our puzzle score by at most 5.1%.

• 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.
• 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.
• Thank you for pointing out these typos, we already addressed them in our paper.

• 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.
  
  At 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.

• 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.