Research map / Large language models / Agents, code and math
Logic.py: Bridging the Gap between LLMs and Constraint Solvers
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces Logic.py, a Python-based DSL that Llama 3.1 70B uses to formalise Zebra logic puzzles, which are then solved by the CBMC constraint solver, reaching 91.4% on ZebraLogicBench.
Problem
LLMs struggle to directly solve search-based logic puzzles such as Zebra/logic grid puzzles, requiring reasoning over many interacting constraints.
Approach
Instead of having the LLM solve puzzles directly, prompt it to formalise the problem in a logic-focused Python-syntax DSL (Logic.py) with type decorators and nondeterministic variables, transpile it via libCST to C, and solve it with CBMC's SAT/SMT backend.
Key results
- Logic Agent reaches 91.4% puzzle accuracy on ZebraLogicBench, versus 24.9% for Llama 3.1 70B Instruct alone and 71.4% for o1-preview.
- Cell accuracy of 92.98% for Logic Agent vs 27.98% for Llama 3.1 70B Instruct.
- On Hard puzzles Logic Agent scores 88.89% vs 60.83% for o1-preview.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Add Logic.py formalisation and constraint-solver solving to direct Llama 3.1 70B Instruct puzzle solving | Llama 3.1 70B Instruct · ZebraLogicBench all | puzzle accuracy: 24.9 -> 91.4 | Helped |
| Add Logic.py formalisation and constraint-solver solving to direct Llama 3.1 70B Instruct puzzle solving | Llama 3.1 70B Instruct · ZebraLogicBench Easy | puzzle accuracy: 73.57 -> 97.86 | Helped |
| Add Logic.py formalisation and constraint-solver solving to direct Llama 3.1 70B Instruct puzzle solving | Llama 3.1 70B Instruct · ZebraLogicBench Hard | puzzle accuracy: 5.97 -> 88.89 | Helped |
| Add Logic.py formalisation and constraint-solver solving to direct Llama 3.1 70B Instruct puzzle solving | Llama 3.1 70B Instruct · ZebraLogicBench | cell accuracy: 27.98 -> 92.98 | Helped |
Surprising findings
- The paper notes that a 70B model with a constraint solver outperforms o1-preview by about 20 points on ZebraLogicBench.
Limitations
- Evaluated only on logic grid puzzles; generalisation to other search problems is untested.
- Error recovery restarts from scratch on syntax or unsatisfiable errors without feeding error info back to the model.
- ZebraLogicBench requires access request to a private dataset, and ambiguity detection was not implemented.
Experimental setup
Datasets: ZebraLogicBench
Benchmarks: ZebraLogicBench
Metrics: puzzle accuracy cell accuracy
Baselines: o1-preview o1-mini claude-3-5-sonnet gpt-4o Llama-3.1-405B-Instruct gemini-1.5-pro Mistral-Large-2 claude-3-opus Qwen2.5-72B-Instruct Meta-Llama-3.1-70B-Instruct
Builds on: Logic-LM SatLM CBMC libCST
Closest papers by meaning
- ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning (ICML 2025 · similarity 0.91)
- Reasoning-as-Logic-Units: Scaling Test-Time Reasoning in Large Language Models Through Logic Unit Alignment (ICML 2025 · similarity 0.88)
- Enhancing Reasoning Capabilities of LLMs via Principled Synthetic Logic Corpus (NeurIPS 2024 · similarity 0.88)
- QuestBench: Can LLMs ask the right question to acquire information in reasoning tasks? (NeurIPS 2025 · similarity 0.88)
- Automated Creation of Reusable and Diverse Toolsets for Enhancing LLM Reasoning (AAAI 2025 · similarity 0.87)
- Enigmata: Scaling Logical Reasoning in Large Language Models with Synthetic Verifiable Puzzles (NeurIPS 2025 · similarity 0.87)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.