Property-Guided LLM Program Synthesis for Planning

• URL: http://arxiv.org/abs/2605.16142v2
• Date: Mon, 18 May 2026 14:26:59 GMT
• Title: Property-Guided LLM Program Synthesis for Planning
• Abstract summary: Instead of scoring programs after evaluation, we check whether a candidate satisfies a formally defined property.<n>This feedback drastically reduces both the number of program generations and the evaluation cost.
• Score: 6.88204255655161
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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 generate stronger programs. We evaluate this approach on PDDL planning domains, asking the LLM to synthesize direct heuristic functions: every state reachable by strictly improving transitions has a strictly improving successor. A heuristic with this property leads hill-climbing algorithm directly to a goal state. A counterexample-guided repair loop generates one candidate program, checks the property over a training set, and returns the first case that violates the property. We evaluate our approach on ten planning domains with an out-of-distribution test set. The synthesized heuristics are effectively direct on virtually all test tasks, and compared to the best prior generation method our approach generates seven times fewer programs per domain on average, solves more tasks without using search, and requires several orders of magnitude less computation to evaluate candidates. Whenever a problem admits a verifiable property, property-guided LLM synthesis can reduce cost and improve program quality.

Related papers

• Overcoming the Weakest-Link Effect in LLM-Driven Program Optimization via Heterogeneous Edit Recombination [59.679182823718556]
  HERO is a program that generates diverse, non-overlapping atomic edits and then systematically selects and composes them into coherent program improvements using evaluator scores.<n>We evaluate HERO across algorithmic problems, strategy games, the design of LLM-based agentic systems, and robotic path planning.
  arXiv  Detail & Related papers  (2026-07-31T02:05:45Z)
• LLM-ERM: Sample-Efficient Program Learning via LLM-Guided Search [23.97383442759484]
  LLM-ERM is a propose-and-verify framework that replaces exhaustive enumeration with an LLM-guided search over candidate programs.<n>We show that coordinate-wise online mini-batch SGD requires many samples to learn certain short programs.<n>These results indicate that language-guided program synthesis recovers much of the statistical efficiency of finite-class ERM.
  arXiv  Detail & Related papers  (2025-10-16T06:10:11Z)
• Do AI models help produce verified bug fixes? [62.985237003585674]
  Large Language Models are used to produce corrections to software bugs.<n>This paper investigates how programmers use Large Language Models to complement their own skills.<n>The results are a first step towards a proper role for AI and LLMs in providing guaranteed-correct fixes to program bugs.
  arXiv  Detail & Related papers  (2025-07-21T17:30:16Z)
• Towards Effectively Leveraging Execution Traces for Program Repair with Code LLMs [13.708569727719434]
  Large Language Models (LLMs) show promising performance on various programming tasks.<n>We aim to remedy this potential blind spot by augmenting standard APR prompts with program execution traces.
  arXiv  Detail & Related papers  (2025-05-07T14:12:41Z)
• AIME: AI System Optimization via Multiple LLM Evaluators [79.03422337674664]
  AIME is an evaluation protocol that utilizes multiple LLMs that each independently generate an evaluation on separate criteria and then combine them via concatenation. We show AIME outperforming baseline methods in code generation tasks, with up to $62%$ higher error detection rate and up to $16%$ higher success rate than a single LLM evaluation protocol on LeetCodeHard and HumanEval datasets.
  arXiv  Detail & Related papers  (2024-10-04T04:03:24Z)
• Code Repair with LLMs gives an Exploration-Exploitation Tradeoff [16.80314690163063]
  Iteratively improving and repairing source code with large language models (LLMs) has emerged as a popular way of generating programs that would be too complex to construct in one shot. We show here that refinement exposes an explore-exploit tradeoff: exploit by refining the program that passes the most test cases, or explore by refining a lesser considered program.
  arXiv  Detail & Related papers  (2024-05-26T04:00:30Z)
• PiCO: Peer Review in LLMs based on the Consistency Optimization [48.48819141999387]
  We use peer-review mechanisms to measure large language models (LLMs) automatically.<n>We formalize it as a constrained optimization problem, intending to maximize the consistency of each LLM's capabilities and scores.<n>We propose three metrics called PEN, CIN, and LIS to evaluate the gap in aligning human rankings.
  arXiv  Detail & Related papers  (2024-02-02T18:49:26Z)
• Human-Instruction-Free LLM Self-Alignment with Limited Samples [64.69906311787055]
  We propose an algorithm that can self-align large language models (LLMs) iteratively without active human involvement. Unlike existing works, our algorithm relies on neither human-crafted instructions nor labeled rewards, significantly reducing human involvement. We show that our method can unlock the LLMs' self-generalization ability to perform alignment with near-zero human supervision.
  arXiv  Detail & Related papers  (2024-01-06T14:00:12Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.