On the Ability of Transformers to Verify Plans

Transformers have shown inconsistent success in AI planning tasks, and theoretical understanding of when generalization should be expected has been limited. We take important steps towards addressing this gap by analyzing the ability of decoder-only models to verify whether a given plan correctly solves a given planning instance. To analyse the general setting where the number of objects -- and thus the effective input alphabet -- grows at test time, we introduce C*-RASP, an extension of C-RASP designed to establish length generalization guarantees for transformers under the simultaneous growth in sequence length and vocabulary size. Our results identify a large class of classical planning domains for which transformers can provably learn to verify long plans, and structural properties that significantly affects the learnability of length generalizable solutions. Empirical experiments corroborate our theory.

Transformer-based large language models often perform inconsistently on planning problems, where the goal is to follow a sequence of actions to reach a desired outcome. To better understand why this happens, we ask: after seeing short example plans, can a Transformer learn to check whether a much longer proposed plan is correct, even when it involves many more objects than seen during training? To answer this, we introduce C*-RASP, a general framework for analyzing how Transformers perform when both the length of test examples and the number of objects in them become much larger than during training. C*-RASP builds on the successful C-RASP framework, which studied cases where only the input length grows. Using our framework, we are able to find certain kinds of plans that transformers can learn to verify and certain other ones which they cannot. Our experiments help confirm these predictions, giving us a first step toward understanding the mysterious performance of Transformers on planning problems.