Tag
This paper proposes property-guided LLM program synthesis, using counterexample-guided inductive synthesis (CEGIS) to provide concrete feedback when a candidate program fails a formal property, reducing the number of generations and evaluation costs. Applied to PDDL planning domains for synthesizing direct heuristic functions, the method outperforms prior approaches, generating seven times fewer programs and solving more tasks without search.