Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Ability of Transformers to Verify Plans

Yash Sarrof, Yupei Du, Katharina Stein, Alexander Koller, Sylvie Thiébaux, Michael Hahn

Abstract

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.

On the Ability of Transformers to Verify Plans

Abstract

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.
Paper Structure (8 sections, 2 theorems, 4 figures, 1 table)

This paper contains 8 sections, 2 theorems, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background & Task Definition
  3. Planning
  4. Planning Subclasses & Our Generalization Setting
  5. C-RASP
  6. Theoretical Results
  7. Generalization over a Fixed Universe
  8. Generalization over a Variable Universe

Key Result

Theorem 3.1

Let ${\cal D}$ be a planning domain and $O$ a fixed set of objects. Consider the language $L_{{\cal D}, O}$ consisting of all sequences $\langle I, \pi, G \rangle$ where $\pi$ is a valid plan for the planning instance $\langle {\cal D}, O, I, G \rangle$. 1. (Delete-Free & Well-Formed) If ${\cal D}$

Figures (4)

  • Figure 1: Overview of our results
  • Figure 2: Heavy Grippers domain. We omit the empty condition sets for the effects in $move$ and $drop$ which are unconditional.
  • Figure 3: Valid plan for a Heavy Grippers instance with 1 gripper, 2 balls and 2 rooms. The goal $G = \{\text{at}(\text{B1},\text{RoomB} ), \text{at}(\text{B2}, \text{RoomA})\}$ is to swap the balls in our rooms. Ball B1 is heavy and requires charge, making moving the only legal action in $I$. The robot then picks B2 from RoomB, moves, drops it in RoomA. It needs charge so it moves back and forth before picking B1, moving and dropping it in RoomB
  • Figure 4: Example from the Colors domain (Fig. \ref{['fig:color']}), where actions add balls of a given color to a bag or remove all balls of a given color from a bag. (a) Well-Formed: balls of the same color cannot be added if already present, and can't be removed if not in the bag. Such alternation allows the truth of “Is a color in the bag?” to be determined by simply counting add versus remove actions from the initial state. (b) STRIPS: In general STRIPS, determining the truth value requires identifying the last action that actually changed the state, making it equivalent to solving the FlipFlop language.

Theorems & Definitions (5)

  • Theorem 3.1: Fixed Universe
  • proof : Proof Sketch
  • Theorem 3.2: Informal version of Theorem \ref{['thm:guarantee']}
  • Definition 3.3: Match Predicate
  • Definition 3.4: $\textbf{C*-RASP}$