Verification-Guided Abstraction Generation with Large Language Models for Generalized Planning

Generalized planning (GP), where a single policy solves multiple instances from a common planning domain, remains a challenging problem in AI. Abstraction plays an important role in GP, and Qualitative Numerical Planning (QNP) provides a compact abstract model for GP. However, useful QNP abstractions are difficult to construct and require substantial manual effort and expertise. We study whether QNP abstractions can be generated from PDDL domains and training instances by coupling LLM generation with symbolic reasoning. We propose a generate--debug--repair framework in which an LLM proposes abstract features and constructs a candidate QNP abstraction over the initial states, actions, and goals of the training instances. To improve reliability, we introduce verification-guided repair based on approximate soundness. Given a candidate abstraction, we solve it, validate the induced abstract instances, and apply one of two checking branches: SRCB tests an $m$-simulation relation between induced abstract and concrete instances to target approximate soundness, while PRCB tests whether the induced abstract plan refines into valid concrete solutions. Detected failures are converted into structured feedback for iterative repair. Experiments on seven GP benchmark domains with five LLMs show that verification-guided repair improves LLM-generated QNP abstractions over both single-pass generation and LLM self-repair, and helps some models produce abstractions that transfer across instances. Our results suggest that LLMs can serve as generators of symbolic abstractions for GP when coupled with formal error detection and structured repair feedback.