Toward a General Framework for Evaluating Per-Domain Generalization Using LLMs, Theorem Provers, and Statistical Model Checking

Abstract

Generalized planning aims to synthesize generalized plans that can solve any instance of a fixed domain. Evaluating these methods is difficult because planning domains usually describe an infinite family of instances. Recent work proposed evaluating generalized planning methods on randomly generated instances of increasing size until statistical guarantees on the performance can be provided. However, this approach does not support generating instances from specific distributions, meaning it can only evaluate the average generalization across the domain, potentially hiding failures on rare but critical instances. In this work, we propose an efficient and flexible approach to targeted instance generation, which is based on the idea that we can modify existing instance generators using large language models (LLMs). Concretely, we specify instance distributions using first-order logic constraints and prompt an LLM to modify an existing instance generator such that it only returns instances fulfilling the given constraints. We then use a theorem prover to verify that the instances returned by the resulting generator fulfill the given constraints. Any incorrectly generated instances are used in an iterative feedback loop with the LLM. We then plug the instance generators into an evaluation framework that specifies a generic agent interface and is compatible with off-the-shelf statistical model checking tools. The result is a first step toward a general evaluation framework for per-domain generalization, which can evaluate any generalized planning approach according to any property on any distribution of instances from a given domain.

@inproceedings{mullerTowardAGeneralFramework2026,
 author = {Müller, Nicola J. and Rudolph, Naya and Taitler, Ayal and Gros, Timo P.},
 booktitle = {Workshop on Planning in the Era of LLMs at ICAPS-26},
 title = {Toward a General Framework for Evaluating Per-Domain Generalization Using LLMs, Theorem Provers, and Statistical Model Checking},
 url = {https://openreview.net/pdf?id=MLnzKKBdT4},
 year = {2026}
}