Property-Guided LLM Program Synthesis for Planning
Andr\'e G. Pereira, Augusto B. Corr\^ea, Jendrik Seipp

TL;DR
This paper introduces a property-guided approach to LLM program synthesis that uses formal property checks and counterexamples to efficiently generate high-quality programs, especially in planning domains.
Contribution
The authors propose a novel property-guided synthesis method that reduces evaluation costs and improves program quality by leveraging formal properties and counterexamples during LLM-based program generation.
Findings
Reduces the number of program generations by seven times on average.
Synthesized heuristics are effective and direct in nearly all test tasks.
Requires significantly less computation compared to prior methods.
Abstract
LLMs have shown impressive success in program synthesis, discovering programs that surpass prior solutions. However, these approaches rely on simple numeric scores to signal program quality, such as the value of the solution or the number of passed tests. Because a score offers no guidance on why a program failed, the system must generate and evaluate many candidates hoping some succeed, increasing LLM inference and evaluation costs. We study a different approach: property-guided LLM program synthesis. Instead of scoring programs after evaluation, we check whether a candidate satisfies a formally defined property. When the property is violated, we stop the evaluation early and provide the LLM with a concrete counterexample showing exactly how the program failed. This feedback drastically reduces both the number of program generations and the evaluation cost, and can guide the LLM to…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
