# Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving

arXiv: https://arxiv.org/abs/2309.16436 · HTML: https://mlsanity.com/paper/2309.16436/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 23 of its 40 references that are in the map.
- First posted on arXiv 28 Sep 2023.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 23 of 23)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [On the Opportunities and Risks of Foundation Models](https://mlsanity.com/paper/2108.07258/) (2021)
- [Survey of Hallucination in Natural Language Generation](https://mlsanity.com/paper/2202.03629/) (2022)
- [Inner Monologue: Embodied Reasoning through Planning with Language Models](https://mlsanity.com/paper/2207.05608/) (2022)
- [Language Models as Zero-Shot Planners: Extracting Actionable Knowledge for Embodied Agents](https://mlsanity.com/paper/2201.07207/) (2022)
- [CodeT5: Identifier-aware Unified Pre-trained Encoder-Decoder Models for Code Understanding and Generation](https://mlsanity.com/paper/2109.00859/) (2021)
- [On Faithfulness and Factuality in Abstractive Summarization](https://mlsanity.com/paper/2005.00661/) (2020)
- [CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis](https://mlsanity.com/paper/2203.13474/) (2022)
- [Recipes for building an open-domain chatbot](https://mlsanity.com/paper/2004.13637/) (2020)
- [LLM-Planner: Few-Shot Grounded Planning for Embodied Agents with Large Language Models](https://mlsanity.com/paper/2212.04088/) (2022)
- [The Next Decade in AI: Four Steps Towards Robust Artificial Intelligence](https://mlsanity.com/paper/2002.06177/) (2020)
- [Mixout: Effective Regularization to Finetune Large-scale Pretrained Language Models](https://mlsanity.com/paper/1909.11299/) (2019)
- [Hallucinated but Factual! Inspecting the Factuality of Hallucinations in Abstractive Summarization](https://mlsanity.com/paper/2109.09784/) (2021)
- [Scaling Transformer to 1M tokens and beyond with RMT](https://mlsanity.com/paper/2304.11062/) (2023)
- [On the Planning Abilities of Large Language Models (A Critical Investigation with a Proposed Benchmark)](https://mlsanity.com/paper/2302.06706/) (2023)
- [GPT Takes the Bar Exam](https://mlsanity.com/paper/2212.14402/) (2022)
- [An Efficient Memory-Augmented Transformer for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2210.16773/) (2022)
- [iDECODe: In-distribution Equivariance for Conformal Out-of-distribution Detection](https://mlsanity.com/paper/2201.02331/) (2022)
- [SKILL: Structured Knowledge Infusion for Large Language Models](https://mlsanity.com/paper/2205.08184/) (2022)
- [A Theory of Formal Synthesis via Inductive Learning](https://mlsanity.com/paper/1505.03953/) (2015)
- [ContraBERT: Enhancing Code Pre-trained Models via Contrastive Learning](https://mlsanity.com/paper/2301.09072/) (2023)
- [Attribution-driven Causal Analysis for Detection of Adversarial Examples](https://mlsanity.com/paper/1903.05821/) (2019)
- [Protein Folding Neural Networks Are Not Robust](https://mlsanity.com/paper/2109.04460/) (2021)

## Built on by (most cited first, 6 of 6)

- [On the Prospects of Incorporating Large Language Models (LLMs) in Automated Planning and Scheduling (APS)](https://mlsanity.com/paper/2401.02500/) (2024)
- [Large Language Models Make Sample-Efficient Recommender Systems](https://mlsanity.com/paper/2406.02368/) (2024)
- [Three Pathways to Neurosymbolic Reinforcement Learning with Interpretable Model and Policy Networks](https://mlsanity.com/paper/2402.05307/) (2024)
- [SafePilot: A Framework for Assuring LLM-enabled Cyber-Physical Systems](https://mlsanity.com/paper/2603.21523/) (2026)
- [Large Language Models in the Loop: A Stability- and Network-Aware Survey in Networked Control, Cyber-Physical, and Multi-Agent Systems](https://mlsanity.com/paper/2609.16599/) (2026)
- [SafeInferCom: Safe Inference-Time Compute via Verifier-Guided Mid-Generation Intervention for Robotic Task Planning](https://mlsanity.com/paper/2610.11223/) (2026)

## Abstract (arXiv)

Generative large language models (LLMs) with instruct training such as GPT-4 can follow human-provided instruction prompts and generate human-like responses to these prompts. Apart from natural language responses, they have also been found to be effective at generating formal artifacts such as code, plans, and logical specifications from natural language prompts. Despite their remarkably improved accuracy, these models are still known to produce factually incorrect or contextually inappropriate results despite their syntactic coherence - a phenomenon often referred to as hallucination. This limitation makes it difficult to use these models to synthesize formal artifacts that are used in safety-critical applications. Unlike tasks such as text summarization and question-answering, bugs in code, plan, and other formal artifacts produced by LLMs can be catastrophic. We posit that we can use the satisfiability modulo theory (SMT) solvers as deductive reasoning engines to analyze the generated solutions from the LLMs, produce counterexamples when the solutions are incorrect, and provide that feedback to the LLMs exploiting the dialog capability of instruct-trained LLMs. This interaction between inductive LLMs and deductive SMT solvers can iteratively steer the LLM to generate the correct response. In our experiments, we use planning over the domain of blocks as our synthesis task for evaluating our approach. We use GPT-4, GPT3.5 Turbo, Davinci, Curie, Babbage, and Ada as the LLMs and Z3 as the SMT solver. Our method allows the user to communicate the planning problem in natural language; even the formulation of queries to SMT solvers is automatically generated from natural language. Thus, the proposed technique can enable non-expert users to describe their problems in natural language, and the combination of LLMs and SMT solvers can produce provably correct solutions.