Near Verification, Far from Guaranteed: LLM–Only PDDL Repair
Abstract
AI planning is concerned with finding a sequence of actions that achieves a specified goal. It relies on explicit models of the world, commonly represented in the Planning Domain Definition Language (PDDL). An active line of research investigates how errors in such models can be detected and repaired. For example, users may provide positive test plans that must be valid solutions and negative test plans that must fail during execution. Automated repair methods then modify the PDDL model to satisfy these constraints. In this setting, the test-plan constraints serve as verification conditions: a repaired model is considered correct with respect to the provided tests if it satisfies all of them. In this paper, we evaluate the ability of recent open-weight large language models to perform this repair task using an LLM-only approach. Our experiments show that the symbolic baseline achieves an F1 score of .49, while the best-performing LLM reaches .87 with high reasoning effort, an absolute improvement of .38. However, that setting has a mean test pass rate of only .82, falling to .06 on the Thoughtful domain; even the best setting that includes the test traces reaches only .92. Thus, current open-weight models cannot guarantee satisfaction of the test constraints required for reliable automated model repair. We call for more sophisticated LLM-symbolic pipelines that combine these semantic gains with symbolic test-satisfaction guarantees.