Provably Complete Generalized Planning with LLMs

# Provably Complete Generalized Planning with LLMs
Source: [https://arxiv.org/html/2609.27105](https://arxiv.org/html/2609.27105)
\\DeclareCaptionType

listing\[Listing\]\[List of Listings\]

###### Abstract

Generalized planning aims to compute a plan that solves all instances of a planning domain\. Recent work has used LLMs to automatically generate and debug such generalized plans in the form of Python programs and achieved perfect test data coverage for several domains\. However, whether these generalized plans are actually complete, i\.e\. solve all instances of the domain, could only be determined by manual evaluation\. Here, we present an approach for automatically generating generalized plans in Lean together with proofs of their completeness relative to a specification of the domain constraints provided as input\. We introduce a semantic\-preserving PDDL\-to\-Lean conversion, and use an LLM to generate both the generalized plan and the formal proof that it solves every instance satisfying the domain constraints\. The correctness of the completeness proof is determined by Lean’s kernel\. We evaluate our approach on 13 commonly used benchmark domains, using GPT\-5\.6\-Sol as the LLM\. For 12 of the domains we obtain generalized plans together with valid completeness proofs\. This is a major advancement of the state of the art in automatic generalized\-plan completeness proofs\.

1Saarland Informatics Campus, Saarland University, Saarbrücken, Germany

2German Research Center for Artificial Intelligence \(DFKI\), Saarbrücken, Germany

Correspondence: kstein@lst\.uni\-saarland\.de

## Introduction

Generalized planning aims to compute a plan that solve not only a single planning task, but all tasks from a given PDDL domain\. Such a strategy will typically contain loops and conditionals to deal with different cases and sizes of tasks\. For example, in the Spanner domain from the IPC Learning track 2023 a man can walk between linked locations, pick up spanners and use a spanner to tighten a loose nut which makes the spanner unusable\([Taitler et al\. 2024](https://arxiv.org/html/2609.27105#bib.bib14)\)\. As per the IPC problem generator, the links between locations form a one\-way path from the initial location \(a shed\) to the location of all loose nuts \(a gate\), and all usable spanners are located between the shed and the gate\. The goal is to tighten all loose nuts\. Figure[1](https://arxiv.org/html/2609.27105#Sx1.F1)shows an example planning task and a strategy that generalizes to all tasks of the domain\.

![Refer to caption](https://arxiv.org/html/2609.27105v1/spanner_ex_strat2.png)Figure 1:Illustration of an example planning task from the Spanner domain and a strategy for solving all Spanner tasks\.![Refer to caption](https://arxiv.org/html/2609.27105v1/approach.png)Figure 2:Illustrations of the main steps of our approach for obtaining generalized plans in Lean and proving their completeness\.A variety of approaches for formalizing and obtaining generalized plans have been proposed, including representing generalized plans as synthesized programs with loops and conditionals\([Srivastava et al\. 2011a](https://arxiv.org/html/2609.27105#bib.bib15);[Jiménez et al\. 2019](https://arxiv.org/html/2609.27105#bib.bib16), e\.g\.\)or general policies\([Bonet et al\. 2019a](https://arxiv.org/html/2609.27105#bib.bib19);[Bonet and Geffner 2018](https://arxiv.org/html/2609.27105#bib.bib21), e\.g\.\)\. Recently, there has been work on using Large Language Models \(LLMs\) to generate, and debug, generalized plans in the form of Python programs\([Silver et al\. 2024](https://arxiv.org/html/2609.27105#bib.bib6);[Stein et al\. 2026](https://arxiv.org/html/2609.27105#bib.bib8)\), with[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8)achieving perfect \(100%\\%\) coverage on the test datasets for 14 benchmark domains\. Yet such empirical evidence is limited to a set of example tasks \(the test dataset\)\. Do the generalized plans actually solve*all*tasks in the domains?

[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8)showed through a manual analysis that this is indeed the case \(similar manual analyses were done by[Drexler et al\. \(2022\)](https://arxiv.org/html/2609.27105#bib.bib22)and[Francès et al\. \(2021\)](https://arxiv.org/html/2609.27105#bib.bib33)\)\. But how to lead this kind of proof automatically?*Given the PDDL description of a domain, as well as some specification of the set of domain instances \(tasks in the domain\) that a generalized plan should solve, how to automatically obtain a generalized plan that provably solves all these instances?*We refer to this challenge as the problem of computing*complete*generalized plans\.

Earlier work on this challenge identified a restricted class of \(so\-called one\-dimensional\) planning problems where complete generalized plans can be found automatically using logical reasoning techniques\([Hu and Levesque 2010](https://arxiv.org/html/2609.27105#bib.bib32)\)\. Another strand of work has addressed the complementary challenge of, given a generalized plan, or as part of the computation of the generalized plan, determining a set of instances which the plan is guaranteed to solve\([Srivastava et al\. 2011a](https://arxiv.org/html/2609.27105#bib.bib15);[Bonet et al\. 2019b](https://arxiv.org/html/2609.27105#bib.bib20), e\.g\.\)\. The key concept in the most recent work on this are so\-called sound abstractions, which underlie the generalized plan and guarantee faithfulness to a concrete set of instances\. Recent work has shown how to automatically prove such abstractions sound, and therewith solve the challenge of proving a given generalized plan complete\([Cui et al\. 2023](https://arxiv.org/html/2609.27105#bib.bib23)\)\. The empirical success with this method is, however, limited to simple domains and/or instance sets, such as clearing a single block in Blocksworld, the IPC Gripper domain, and Logistics with a single vehicle\.

In the present work, we leverage the power of LLMs to not only generate the generalized plans, but also the completeness proofs in a suitable formalization\. Specifically, we prove completeness of LLM\-generated generalized plans using Lean\([de Moura et al\. 2015](https://arxiv.org/html/2609.27105#bib.bib11)\), a functional programming language and theorem prover\. We generate the generalized plans directly in Lean, and automatically prove their completeness relative to*domain constraints*formalizing the set of instances\.

We automatically generate Lean code from the PDDL enforcing the domain semantics\. Following[Silver et al\. \(2024\)](https://arxiv.org/html/2609.27105#bib.bib6)and[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8), we let the LLM generate the generalized plan as a program that takes a problem instance as input and outputs a complete plan\. We then prompt the LLM to write a proof for the following theorem:LetGPbe the generated generalized plan\. IfIis a problem instance satisfying the domain constraints, thenGP\(I\)returns a plan where 1\) all actions are sequentially applicable and 2\) the resulting state satisfies the goal\.A valid proof for this theorem shows that the generalized planGPis complete\.111In our benchmarks, we only consider solvable problem instances\. If the domain constraints do not guarantee solvability, then there exists no proof of the theorem\.Apart from the PDDL itself, our approach requires as input only a specification of the domain constraints, as well as a specification of state invariants\. Everything else is completely automated, including the generation and debugging ofGPas per[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8), and the proof thatGPis complete\. Figure[2](https://arxiv.org/html/2609.27105#Sx1.F2)illustrates our approach\.

We empirically evaluate our approach on 13 commonly used benchmark domains \(a subset of the domains addressed by[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8)\)\. Using GPT\-5\.6\-Sol as the LLM, for 12 of these domains we obtain a generalized plan and a valid proof, showing automatically that the generalized plan is complete\. This is a major advancement of the state of the art in automatic generalized\-plan completeness proofs\.

## Background

#### PDDL planning\.

In our work we focus on planning domains and problems defined in the Planning Domain Definition Language \(PDDL\)\([McDermott 2000](https://arxiv.org/html/2609.27105#bib.bib7);[Haslum et al\. 2019](https://arxiv.org/html/2609.27105#bib.bib5)\)\. In PDDL, a planning task is specified by domain𝒟\\mathcal\{D\}and a problem instanceIIof the domain\. A domain is a pair𝒟=⟨𝒫𝒟,𝒜𝒟⟩\\mathcal\{D\}=\\langle\\mathcal\{P\}\_\{\\mathcal\{D\}\},\\mathcal\{A\}\_\{\\mathcal\{D\}\}\\ranglewhere𝒫𝒟\\mathcal\{P\}\_\{\\mathcal\{D\}\}defines the set of predicates for describing states and𝒜𝒟\\mathcal\{A\}\_\{\\mathcal\{D\}\}defines the set of action schemas\. Each predicateP∈𝒫𝒟P\\in\\mathcal\{P\}\_\{\\mathcal\{D\}\}takes a finite number of arguments, i\.e\. has an arity ofk≥0k\\geq 0\. Each action schemaA∈𝒜𝒟A\\in\\mathcal\{A\}\_\{\\mathcal\{D\}\}is a triplet⟨Arg​\(A\),Pre​\(A\),Eff​\(A\)⟩\\langle\\text\{Arg\}\(A\),\\text\{Pre\}\(A\),\\text\{Eff\}\(A\)\\ranglewhereArg​\(A\)\\text\{Arg\}\(A\)are the arguments of the action,Pre​\(A\)\\text\{Pre\}\(A\)defines its preconditions andEff​\(A\)\\text\{Eff\}\(A\)its effects\.

\(a\)\(b\)
Figure 3:PDDL examples from the Spanner domain\.We focus on domains that can be expressed by a subset of PDDL that is restricted to conjunctive conditions with negation\. Hence, all preconditions and effects are conjunctions of literals from𝒫\\mathcal\{P\}where all predicate arguments are also arguments of the action\. We refer to the positive preconditions and effects asPre\+\\text\{Pre\}^\{\+\}andEff\+\\text\{Eff\}^\{\+\}, and to the negative preconditions and effects asPre−\\text\{Pre\}^\{\-\}andEff−\\text\{Eff\}^\{\-\}respectively\. We requireEff\+​\(A\)∩Eff−​\(A\)=∅\\text\{Eff\}^\{\+\}\(A\)\\cap\\text\{Eff\}^\{\-\}\(A\)=\\emptyset\.

A problem instanceIIis a triplet⟨O,S0,G⟩\\langle O,S\_\{0\},G\\ranglewhereOOis a finite set of objects, potentially with types,S0S\_\{0\}defines the initial state andGGthe goal conditions\. BothS0S\_\{0\}andGGare defined in terms of ground atoms, i\.e\. predicates of the domain where the arguments are replaced by objectso∈Oo\\in O,p⁡\(o1,…,ok\)p\(o\_\{1\},\.\.\.,o\_\{k\}\)\. The initial state forms a set of atoms and is interpreted under the closed\-world assumption, which means that all atoms that are not listed as part of the initial state are false\. The goal is a conjunction of literals,G=G\+∪G−G=G^\{\+\}\\cup G^\{\-\}, that needs to be true at the end of the plan\. A statesssatisfies a goalGGiffG\+⊆s∧G−∩s=∅G^\{\+\}\\subseteq s\\wedge G^\{\-\}\\cap s=\\emptyset\. We writes⊧Gs\\models GifsssatisfiesGG\.

Figure[3\(a\)](https://arxiv.org/html/2609.27105#Sx2.F3.sf1)shows an excerpt from the PDDL Spanner domain \([3\(a\)](https://arxiv.org/html/2609.27105#Sx2.F3.sf1)\) and Figure[3\(b\)](https://arxiv.org/html/2609.27105#Sx2.F3.sf2)shows an example of a problem instance\.

An actiona⁡\(o1,…,ok\)a\(o\_\{1\},\.\.\.,o\_\{k\}\)is an instance of an action schemaAAgrounded by objects fromOO\. An actionaais applicable in a statessiff all its preconditions are satisfied inss, i\.e\.Pre\+​\(a\)⊆s∧Pre−​\(a\)∩s=∅\\text\{Pre\}^\{\+\}\(a\)\\subseteq s\\wedge\\text\{Pre\}^\{\-\}\(a\)\\cap s=\\emptyset\. Applying an actionaain a statessyields a successor states′s^\{\\prime\}wheres′=\(s∖Eff−​\(a\)\)∪Eff\+​\(a\)s^\{\\prime\}=\(s\\setminus\\text\{Eff\}^\{\-\}\(a\)\)\\cup\\text\{Eff\}^\{\+\}\(a\)\. We define the successor state functionγ:S×A→S\\gamma:S\\times A\\rightarrow Swhere S denotes the set of all states as follows: If an actionaais applicable in a statessthenγ⁡\(s,a\)=s′=\(s∖Eff−​\(a\)\)∪Eff\+​\(a\)\\gamma\(s,a\)=s^\{\\prime\}=\(s\\setminus\\text\{Eff\}^\{\-\}\(a\)\)\\cup\\text\{Eff\}^\{\+\}\(a\)\. Ifaais not applicable thenγ⁡\(s,a\)\\gamma\(s,a\)is undefined\. We extendγ\\gammato sequences of actions\[a1,…,an\]\[a\_\{1\},\.\.\.,a\_\{n\}\]by iterated application:γ⁡\(s,\[\]\)=s\\gamma\(s,\[\]\)=sandγ⁡\(s,\[a1,…,an\]\)=γ⁡\(γ⁡\(s,a1\),\[a2,…,an\]\)\\gamma\(s,\[a\_\{1\},\.\.\.,a\_\{n\}\]\)=\\gamma\(\\gamma\(s,a\_\{1\}\),\[a\_\{2\},\.\.\.,a\_\{n\}\]\), which is defined only if eachaia\_\{i\}is applicable in the state resulting from applying\[a1,…,ai−1\]\[a\_\{1\},\.\.\.,a\_\{i\-1\}\]toss\. We say a planπ\\piis applicable from a statessifγ⁡\(s,π\)\\gamma\(s,\\pi\)is defined\.

A planπ=\[a1,…,an\]\\pi=\[a\_\{1\},\.\.\.,a\_\{n\}\]is a solution for a planning task⟨𝒟,I⟩\\langle\\mathcal\{D\},I\\ranglewithI=⟨O,S0,G⟩I=\\langle O,S\_\{0\},G\\rangleif and only ifγ⁡\(S0,π\)\\gamma\(S\_\{0\},\\pi\)is defined andγ⁡\(S0,π\)\\gamma\(S\_\{0\},\\pi\)satisfiesGG\.

Domains can be typed, i\.e\. define a hierarchy of object types\. A typed domain can be converted into an equivalent untyped domain by converting types into unary predicates\.

PDDL does not provide a specification language for the set of problem instances considered\. Instead, in most of the planning literature, this is encoded implicitly through a fixed set of instances considered, or as part of the program code of a problem generator associated with the domain\. For example, the problem generator for the Spanner domain generates only instances where all nuts are loose in the initial state and need to be tightened in the end\. Such an implicit representation does not permit to reason about whether a generalized plan is complete w\.r\.t\. a \(possible infinite\) set of problem instances\. In our work here, we specify the instance set in terms of instance\-validity constraintsCCin Lean\.

#### Generalized planning\.

Research on generalized planning comprises a variety of different representations for generalized plans and different approaches to obtain them\. These include policies based on features and abstractions that are hand\-crafted\([Bonet and Geffner 2018](https://arxiv.org/html/2609.27105#bib.bib21)\)or learned\([Bonet et al\. 2019a](https://arxiv.org/html/2609.27105#bib.bib19)\), policies for qualitative numerical problems\([Srivastava et al\. 2011b](https://arxiv.org/html/2609.27105#bib.bib31)\), finite\-state controllers that augment a policy with an internal memory\([Bonet et al\. 2009](https://arxiv.org/html/2609.27105#bib.bib18)\)and directly synthesized programs with control flow structures such as loops and conditionals\([Jiménez et al\. 2019](https://arxiv.org/html/2609.27105#bib.bib16);[Srivastava et al\. 2011a](https://arxiv.org/html/2609.27105#bib.bib15), e\.g\.\)

More recently, approaches involving neural models have been proposed, including learning general policies with graph neural networks\([Ståhlberg et al\. 2022](https://arxiv.org/html/2609.27105#bib.bib17);[Ståhlberg et al\. 2025](https://arxiv.org/html/2609.27105#bib.bib30)\)and generating programmatic generalized plans using pretrained LLMs\.[Silver et al\. \(2024\)](https://arxiv.org/html/2609.27105#bib.bib6)and[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8)use LLMs to come up with strategies for solving all planning tasks from a specific domain and to implement these strategies in the form of Python functions that take a Python representation of a planning problem as input and return a sequence of actions\. Their approaches include an automated debugging loop for the Python programs and[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8)also include an automated debugging step of the strategies\. Here, we consider generalized plans in the form of executable programs that take a problem instance as input and return a plan\.

#### Completeness of generalized plans\.

Completeness guarantees for generalized plans have been approached in different ways\. One line of work restricts the representation of generalized plans itself\. For this restricted class of so\-called one\-dimensional planning problems, complete generalized plans can be found automatically using logical reasoning constraints\([Hu and Levesque 2010](https://arxiv.org/html/2609.27105#bib.bib32)\)\. A complementary line of work starts from a generalized plan and determines the characterization of the set of instances that the generalized plan solves\([Bonet et al\. 2019b](https://arxiv.org/html/2609.27105#bib.bib20)\), or computes the characterization of the set of covered instances jointly with the generalized plan\([Srivastava et al\. 2011a](https://arxiv.org/html/2609.27105#bib.bib15)\)\. The key concept underlying the most recent work in this direction is that of a sound abstraction: whenever the abstract generalized plan reaches the abstract goal, the resulting concrete plan is guaranteed to solve every concrete instance that is covered by the abstraction\.[Cui et al\. \(2023\)](https://arxiv.org/html/2609.27105#bib.bib23)show how to automatically prove the soundness of such abstractions, and hence automatically prove that the generalized plan is complete\. However, this has only been shown for very simple domains \(e\.g\. IPC Gripper\) and restricted set\-ups \(Logistics with one vehicle\) so far\. Another approach for establishing completeness is manual analysis, which can be applied to a larger variety of domains but at the cost of manual work by experts\.[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8),[Drexler et al\. \(2022\)](https://arxiv.org/html/2609.27105#bib.bib22)and[Francès et al\. \(2021\)](https://arxiv.org/html/2609.27105#bib.bib33)manually verified that their generated or hand\-crafted generalized plans solve all instances of a domain\.

#### Lean\.

Lean\([de Moura and Ullrich 2021](https://arxiv.org/html/2609.27105#bib.bib12)\)is a dependently typed functional programming language which enables the implementation of a generalized plan as an executable, type\-checked function directly in Lean\. Furthermore, Lean is also an interactive theorem prover\. So, it is used to write programs as well as to state and prove mathematical and program\-correctness theorems about them\. It is based on a dependent type theory where types may depend on values\. Lean is built on the Curry\-Howard correspondence, thus propositions are represented as types and a proof of a proposition is a term of that type\. Stating a theorem therefore amounts to writing down a type, while proving it amounts to constructing a term of that type\. A Lean representation is thus a sequence of*definitions*introducing functions and datatypes,*statements*expressing propositions and*proofs*constructing terms that inhabit the types of their propositions\. Type\-checking is what constitutes verification in Lean: if the term type\-checks, the statement counts as proven since a proof of a proposition is by constructing a term of the corresponding type\. Constructing such terms explicitly is impractical, so Lean offers a*tactic mode*to provide such proofs as a sequence of transformation steps, such as rewriting with an equation or performing induction\. Lean executes this sequence to construct the explicit proof term\. This term, along with definitions and previously proven lemmas it depends on, is provided to Lean’s*kernel*, a small trusted program that type\-checks it\.

## Lean Representations and Correctness

Our objective is to obtain domain\-specific generalized plans for PDDL planning domains and prove their completeness in Lean\. This requires a conversion from PDDL to Lean that faithfully preserves the semantics of the planning task\. In this section, we describe our Lean representation and the conversion\.

We use the subscript “L” to indicate that a concept is represented in Lean and no subscript for PDDL, e\.g\.IIrefers to PDDL problem instance andILI\_\{L\}to a Lean problem instance\. We write⟦⋅⟧\\llbracket\\cdot\\rrbracketfor the conversion operator that maps PDDL concepts to their Lean counterparts as defined in this section\.⟦I⟧\\llbracket I\\rrbrackettherefore refers to the specific problem instance obtained by applying the conversion to the PDDL instanceII\. We use the inversion of the operator, i\.e\.,⟦⋅⟧\\llbracket\\cdot\\rrbracket\-1, to refer to the conversion from Lean concepts back to their original PDDL counterpart\.

### Representing States and Instances

#### States\.

Our Lean representation of a PDDL state is split into two parts: astatic stateand adynamic stateas shown in Listing[1](https://arxiv.org/html/2609.27105#listing1)\. The static and dynamic parts together comprise everything that is required for capturing all parts of a PDDL state: the set of objects, and a boolean\-valued function for every predicate of the domain\.

We represent objects as natural numbersi∈ℕi\\in\\mathbb\{N\}, i\.e\. our conversion maps each PDDL objecto∈Oo\\in Oto a uniquei∈ℕi\\in\\mathbb\{N\}by enumeration, hence⟦⋅⟧\\llbracket\\cdot\\rrbracketis bijective onOO\. Each PDDL predicateP∈𝒫𝒟P\\in\\mathcal\{P\_\{D\}\}of aritykkis represented as a boolean curried functionPL:ℕk→B​o​o​lP\_\{L\}:\\mathbb\{N\}^\{k\}\\rightarrow Boolthat takeskkobjects as input and returns a truth value\. Since the predicate functions are total functions relative to the set of objects, this matches the closed\-world interpretation of PDDL states\. All predicate functions for which the truth assignments cannot be changed by any action are part of the static state part together with the set of objects\. For example, the predicate\(link ?l1 \- location ?l2 \- location\)becomes the functionlink\_p::ℕ\\mathbb\{N\}→\\rightarrowℕ\\mathbb\{N\}→B​o​o​l\\rightarrow Bool, and is part of the static state part because none of the action effects affect the connections between locations\. All other predicate functions are part of the dynamic part\. We compile away PDDL types by turning each type into a unary predicate\.

Given the object mappings, a PDDL statessis converted into a Lean statesLs\_\{L\}by defining the truth assignments of the predicate functions such that the following state correspondence relation holds uniquely:

###### Definition 1\(State Correspondence\)\.

Letssbe a PDDL state,sLs\_\{L\}a Lean state\.ssandsLs\_\{L\}correspond to each other, writtens∼sLs\\sim s\_\{L\}, if for every predicatePPand tuple of objects\(o1,…,ok\)\(o\_\{1\},\.\.\.,o\_\{k\}\),p⁡\(o1,…,ok\)∈sp\(o\_\{1\},\.\.\.,o\_\{k\}\)\\in siff⟦p⁡\(o1,…,ok\)⟧\\llbracket p\(o\_\{1\},\.\.\.,o\_\{k\}\)\\rrbracket=PL​\(i1,…,ik\)=P\_\{L\}\(i\_\{1\},\.\.\.,i\_\{k\}\)returns true, whereij=i\_\{j\}=⟦oj⟧\\llbracket o\_\{j\}\\rrbracket\.

#### Instances\.

Encoding a PDDL goal condition follows a similar principle, but differs in two key aspects\. First, predicates in the goal are defined as partial functions, as shown in Listing[1](https://arxiv.org/html/2609.27105#listing1), whereO​p​t​i​o​n​B​o​o​lOption\\ Bool:nonemeans that the atom is unconstrained, whilesome brequires the state to assign it the truth valueb\. Second, the goal is defined only in terms of the predicate functions for which truth assignments can change, i\.e\. the dynamic part of the state\. We refer to the goal function for a predicateP∈𝒫𝒟P\\in\\mathcal\{P\_\{D\}\}asP​GLPG\_\{L\}\.

structureStatewhere

statics:StaticState

dynamic:DynamicState

structureStaticStatewhere

objects:Listℕ\\mathbb\{N\}

link\_p:ℕ\\mathbb\{N\}→\\rightarrowℕ\\mathbb\{N\}→\\rightarrowBool

location\_t:ℕ\\mathbb\{N\}→\\rightarrowBool

locatable\_t:ℕ\\mathbb\{N\}→\\rightarrowBool

\.\.\.

structureDynamicStatewhere

at\_p:ℕ\\mathbb\{N\}→\\rightarrowℕ\\mathbb\{N\}→\\rightarrowBool

carrying\_p:ℕ\\mathbb\{N\}→\\rightarrowℕ\\mathbb\{N\}→\\rightarrowBool

useable\_p:ℕ\\mathbb\{N\}→\\rightarrowBool

\.\.\.

structureGoalwhere

dynamic:GoalDynamic

structureGoalDynamicwhere

at\_p:ℕ\\mathbb\{N\}→\\rightarrowℕ\\mathbb\{N\}→\\rightarrowOptionBool

carrying\_p:ℕ\\mathbb\{N\}→\\rightarrowℕ\\mathbb\{N\}→\\rightarrowOptionBool

useable\_p:ℕ\\mathbb\{N\}→\\rightarrowOptionBool

\.\.\.

Listing 1Excerpt of the Lean state and goal representations of the PDDL Spanner domain \(Figure[3\(a\)](https://arxiv.org/html/2609.27105#Sx2.F3.sf1)\)\.A PDDL goal is converted into a Lean goal analogously to a state:⟦G⟧\\llbracket G\\rrbracketis created such that for every predicatePPof aritykkand tuple of objects,P​GL​\(i1,…,ik\)=PG\_\{L\}\(i\_\{1\},\.\.\.,i\_\{k\}\)=true iffp⁡\(o1,…,ok\)∈G\+p\(o\_\{1\},\.\.\.,o\_\{k\}\)\\in G^\{\+\}andP​GL​\(i1,…,ik\)=PG\_\{L\}\(i\_\{1\},\.\.\.,i\_\{k\}\)=false iffp⁡\(o1,…,ok\)∈G−p\(o\_\{1\},\.\.\.,o\_\{k\}\)\\in G^\{\-\}and is undefined otherwise\. For example, if the goal specifies that nutn​u​t​1nut1needs to be tightened but does not specify the location of the manb​o​bbob, and⟦n​u​t​1⟧\\llbracket nut1\\rrbracket=3=3and⟦b​o​b⟧\\llbracket bob\\rrbracket=4=4thentightened\_p\(3\)G\{\}\_\{G\}\(3\)returns true andat\_p\(4,o\)G\{\}\_\{G\}\(4,o\)returns none for anyo∈Oo\\in O\(see Figure[5](https://arxiv.org/html/2609.27105#A2.F5)in Appendix for a full example of a converted problem instance\)\.

Thegoal satisfaction relation,⊧L\\models\_\{L\}, is defined in Lean as a functionSatisfiesGoal : State→\\rightarrowGoal→\\rightarrowProp\.SatisfiesGoal s gholds iff for every goal predicate and every argument, the corresponding predicate of the Lean statesagrees with the value thatgrequires wherevergrequires one\. We define the result as aProprather than aBoolbecause goal satisfaction appears in our completeness theorem \(Theorem[2](https://arxiv.org/html/2609.27105#Thmtheorem2)\), and a theorem statement must be a proposition\. Listing[2](https://arxiv.org/html/2609.27105#listing2)shows an excerpt for the Spanner domain\.

defSatisfiesGoal\(s:State\)\(g:Goal\):Prop:=

\(∀\\forallvar\_mvar\_l,

matchg\.dynamic\.at\_pvar\_mvar\_lwith

\|none=\>True

\|someb=\>s\.dynamic\.at\_pvar\_mvar\_l=b\)∧\\wedge

\(∀\\forallvar\_n,

matchg\.dynamic\.tightened\_pvar\_nwith

\|none=\>True

\|someb=\>s\.dynamic\.tightened\_pvar\_n=b\)∧\\wedge

\.\.\.

Listing 2Example of the Lean function checking for goal satisfaction\.A complete PDDL and Lean problem instance then correspond to each other if the following holds:

###### Definition 2\(Instance correspondence\)\.

A PDDL instanceI=⟨O,S0,G⟩I=\\langle O,S\_\{0\},G\\rangleand a Lean instanceIL=I\_\{L\}=⟦I⟧\\llbracket I\\rrbracket=⟨=\\langle⟦O⟧\\llbracket O\\rrbracket,⟦S0⟧\\llbracket S\_\{0\}\\rrbracket,⟦G⟧\\llbracket G\\rrbracket⟩\\ranglecorrespond to each other, writtenI∼ILI\\sim I\_\{L\}, ifS0∼S\_\{0\}\\sim⟦S0⟧\\llbracket S\_\{0\}\\rrbracketand for any statess:s⊧Gs\\models Giff⟦s⟧\\llbracket s\\rrbracket⊧L\\models\_\{L\}⟦G⟧\\llbracket G\\rrbracket

By construction, our conversion ensures that for each PDDL instanceII,I∼I\\sim⟦I⟧\\llbracket I\\rrbracket\.

### Representing Actions and Transitions

#### Actions\.

Actions are encoded as an inductive typePlanActionwith one constructor per PDDL action schema \(Listing[3](https://arxiv.org/html/2609.27105#listing3)\)\. We use an inductive type here rather than a structure as we did for states, because a structure in Lean has a single constructor, whereas actions form a choice among several schemas\. Lean requires that any function overPlanAction, such as the transition function, handles every constructor\. Each constructor fixes the arity of its schema, so that ill\-formed ground actions are rejected by Lean’s type checker\. A Lean ground action is simply a constructor applied to all its arguments, e\.g\.walk\(1,2,3\)\(1,2,3\)\. Since all ground actions thus share the typePlanAction, aLean planπL\\pi\_\{L\}is of typeList PlanAction\.

inductivePlanActionwhere

\|walk\(var\_s:ℕ\\mathbb\{N\}\)\(var\_e:ℕ\\mathbb\{N\}\)\(var\_m:ℕ\\mathbb\{N\}\)

\|pickup\_spanner\(var\_l:ℕ\\mathbb\{N\}\)\(var\_s:ℕ\\mathbb\{N\}\)\(var\_m:ℕ\\mathbb\{N\}\)

\|tighten\_nut\(var\_l:ℕ\\mathbb\{N\}\)\(var\_s:ℕ\\mathbb\{N\}\)\(var\_m:ℕ\\mathbb\{N\}\)\(var\_n:ℕ\\mathbb\{N\}\)

Listing 3Example of the action constructors for the action schemas from the Spanner domain\.Preconditions and effects for each action schema are represented as a pair of Lean functions\. LikeSatisfiesGoal, the precondition function for an action schemaAAtakes the arguments of the encoded action and Lean statesLs\_\{L\}to return a proposition that the grounded action is applicable insLs\_\{L\}\. This function is defined as a conjunction where the conjuncts correspond to the Lean conversions of the literals in Pre\(A\)\(A\)\. Since state predicates are Boolean\-valued, each conjunct is an equation requiring the corresponding predicate function to returntruefor a positive literal, orfalsefor a negative literal\. Listing[4](https://arxiv.org/html/2609.27105#listing4)shows an example for the preconditions of the “walk” action schema from the Spanner domain\.

defwalkPre\(var\_s:ℕ\\mathbb\{N\}\)\(var\_e:ℕ\\mathbb\{N\}\)\(var\_m:ℕ\\mathbb\{N\}\)\(s:State\):Prop:=

s\.dynamic\.at\_pvar\_mvar\_s=true∧\\wedge

s\.statics\.link\_pvar\_svar\_e=true∧\\wedge

s\.statics\.location\_tvar\_s=true∧\\wedge

s\.statics\.location\_tvar\_e=true∧\\wedge

s\.statics\.man\_tvar\_m=true

defwalkEff\(var\_s:ℕ\\mathbb\{N\}\)\(var\_e:ℕ\\mathbb\{N\}\)\(var\_m:ℕ\\mathbb\{N\}\)\(s:State\):State:=

\{swithdynamic:=\{

s\.dynamicwith

at\_p:=

funvar\_m’var\_e’=\>

ifvar\_m’=var\_m∧\\wedgevar\_e’=var\_ethen

true

elseifvar\_m’=var\_m∧\\wedgevar\_e’=var\_sthen

false

else

s\.dynamic\.at\_pvar\_m’var\_e’\}\}

Listing 4Example of the Lean representation of the preconditions and effects of the action schema ‘walk’\.The effect function for an action schemaAAtakes the same input as the precondition function and returns the updated statesL′s^\{\\prime\}\_\{L\}, in which the predicate function of each add effect in Eff\(AA\) returnstrueat the affected arguments, each delete effect returnsfalse, and all other truth assignments are unchanged\. Listing[4](https://arxiv.org/html/2609.27105#listing4)shows this for the “walk” schema, where onlyat\_pis affected\. The Lean syntax\{s with dynamic := …\}builds a copy ofsin which only the named field differs, and the nesteds\.dynamic with …analogously replaces onlyat\_p; every other predicate function is carried over unchanged\. The newat\_preturnstruefor the man’s new locationvar\_e,falsefor the previous locationvar\_s, and the previous truth value for all other argument pairs\.

#### Transitions\.

By construction, for any ground actionaaof an action schemaAAand any statessthe following holds: the Lean precondition function returns true on⟦a⟧\\llbracket a\\rrbracketand⟦s⟧\\llbracket s\\rrbracketiffaais applicable inssand if so, then the effect function applied to⟦a⟧\\llbracket a\\rrbracketand⟦s⟧\\llbracket s\\rrbracketreturns a statesL′s^\{\\prime\}\_\{L\}that corresponds to the PDDL successor states′=γ⁡\(s,a\)s^\{\\prime\}=\\gamma\(s,a\)\.

The functions defined so far are specific to a single action schema, whereas the transitions of a planning task are defined for arbitrary ground actions\. We therefore combine them intoactionPreandactionApply\(Listing[5](https://arxiv.org/html/2609.27105#listing5)\), which take an arbitraryPlanActionand a state as input\. Lean accepts these definitions only if they match exhaustively over every constructor ofPlanAction, so all action schemas of the domain are covered, each branch calling the precondition or effect function of its corresponding schema\. Together,actionPreandactionApplyform the Lean counterpartγL\\gamma\_\{L\}to the PDDL successor state functionγ\\gamma, withγL​\(sL,aL\):=\\gamma\_\{L\}\(s\_\{L\},a\_\{L\}\):=actionApply\(aL,sL\)\(a\_\{L\},s\_\{L\}\)ifactionPre\(aL,sL\)\(a\_\{L\},s\_\{L\}\)is true and undefined otherwise\. Unlikeγ\\gamma,actionApplyis a total function by itself, and reproduces the partial definition ofγ\\gammain combination withactionPre\. Figure[4](https://arxiv.org/html/2609.27105#Sx3.F4)\(left\) illustrates the following lemma:

###### Lemma 1\(Action Transitions Commute\)\.

For any statessand ground actionaa,γ⁡\(s,a\)\\gamma\(s,a\)is defined iffγL​\(𝐶𝐿𝑂𝑆𝐸\\gamma\_\{L\}\(⟦s⟧\\llbracket s\\rrbracket,⟦a⟧\\llbracket a\\rrbracket\)\)is defined\. Ifγ⁡\(s,a\)=s′\\gamma\(s,a\)=s^\{\\prime\}andγL​\(𝐶𝐿𝑂𝑆𝐸\\gamma\_\{L\}\(⟦s⟧\\llbracket s\\rrbracket,⟦a⟧\\llbracket a\\rrbracket𝑂𝑃𝐸𝑁\)=sL′\)=s^\{\\prime\}\_\{L\}thensL′=s^\{\\prime\}\_\{L\}=⟦s′⟧\\llbracket s^\{\\prime\}\\rrbracket\.

defactionPre:PlanAction→\\rightarrowState→\\rightarrowProp

\|\.walkvar\_svar\_evar\_m,s=\>walkPrevar\_svar\_evar\_ms

\|\.pickup\_spannervar\_lvar\_svar\_m,s=\>pickup\_spannerPrevar\_lvar\_svar\_ms

\|\.tighten\_nutvar\_lvar\_svar\_mvar\_n,s=\>tighten\_nutPrevar\_lvar\_svar\_mvar\_ns

defactionApply:PlanAction→\\rightarrowState→\\rightarrowState

\|\.walkvar\_svar\_evar\_m,s=\>walkvar\_svar\_evar\_ms

\|\.pickup\_spannervar\_lvar\_svar\_m,s=\>pickup\_spannervar\_lvar\_svar\_ms

\|\.tighten\_nutvar\_lvar\_svar\_mvar\_n,s=\>tighten\_nutvar\_lvar\_svar\_mvar\_ns

Listing 5Example of the Lean applicability and state update functions for the Spanner domain\.s\{\\lx@inpgf@ignorespaces s\}⟦s⟧\{\\lx@inpgf@ignorespaces\\llbracket s\\rrbracket\}s′\{\\lx@inpgf@ignorespaces s^\{\\prime\}\}⟦s′⟧\{\\lx@inpgf@ignorespaces\\llbracket s^\{\\prime\}\\rrbracket\}⟦⋅⟧\\scriptstyle\{\\lx@inpgf@ignorespaces\\llbracket\\cdot\\rrbracket\}γ⁡\(s,a\)\\scriptstyle\{\\lx@inpgf@ignorespaces\\gamma\(s,a\)\}γL​\(⟦s⟧,⟦a⟧\)\\scriptstyle\{\\lx@inpgf@ignorespaces\\gamma\_\{L\}\(\\llbracket s\\rrbracket,\\llbracket a\\rrbracket\)\}⟦⋅⟧\\scriptstyle\{\\lx@inpgf@ignorespaces\\llbracket\\cdot\\rrbracket\}\(a\)Single\-action transition\.S0\{\\lx@inpgf@ignorespaces S\_\{0\}\}⟦S0⟧\{\\lx@inpgf@ignorespaces\\llbracket S\_\{0\}\\rrbracket\}sn\{\\lx@inpgf@ignorespaces s\_\{n\}\}⟦sn⟧\{\\lx@inpgf@ignorespaces\\llbracket s\_\{n\}\\rrbracket\}⟦⋅⟧\\scriptstyle\{\\lx@inpgf@ignorespaces\\llbracket\\cdot\\rrbracket\}γ⁡\(S0,π\)\\scriptstyle\{\\lx@inpgf@ignorespaces\\gamma\(S\_\{0\},\\pi\)\}γL​\(⟦S0⟧,⟦π⟧\)\\scriptstyle\{\\lx@inpgf@ignorespaces\\gamma\_\{L\}\(\\llbracket S\_\{0\}\\rrbracket,\\llbracket\\pi\\rrbracket\)\}⟦⋅⟧\\scriptstyle\{\\lx@inpgf@ignorespaces\\llbracket\\cdot\\rrbracket\}\(b\)Full\-plan transition\.
Figure 4:Conversion⟦⋅⟧\\llbracket\\cdot\\rrbracketcommutes with each applicable ground action when applying this single action \(left\)\. Iterating the square over a full plan shows that⟦⋅⟧\\llbracket\\cdot\\rrbracketalso commutes with applying a sequence of actions \(right\)\.

### From Single Steps to Plan Correctness

We lift applicability and state updates from single actions to sequences by defining two recursive functions,ValidPlanandrunPlan\(Listing[6](https://arxiv.org/html/2609.27105#listing6)\), the former stating the proposition under which a plan is applicable and the second computing the state it produces\. The empty plan is always applicable and leaves the state unchanged\. For a non\-empty list,ValidPlanrequires the first action to be applicable in the current state and the remaining actions to form a valid plan from the state that results from applying it, whilerunPlanapplies the first action and continues on the remaining list\. Notice thatrunPlanapplies an action regardless of whether its preconditions hold and applicability is captured separately byValidPlan\. Checking for the correctness of a plan hence requires both: a planπL\\pi\_\{L\}is a solution for a problem instance with the initial stateS0​LS\_\{0L\}and the goalGLG\_\{L\}iffValidPlan\(πL,S0​L\\pi\_\{L\},S\_\{0L\}\) is true andrunPlan\(πL,S0​L\\pi\_\{L\},S\_\{0L\}\) satisfiesGLG\_\{L\}\(seecorrectSolution, Listing[6](https://arxiv.org/html/2609.27105#listing6)\)\.

defValidPlan:ListPlanAction→\\rightarrowState→\\rightarrowProp

\|\[\],\_=\>True

\|a::as,s=\>actionPreas∧\\wedgeValidPlanas\(actionApplyas\)

defrunPlan:ListPlanAction→\\rightarrowState→\\rightarrowState

\|\[\],s=\>s

\|a::as,s=\>runPlanas\(actionApplyas\)

defcorrectSolution\(s:State\)\(g:Goal\)\(plan:ListPlanAction\):Prop

ValidPlanplans∧\\wedge

SatisfiesGoal\(runPlanplans\)g

Listing 6Lean functions for checking plan applicability and correctnes and for executing a plan\.Since initial states are states and since a single action corresponds to a plan of length 1, Lemma[1](https://arxiv.org/html/2609.27105#Thmlemma1)applies to the initial state of a problem instance and extends to plans by induction over plan length, as illustrated in Figure[4](https://arxiv.org/html/2609.27105#Sx3.F4)\(right\)\.

By construction, our PDDL to Lean conversion ensures that a PDDL problem instanceIIand its converted Lean counterpart⟦I⟧\\llbracket I\\rrbracketcorrespond\. Therefore, a PDDL plan and its Lean counterpart agree on applicability and goal satisfaction:

###### Lemma 2\(Plan Correctness Transfers to Conversion\)\.

LetI=⟨O,S0,G⟩I=\\langle O,S\_\{0\},G\\ranglebe an instance of𝒟\\mathcal\{D\}, and letπ=\[a1,…,an\]\\pi=\[a\_\{1\},\.\.\.,a\_\{n\}\]be a sequence of actions\. Thenπ\\piis a correct plan solvingIIiff⟦π⟧\\llbracket\\pi\\rrbracketis a correct plan solving the corresponding Lean planning problem⟦I⟧\\llbracket I\\rrbracket\.

Since⟦⋅⟧\\llbracket\\cdot\\rrbracketis bijective on objects and each PDDL action schema corresponds to exactly onePlanActionconstructor,⟦⋅⟧\\llbracket\\cdot\\rrbracketis bijective on ground action sequences and hence every Lean planπL\\pi\_\{L\}has a unique PDDL counterpart⟦πL⟧\\llbracket\\pi\_\{L\}\\rrbracket\-1\.

###### Theorem 1\(Soundness of Lean Plan Verification\)\.

LetI=⟨O,S0,G⟩I=\\langle O,S\_\{0\},G\\ranglebe an instance of𝒟\\mathcal\{D\}\. If we obtain a sequence of actions,πL:\\pi\_\{L\}:List PlanAction, and applyingcorrectSolutionto⟦S0⟧\\llbracket S\_\{0\}\\rrbracket,⟦G⟧\\llbracket G\\rrbracketandπL\\pi\_\{L\}returns true then convertingπL\\pi\_\{L\}from Lean to PDDL gives a planπ=\\pi=⟦πL⟧\\llbracket\\pi\_\{L\}\\rrbracket\-1such thatπ\\piis guaranteed to be a solution of the original PDDL problem instanceII\.

Theorem[1](https://arxiv.org/html/2609.27105#Thmtheorem1)follows directly from Lemma[2](https://arxiv.org/html/2609.27105#Thmlemma2):correctSolution\(⟦S0⟧\\llbracket S\_\{0\}\\rrbracket,⟦G⟧\\llbracket G\\rrbracket,πL\\pi\_\{L\}\) is by definition the Lean statement thatπL\\pi\_\{L\}is a correct plan solving⟦I⟧\\llbracket I\\rrbracketand the bidirectionality of Lemma[2](https://arxiv.org/html/2609.27105#Thmlemma2)gives that⟦πL⟧\\llbracket\\pi\_\{L\}\\rrbracket\-1is a correct plan solvingII\.

### Completeness of Generalized Plans

We now lift the correctness from individual plans to the completeness of generalized plans\. We define a generalized plan as a \(domain\-specific\) Lean functionsolvethat takes a Lean problem instance, separated into the initial state and the goal, as input and returns a plan in the form of a list ofPlanActionfor the input problem instance\. Listing[7](https://arxiv.org/html/2609.27105#listing7)shows the signature of a generalized plan\.

defsolve\(s:State\)\(g:Goal\):ListPlanAction:=

Listing 7Signature of the generalized plansolve, which takes a state and a goal and returns a plan\.Not every problem instance expressible in Lean needs to be handled by thesolvefunction\. As described in the Background, we define the set of problem instances by validity constraintsCCon valid initial states and goals\. We represent these constraints in Lean as two predicatesValidInit:S​t​a​t​e→P​r​o​pState\\rightarrow PropandValidGoal:S​t​a​t​e→G​o​a​l→P​r​o​pState\\rightarrow Goal\\rightarrow Prop\. Completeness of a generalized plansolveis then defined as follows:

###### Definition 3\(Generalized Plan Completeness\)\.

Let𝒟\\mathcal\{D\}be a domain\. A Lean functionsolvewith the signature of Listing[7](https://arxiv.org/html/2609.27105#listing7)is a complete generalized plan for𝒟\\mathcal\{D\}if, for every initial statesLs\_\{L\}and every goalGLG\_\{L\}that satisfyValidInit\(sL\)\(s\_\{L\}\)andValidGoal\(sL,GL\)\(s\_\{L\},G\_\{L\}\), the plan returned bysolvesL​gLs\_\{L\}g\_\{L\}is applicable fromsLs\_\{L\}and the resulting state satisfiesGLG\_\{L\}\.

Definition[3](https://arxiv.org/html/2609.27105#Thmdefinition3)guarantees the correctness of the generated plans for an infinite number of problem instances because there are infinitely many pairs of valid initial states and goals\. It is expressed as a Lean theorem of the type shown in Listing[8](https://arxiv.org/html/2609.27105#listing8)which expresses exactly the universal implication statement\. Listing[9](https://arxiv.org/html/2609.27105#listing9)shows the actual Lean declaration of the theorem which can be completed by a proof candidate that can then be checked by Lean’s kernel\. A Lean proof ofsolveComplete\(Listing[9](https://arxiv.org/html/2609.27105#listing9)\) for a specific candidatesolvefunction establishes exactly the completeness definition \(Def\.[3](https://arxiv.org/html/2609.27105#Thmdefinition3)\) for that candidate if accepted by Lean’s kernel:

solveComplete:∀\\forall\(s:State\)\(g:Goal\),

ValidInits→\\rightarrowValidGoalsg→\\rightarrow

ValidPlan\(solvesg\)s∧\\wedge

SatisfiesGoal\(runPlan\(solvesg\)s\)g

Listing 8Type of the completeness theorem statement for the generalized plansolve: for any valid initial state and goal,solvereturns an applicable plan that reaches the goal\.theoremsolveComplete

\(s:State\)

\(g:Goal\)

\(hinit:ValidInits\)

\(hgoal:ValidGoalsg\):

ValidPlan\(solvesg\)s∧\\wedge

SatisfiesGoal\(runPlan\(solvesg\)s\)g:=by

Listing 9Lean declaration of the completeness theorem statement in Listing[8](https://arxiv.org/html/2609.27105#listing8)\.###### Theorem 2\(Completeness GP Lean\)\.

Let𝒟\\mathcal\{D\}be a domain and letGPL\\text\{GP\}\_\{L\}be a candidate generalized plan for𝒟\\mathcal\{D\}, i\.e\. a Lean function with the signature shown in Listing[7](https://arxiv.org/html/2609.27105#listing7)\. If there exists a proof forsolveComplete\(Def\.[3](https://arxiv.org/html/2609.27105#Thmdefinition3)\) withsolve:=GPL:=\\text\{GP\}\_\{L\}, that is accepted by Lean’s kernel, thenGPL\\text\{GP\}\_\{L\}is a complete generalized plan for𝒟\\mathcal\{D\}: for every problem instanceILI\_\{L\}satisfying the domain constraints, applyingG​PLGP\_\{L\}toILI\_\{L\}returns a plan that is applicable from the initial state and reaches the goal\.

Theorem[2](https://arxiv.org/html/2609.27105#Thmtheorem2)itself requires no separate proof beyond Lean’s own soundness guarantee that whenever the kernel accepts a proof term of a proposition then the proposition holds\. Theorem[2](https://arxiv.org/html/2609.27105#Thmtheorem2)is, however, about the correctness of a generalized planG​PLGP\_\{L\}with respect to Lean problem instances and not the original PDDL\. We extend the correctness theorem in order to carry over to PDDL based on Lemma[2](https://arxiv.org/html/2609.27105#Thmlemma2)and Theorem[1](https://arxiv.org/html/2609.27105#Thmtheorem1)\. From Lemma[2](https://arxiv.org/html/2609.27105#Thmlemma2)and Theorem[1](https://arxiv.org/html/2609.27105#Thmtheorem1)we get that, given our conversion⟦⋅⟧\\llbracket\\cdot\\rrbracket, every PDDL instanceIIof a domain has a corresponding Lean instance, and every Lean plan that solves the converted problem instance has a PDDL counterpart that solves the original PDDL instance\. Therefore, correctness ofsolvein Lean transfers to a correctness guarantee for the original PDDL\.

###### Corollary 1\(Completeness of GP for PDDL Domain\)\.

LetG​PLGP\_\{L\}be a complete generalized plan in Lean for a domain𝒟\\mathcal\{D\}\(Theorem[2](https://arxiv.org/html/2609.27105#Thmtheorem2)\), and let⟦⋅⟧\\llbracket\\cdot\\rrbracketbe our PDDL to Lean conversion\. Then for everyI=⟨O,S0,G⟩∈ℐ𝒟I=\\langle O,S\_\{0\},G\\rangle\\in\\mathcal\{I\_\{D\}\}, GPL\(⟦I⟧\\llbracket I\\rrbracket\) returns a planπL\\pi\_\{L\}such thatπL=\\pi\_\{L\}=⟦π⟧\\llbracket\\pi\\rrbracketfor some planπ\\pithat solvesII\.

### Validity Constraints

The completeness theorem in Listing[9](https://arxiv.org/html/2609.27105#listing9)is proven relative toValidInitandValidGoal: these two Lean predicates specify which problem instances a generalized plan is required to solve by defining the constraints on valid problem instances, which we call validity constraints\. Our assumption here is that the user provides this specification along with the PDDL\. This makes sense as the user wants a generalized plan, and the set of instances which that plan should solve is naturally part of the problem specification\. In other words, we view generalized planning as the problem of plan generation replacing a single PDDL problem instance with a set of PDDL problem instances as captured by the validity constraints\. \(A trivial specification would admit all initial states and goals, but this rarely makes sense; consider e\.g\. Blocksworld initial states with cyclic towers\.\)

Listing[10](https://arxiv.org/html/2609.27105#listing10)shows examples of validity constraints for the Spanner domain\. The goal constraints take the goal and the initial state as parameters, hence allowing dependencies between initial state and goal\.

defAtLeastAsManySpannersAsNuts\(s:StaticState\):Prop:=

\(s\.objects\.filter\(funx=\>s\.nut\_tx\)\)\.length≤\\leq\(s\.objects\.filter\(funx=\>s\.spanner\_tx\)\)\.length

defValidLinkParam\(s:StaticState\):Prop:=

∀\\forallvar\_l1var\_l2,s\.link\_pvar\_l1var\_l2=true→\\rightarrows\.location\_tvar\_l1=true∧\\wedges\.location\_tvar\_l2=true

defLinkAcyclic\(s:StaticState\):Prop:=

∀\\foralll,¬\\negRelation\.TransGen\(funab=\>s\.link\_pab=true\)ll

defInitNutsLoose\(s:State\):Prop:=

∀\\foralln,s\.statics\.nut\_tn=true→\\rightarrows\.dynamic\.loose\_pn=true

defGoalAllNutsTightened\(initial:State\)\(g:Goal\):Prop:=

∀\\foralln,initial\.statics\.nut\_tn=true→\\rightarrowg\.dynamic\.tightened\_pn=sometrue

Listing 10Examples of constraints on valid instances of the Spanner domain\.Lean’s logic is the calculus of inductive constructions\([Pfenning and Paulin\-Mohring 1990](https://arxiv.org/html/2609.27105#bib.bib4)\), used for defining relations by induction and quantifying over predicates\. This allows directly expressing properties such as reachability and hence the absence of cycles of any length\. Thus constraints such as the location graph in Spanner forming a linear sequence are straightforward as we can define the transitive closure oflink\_pand state that no location is reachable from itself \(LinkAcyclic\)\.

The validity of an initial state \(ValidInit\) is then defined as a conjunction of the initial state constraints and validity of a state in general, which itself is again a conjunction of the constraints on the dynamic state part and the constraints on the static state part\. Similarly, goal validity of a state \(ValidGoal\) is defined as a conjunction of the goal constraints\.

## Generalized Planning in Lean with LLMs

The previous section described the theoretical foundation of our approach and the prerequisites for representing generalized plans for PDDL planning tasks in Lean and proving their completeness\. In this section, we now describe how we obtain the generalized plans and completeness proofs\. Given a PDDL domain and the specifications of the validity constraints, our pipeline 1\) automatically generates its Lean representation, 2\) lets an LLM generate a candidate generalized plansolve, and 3\) uses again an LLM to generate the proof thatsolvesatisfies the correctness theorem from Listing[9](https://arxiv.org/html/2609.27105#listing9)\. All these steps, including potential debugging of the LLM\-generated Lean code, are fully automated\.

#### Generating the Lean domain representation\.

In order to obtain the Lean formalizations, we implemented a domain\-independent Python converter that takes as input the PDDL domain, and optionally a PDDL problem, and outputs the converted Lean representation, i\.e\. the state, action and instance representations described above \(see Listings[1](https://arxiv.org/html/2609.27105#listing1),[3](https://arxiv.org/html/2609.27105#listing3)\-[5](https://arxiv.org/html/2609.27105#listing5)\)\. Our implementation for processing the PDDL covers a subset of PDDL that is restricted to conjunctive conditions with negation, no action costs, and can be applied to typed and untyped domains222In order to extend the approach to a larger PDDL fragment only the PDDL processing part needs to be adapted\.\. The converter is purely symbolic and deterministic333The only exception with respect to the determinism concerns the order of iterations, e\.g\. in which the actions are converted and objects are enumerated\. None of the iteration orderings, however, has any effect on the validity of our results\., and applies the conversion described in the previous section in the same structured way to any domain of the covered PDDL fragment\. Therefore, all claims and guarantees that depend on the specific conversion mechanism described before hold for the Lean representation of any domain obtained from our converter\.

#### Generating the generalized plan in Lean

To generate generalized plans with LLMs, we follow the process introduced by[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8), which consists of two main steps: 1\) deriving the pseudocode strategy for solving a planning domain, and 2\) implementing that strategy in a programming language\. As our focus here is on completeness proofs rather than on finding strategies, we start from the pseudocode strategies of[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8), check them and revise them if necessary\. We provide an LLM with the revised strategies as well as the complete Lean representation of the target domain and have it implement thesolvefunction \(Listing[7](https://arxiv.org/html/2609.27105#listing7)\) such thatcorrectSolution\(Listing[6](https://arxiv.org/html/2609.27105#listing6)\) holds\. This code is debugged in two steps\. Statically, Lean’s kernel must accept the code\. Dynamically, the candidate generalized plan is run on a set of debugging tasks and the plans it returns are converted to PDDL and validated with VAL\([Howey et al\. 2004](https://arxiv.org/html/2609.27105#bib.bib13)\)\. If either step fails, the LLM receives feedback about the specific error and is prompted to revise its generated code\. If the generated candidate generalized plan returns correct solutions for all debugging tasks within a defined number of iterations, the process moves on to the proof step\. An example of a generalized plan generated for the Spanner domain can be found in Listing[14](https://arxiv.org/html/2609.27105#LST14)\.

#### Generating the completeness proof\.

Once a generalized plan has been generated, we ask the LLM to prove that it is correct, i\.e\., to state and prove the correctness theorem shown in Listing[9](https://arxiv.org/html/2609.27105#listing9)\. As input, the LLM receives \(i\) the complete Lean code from the previous step, consisting of the Lean representation and the LLM\-generated generalized plan, \(ii\) lemmas stating that actions preserve state validity, described in the next section, and \(iii\) helper lemmas describing which parts of a state an action changes and which it leaves unchanged\. These helper lemmas are generated automatically from the PDDL by a symbolic, domain\-independent generator \(see Listing[12](https://arxiv.org/html/2609.27105#listing12)and[13](https://arxiv.org/html/2609.27105#listing13)in Appendix\)\.

We again use an automatic debugging procedure to let the LLM revise its generated proof in case the generated proof is rejected\. If Lean reports any error, or the proof fails one of the checks against cheating described below, the error message is passed back to the LLM, together with a prompt asking it to regenerate the complete proof\.

Depending on the specific planning domain and the concrete implementation of the generalized plan, completeness can be hard to prove and the simple, basic approach described may not work\. In particular, we observe that in these cases the LLM explicitly replies that proving completeness is too complex\. To address this we propose a second, iterative approach inspired by[Ospanov et al\. \(2025\)](https://arxiv.org/html/2609.27105#bib.bib24), which, as our experiments show, works better for those complex cases\. The LLM is given the same information as in the basic approach but is instructed to provide a proof sketch that states all lemmas it requires\. Notably, this approach allows the LLM to decide which lemmas it proves immediately in its first response and which are marked unproven for now\. The remaining lemmas are then proven in subsequent iterations\. The completeness proof is only accepted once it depends on no unproven lemmas\.

To debug the proof sketch, we split it into its individual declarations, i\.e\. definitions, lemmas and theorems\. These declarations are added to the Lean representation one at a time, checking the code after each addition\. When a declaration is rejected, the LLM revises the declaration based on the code accepted so far and the error message\. Thus, errors are repaired locally without discarding the parts Lean has already accepted in contrast to the basic approach where the complete proof needs to be regenerated\. The process ends when all declarations are accepted or the maximum number of iterations is reached\. During the debugging, to account for declarations missing in the initial sketch, the LLM is explicitly allowed to generate more declarations than the one that failed\. They are then inserted into the proof sketch at the same place as the declaration that is currently being debugged\.

#### Preventing LLM cheating\.

LLMs generating Lean code are known to find workarounds that make the code compile without establishing the intended result\([Wang et al\. 2026](https://arxiv.org/html/2609.27105#bib.bib1);[Paglieri et al\. 2026](https://arxiv.org/html/2609.27105#bib.bib2)\), and recent work analyzing Lean benchmarks has found related evaluation\-time loopholes that can affect the reliability of evaluation results\([Ammanamanchi et al\. 2026](https://arxiv.org/html/2609.27105#bib.bib3)\)\. There are three ways in which this can happen in our setting\. First, the LLM may changecorrectSolutioneither by directly editing the statement itself, e\.g\. adding hypotheses that make the statement easier to prove, or by altering the semantics, e\.g\. by redefining notation or introducing new definitions\([Paglieri et al\. 2026](https://arxiv.org/html/2609.27105#bib.bib2)\)\. Second, the proof may silently rely on unjustified axioms which do not appear in the theorem’s type\. Third, a proof may be accepted while bypassing Lean’s kernel checks due to metaprogramming or bugs in incremental compilation within Lean\.

We address these with four checks\. We reject code that alters how subsequent code is parsed or elaborated, such as custom notation or macros\. We further verify that the final code contains a theorem exactly as written in Listing[8](https://arxiv.org/html/2609.27105#listing8)\. Together, these rule out the first form of cheating\. For the second form of cheating, we check that the proof does not depend on axioms beyond the standard ones\.444https://lean\-lang\.org/doc/reference/latest/Axioms/\#standard\-axiomsFinally, for efficiency, our iterative debugging loop is performed incrementally in REPL\.555https://github\.com/leanprover\-community/replAs a sanity check, the complete code is rebuilt from scratch as a self\-contained module and rechecked by Lean’s standalone checker, thus ruling out the third form of cheating as well\.

#### Invariants\.

In addition to the types of constraints described above, we specify a set of state invariants: properties that hold in the initial state and remain true in any state reachable from it, such asNutTightenedLooseExhaustiveshown in Listing[11](https://arxiv.org/html/2609.27105#listing11)which specifies that each nut is always either tightened or loose\. Every invariant of this kind is a consequence of the initial state constraints together with the action schemas\. In practice, however, we provide these invariants explicitly as part of the valid state specification because doing so removes the burden of re\-deriving them from scratch from the LLM\. At the same time, adding them to the constraints does not add a substantial additional amount of work\. For example, without invariants, the initial state constraints need to include both a constraint that all nuts are loose \(InitNutsLoose\) and one specifying that no nut is tightened\. When addingNutTightenedLooseExhaustiveas an invariant constraint, the constraint about all nuts being not tightened becomes redundant\.

defNutTightenedLooseExhaustive\(s:State\):Prop:=

∀\\foralln,s\.statics\.nut\_tn=true

→\\rightarrows\.dynamic\.tightened\_pn=true∨\\vee

s\.dynamic\.loose\_pn=true

Listing 11Examples of a state invariant constraint of the Spanner domain\.We define aValidStateas a conjunction over all constraints that apply to arbitrary states \(i\.e\. not only initial states\)\. We then automatically generate one lemma per action schema for proving that applying the specific action in a valid state yields again a valid state\. Then, an LLM is prompted to generate the proof\. We include an automatic debugging loop where the LLM has up to five tries for generating these proofs\. Here, the LLM is prompted to generate, and debug, the proofs for all actions together instead of for each action individually\.

## Experiments

### Pipeline and Set\-up

We test our approach using GPT\-5\.6\-Sol with temperature set to 1 and reasoning set to high\. We select 13 of the 17 domains on which also[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8)ran their experiments\. We exclude Gripper because of its similarity to Grippers, Beluga because LLMs struggle to find generalized plans there\([Stein et al\. 2026](https://arxiv.org/html/2609.27105#bib.bib8)\)and Minigrid and Visitall as the specification of solvability is not straightforward666[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8)used a version of Visitall that allows missing cells in the grid\. For all the domains that we test our approach on except Rovers,[Stein et al\. \(2026\)](https://arxiv.org/html/2609.27105#bib.bib8)manually proved that their generalized plans were complete\. We define the domain constraints on valid instances based on the problem generators, example problems from datasets, potential domain descriptions, and the PDDL domain definition\. For each domain, we select six small problem instances from existing datasets as debugging tasks \(see Table[3](https://arxiv.org/html/2609.27105#A1.T3)in Appendix for sources of datasets\)\.

### Generalized Plans and Proofs

#### Results generalized plans\.

The approach for generating the generalized plan \(GP\) described above is applied for obtaining the GPs for all 13 domains\. We set the maximum number of debugging iterations to four\. Table[1](https://arxiv.org/html/2609.27105#Sx5.T1)presents the results\. For all 13 domains, the LLM successfully generated generalized plans that were accepted by Lean and returned plans that were accepted by VAL for all six debugging tasks\. The number of interactions \(N interactions\) refers to the number of input\-output pairs of the LLM generation process for the generalized plan \(GP\) and the proof \(Prf\.\), and includes both the initial versions generated by the LLM as well as the debugging iterations\. For 10 of the domains, the first generated version of the generalized plan already solved the debugging tasks, and for the other three domains a single debugging iteration was enough\. Given that we made sure to already provide the LLM a correct strategy for solving the domain, a low number of debugging iterations is expected here\.

#### Results proofs\.

As described above, we consider two different approaches for generating the completeness proofs: a basic approach where the complete proof is generated and debugged as a whole and an iterative approach where the LLM first generates a sketch of the proof and then debugs the individual declarations \(e\.g\., lemmas, definitions, theorems, etc\.\)\.

We first tested the basic approach for all domains with the maximum iterations for debugging set to six\. For 7 of the 13 domains, the LLM successfully completed the completeness statement from Listing[9](https://arxiv.org/html/2609.27105#listing9)with a proof that was accepted by Lean’s kernel\. The number of generated proof versions \(i\.e\. initial \+ debugging iterations\) and the time required for obtaining the generalized plans and proofs for these 7 domains are shown in the upper part of Table[1](https://arxiv.org/html/2609.27105#Sx5.T1)\.

For the other six domains, the LLM was not able to generate the completeness proof using the basic set\-up\. In particular, for all of these domains the LLM explicitly stated in the first response that providing a complete proof at once is not possible due to its complexity and the number of required additional lemmas\. We therefore ran the iterative approach for those six domains\. As the debugging is applied at the level of individual declarations here, we set the debugging limit such that the debugging terminates if the same declaration \(as identified by the name of e\.g\. the lemma\) is debugged six times in a row without success\. Using the iterative approach, we successfully obtain proofs accepted by Lean’s kernel for all domains except Transport\. The lower part of Table[1](https://arxiv.org/html/2609.27105#Sx5.T1)shows the maximum number of iterations required for the same declaration \(Decl\.\) as well as the total number of interactions \(Prf\.\) for obtaining the complete correct proof\.

Note, however, that the lack of a proof for Transport does not mean that the generalized plan does not solve all instances of the domain, but that the LLM was not capable of generating one\. In order to still get an idea of how well the generalized plan performs, we tested it on the easy and medium test splits of the IPC Learning track 2023\([Taitler et al\. 2024](https://arxiv.org/html/2609.27105#bib.bib14)\)on which it achieved perfect coverage\.

Table 1:Number of LLM interactions and run time of the pipeline \(in seconds\) for generating the generalized plan \(GP\) and its completeness proof \(Prf\.\)\. “N interactions” counts the number of interactions, i\.e\. input\-output pairs, with the LLM, including the initial generation and all debugging iterations\. The upper part shows the domains for which the basic approach succeeded, the lower part shows the results using the iterative approach on the other domains\. For the iterative approach, “Decl\.” reports the maximum number of debugging iterations required for a single declaration\.
#### Generation times\.

Table[1](https://arxiv.org/html/2609.27105#Sx5.T1)also shows how long it takes to obtain the generalized plans and the completeness proofs\. The required time varies a lot between the different domains, ranging from 9 minutes for Heavy to almost one hour \(54 minutes\) for Rovers\. Generating the generalized plans takes significantly less time even if the number of iterations is only slightly higher\. As shown in Table[2](https://arxiv.org/html/2609.27105#Sx5.T2), the Lean code for the proofs consists also of significantly more individual declarations, both with respect to the number of declarations the LLM generates and the number of declarations already provided to the LLM in the prompt\. The number of declarations provided to the LLM is necessarily larger for the proof generation because it includes the complete Lean code \(provided and LLM\-generated\) for the generalized plan\.

Table 2:Number of Lean code declarations \(i\.e\., lemmas, theorems, and definitions\) involved in generating the generalized plan \(GP\) and its completeness proof \(Prf\.\)\. “Given” reports the number of declarations provided to the LLM as part of the prompt \(e\.g\., the domain formalization and, for proof generation, the complete GP code\); “LLM” reports the number of individual declarations generated by the LLM itself\.

## Related Work

#### Software verification\.

Verifying the correctness of synthesized programs has long been studied in software verification and program synthesis\. Classical work established that a verifier can be used not only to check a synthesized program in the end, but to guide synthesis itself, iteratively refining candidate programs against counterexamples until a verified implementation is found\([Solar\-Lezama et al\. 2006](https://arxiv.org/html/2609.27105#bib.bib35)\)\. More recently, this combination of synthesis and verification has been extended to use LLMs as the source of the candidate programs\.[Bhatia et al\. \(2024\)](https://arxiv.org/html/2609.27105#bib.bib29)use an LLM to jointly generate a program and a proof of its functional equivalence to a source program, translating both into an automated theorem prover to verify correctness for all program states rather than testing on a finite test set\.[Aggarwal et al\. \(2025\)](https://arxiv.org/html/2609.27105#bib.bib28)similarly address formally verified code generation by iteratively translating and refining candidate programs against feedback from a formal verifier, and[Chen et al\. \(2025\)](https://arxiv.org/html/2609.27105#bib.bib36)fine\-tune models on synthesized proof data for proof generation and debugging in Rust\.

In all these approaches, an external, trusted verifier provides the correctness guarantee for an LLM\-generated program, e\.g\. a transpiled function\([Bhatia et al\. 2024](https://arxiv.org/html/2609.27105#bib.bib29)\)or a Verus\-annotated Rust function\([Aggarwal et al\. 2025](https://arxiv.org/html/2609.27105#bib.bib28)\), but the guarantees are only checked once against one specification\. We adopt the same overall pattern here, but for programs that must remain correct across every valid instance of a planning domain, not a single specific input\-output specification\.

#### LLMs for theorem proving\.

[First et al\. \(2023\)](https://arxiv.org/html/2609.27105#bib.bib10)introduce an approach to automatically generate and repair complete proofs using LLMs based on feedback from the Isabelle proof assistant to iteratively debug incorrect generated proofs\. They fine\-tune models and evaluate them on a benchmark of general mathematical theorems rather than software or planning related theorems\.[Song et al\. \(2024\)](https://arxiv.org/html/2609.27105#bib.bib9)integrate LLM\-based tactic suggestions, proof search and premise selection directly into the Lean workflow, focusing on interactively developing proofs for math\. Most closely related to our proof\-debugging approach is the work by[Ospanov et al\. \(2025\)](https://arxiv.org/html/2609.27105#bib.bib24): they isolate failing sub\-lemmas in an LLM\-generated proof sketch and repair them individually, using a hybrid approach that combines automated solvers and LLM calls, instead of debugging the whole proof at once\. Their focus is on competition\-style mathematical benchmarks\.

#### Formally verified planning components\.

In ensuring the correct PDDL semantics in Lean, our work loosely relates to works on formal verification of components or aspects of planning\. Previous work has worked on formalizing classical planning domains for the purpose of verification\. One line of work formalizes the semantics of a PDDL fragment directly inside an interactive theorem prover:[Abdulaziz and Lammich \(2018\)](https://arxiv.org/html/2609.27105#bib.bib25)formalize STRIPS\-like PDDL in Isabelle/HOL and derive a formally verified plan validator, and follow\-up work extends this to a verified compositional planning algorithm\([Abdulaziz et al\. 2019](https://arxiv.org/html/2609.27105#bib.bib27)\)and a formally verified SAT\-based planner\([Abdulaziz and Kurz 2023](https://arxiv.org/html/2609.27105#bib.bib26)\)\. Another line of work lets planners emit independently checkable certificates alongside their output, without formalizing the planner itself:[Eriksson et al\. \(2017\)](https://arxiv.org/html/2609.27105#bib.bib37)introduce certificates of unsolvability that a planner\-independent validator can verify, and[Mugdan et al\. \(2023\)](https://arxiv.org/html/2609.27105#bib.bib38)extend this approach of certifying algorithms to certificates of plan optimality\. Like our work, both lines of work target machine\-checked guarantees in the context of classical planning but verify a fixed planning algorithm’s output, e\.g\. single plans, \(un\)solvability claims, rather than verifying correctness across the entire set of domain instances\.

## Conclusion

We introduce an approach for automatically obtaining generalized plans together with machine\-checked completeness proofs, using LLMs to generate both of them directly in Lean\. Out of 13 commonly used benchmark domains, our approach produced provably complete generalized plans in 12\. To our knowledge, this is the first time that generalized plans were automatically proved complete at such a scale, with prior work limited to simple domains and/or instance sets\. This is a major advancement of the state of the art in automatic generalized\-plan completeness proofs\.

## Acknowledgments

The work was partially funded by the Deutsche Forschungsgemeinschaft \(DFG, German Research Foundation\) under the project number 232722074 – SFB 1102\. It was also funded in part by the Deutsche Forschungsgemeinschaft – GRK 2853/1 “Neuroexplicit Models of Language, Vision, and Action” \- project number 471607914\. We thank Jan Reineke, Dan Fišer and Nicola Müller for insightful discussions\.

## References

- Abdulazizet al\.\(2019\)M\. Abdulaziz, C\. Gretton, and M\. NorrishA Verified Compositional Algorithm for AI Planning\.In10th International Conference on Interactive Theorem Proving \(ITP 2019\),J\. Harrison, J\. O’Leary, and A\. Tolmach \(Eds\.\),Leibniz International Proceedings in Informatics \(LIPIcs\), Vol\.141,Dagstuhl, Germany,pp\. 4:1–4:19\.Note:Keywords: AI Planning, Compositional Algorithms, Algorithm Verification, Transition SystemsExternal Links:ISBN 978\-3\-95977\-122\-1,ISSN 1868\-8969,[Link](http://drops.dagstuhl.de/opus/volltexte/2019/11059),[Document](https://dx.doi.org/10.4230/LIPIcs.ITP.2019.4)Cited by:[Formally verified planning components\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px3.p1.1)\.
- Abdulaziz and Kurz \(2023\)M\. Abdulaziz and F\. KurzFormally verified SAT\-based AI planning\.InProceedings of the Thirty\-Seventh AAAI Conference on Artificial Intelligence \(AAAI 2023\),pp\. 14665–14673\.Cited by:[Formally verified planning components\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px3.p1.1)\.
- Abdulaziz and Lammich \(2018\)M\. Abdulaziz and P\. LammichA formally verified validator for classical planning problems and solutions\.In2018 IEEE 30th International Conference on Tools with Artificial Intelligence \(ICTAI\),pp\. 474–479\.External Links:[Document](https://dx.doi.org/10.1109/ICTAI.2018.00079)Cited by:[Formally verified planning components\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px3.p1.1)\.
- Aggarwalet al\.\(2025\)P\. Aggarwal, B\. Parno, and S\. WelleckAlphaVerus: bootstrapping formally verified code generation through self\-improving translation and treefinement\.InProceedings of the 42nd International Conference on Machine Learning,ICML’25\.Cited by:[Software verification\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px1.p1.1),[Software verification\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px1.p2.1)\.
- Ammanamanchiet al\.\(2026\)P\. S\. Ammanamanchi, S\. Bhat, and S\. BidermanFaults in our formal benchmarking: dataset defects and evaluation failures in lean theorem proving\.External Links:2606\.29493,[Link](https://arxiv.org/abs/2606.29493)Cited by:[Preventing LLM cheating\.](https://arxiv.org/html/2609.27105#Sx4.SSx5.SSS0.Px4.p1.1)\.
- Bhatiaet al\.\(2024\)S\. Bhatia, J\. Qiu, N\. Hasabnis, S\. Seshia, and A\. CheungVerified code transpilation with llms\.InAdvances in Neural Information Processing Systems,A\. Globerson, L\. Mackey, D\. Belgrave, A\. Fan, U\. Paquet, J\. Tomczak, and C\. Zhang \(Eds\.\),Vol\.37,pp\. 41394–41424\.External Links:[Document](https://dx.doi.org/10.52202/079017-1310),[Link](https://proceedings.neurips.cc/paper_files/paper/2024/file/48bb60a0c0aebb4142bf314bd1a5c6a0-Paper-Conference.pdf)Cited by:[Software verification\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px1.p1.1),[Software verification\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px1.p2.1)\.
- Bonetet al\.\(2019a\)B\. Bonet, G\. Francès, and H\. GeffnerLearning features and abstract actions for computing generalized plans\.InProceedings of the Thirty\-Third AAAI Conference on Artificial Intelligence \(AAAI 2019\),pp\. 2703–2710\.Cited by:[Introduction](https://arxiv.org/html/2609.27105#Sx1.p2.1),[Generalized planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px2.p1.1)\.
- Bonetet al\.\(2019b\)B\. Bonet, R\. Fuentetaja, Y\. E\-Martín, and D\. BorrajoGuarantees for sound abstractions for generalized planning\.InProceedings of the 28th International Joint Conference on Artificial Intelligence \(IJCAI 2019\),pp\. 1566–1573\.Cited by:[Introduction](https://arxiv.org/html/2609.27105#Sx1.p4.1),[Completeness of generalized plans\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px3.p1.1)\.
- Bonet and Geffner \(2018\)B\. Bonet and H\. GeffnerFeatures, projections, and representation change for generalized planning\.InProceedings of the 27th International Joint Conference on Artificial Intelligence \(IJCAI 2018\),pp\. 4667–4673\.Cited by:[Introduction](https://arxiv.org/html/2609.27105#Sx1.p2.1),[Generalized planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px2.p1.1)\.
- Bonetet al\.\(2009\)B\. Bonet, H\. Palacios, and H\. GeffnerAutomatic derivation of memoryless policies and finite\-state controllers using classical planners\.InProceedings of the Nineteenth International Conference on Automated Planning and Scheduling \(ICAPS 2009\),pp\. 34–41\.Cited by:[Generalized planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px2.p1.1)\.
- Chenet al\.\(2025\)T\. Chen, S\. Lu, S\. Lu, Y\. Gong, C\. Yang, X\. Li, M\. R\. H\. Misu, H\. Yu, N\. Duan, P\. CHENG, F\. Yang, S\. Lahiri, T\. Xie, and L\. ZhouAutomated proof generation for rust code via self\-evolution\.InInternational Conference on Learning Representations,Y\. Yue, A\. Garg, N\. Peng, F\. Sha, and R\. Yu \(Eds\.\),Vol\.2025,pp\. 71891–71918\.External Links:[Link](https://proceedings.iclr.cc/paper_files/paper/2025/file/b2e20d7402c9985eae4ba924c65370a8-Paper-Conference.pdf)Cited by:[Software verification\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px1.p1.1)\.
- Cuiet al\.\(2023\)Z\. Cui, W\. Kuang, and Y\. LiuAutomatic verification for soundness of bounded qnp abstractions for generalized planning\.\.InProceedings of the 32nd International Joint Conference on Artificial Intelligence \(IJCAI 2023\),pp\. 3149–3157\.Cited by:[Introduction](https://arxiv.org/html/2609.27105#Sx1.p4.1),[Completeness of generalized plans\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px3.p1.1)\.
- de Mouraet al\.\(2015\)L\. de Moura, S\. Kong, J\. Avigad, F\. van Doorn, and J\. von RaumerThe lean theorem prover \(system description\)\.InAutomated Deduction \- CADE\-25,A\. P\. Felty and A\. Middeldorp \(Eds\.\),Cham,pp\. 378–388\.Cited by:[Introduction](https://arxiv.org/html/2609.27105#Sx1.p5.1)\.
- de Moura and Ullrich \(2021\)L\. de Moura and S\. UllrichThe lean 4 theorem prover and programming language\.InAutomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings,Berlin, Heidelberg,pp\. 625–635\.External Links:ISBN 978\-3\-030\-79875\-8,[Link](https://doi.org/10.1007/978-3-030-79876-5_37),[Document](https://dx.doi.org/10.1007/978-3-030-79876-5%5F37)Cited by:[Lean\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px4.p1.1)\.
- Drexleret al\.\(2022\)D\. Drexler, J\. Seipp, and H\. GeffnerLearning sketches for decomposing planning problems into subproblems of bounded width\.InProceedings of the Thirty\-Second International Conference on Automated Planning and Scheduling \(ICAPS 2022\),pp\. 62–70\.Cited by:[Introduction](https://arxiv.org/html/2609.27105#Sx1.p3.1),[Completeness of generalized plans\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px3.p1.1)\.
- Erikssonet al\.\(2017\)S\. Eriksson, G\. Röger, and M\. HelmertUnsolvability certificates for classical planning\.InProceedings of the Twenty\-Seventh International Conference on Automated Planning and Scheduling \(ICAPS 2017\),pp\. 88–97\.Cited by:[Formally verified planning components\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px3.p1.1)\.
- Firstet al\.\(2023\)E\. First, M\. N\. Rabe, T\. Ringer, and Y\. BrunBaldur: whole\-proof generation and repair with large language models\.InProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering,ESEC/FSE 2023,pp\. 1229–1241\.External Links:ISBN 9798400703270Cited by:[LLMs for theorem proving\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px2.p1.1)\.
- Francèset al\.\(2021\)G\. Francès, B\. Bonet, and H\. GeffnerLearning general planning policies from small examples without supervision\.InProceedings of the Thirty\-Fifth AAAI Conference on Artificial Intelligence \(AAAI 2021\),pp\. 11801–11808\.Cited by:[Introduction](https://arxiv.org/html/2609.27105#Sx1.p3.1),[Completeness of generalized plans\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px3.p1.1)\.
- Haslumet al\.\(2019\)P\. Haslum, N\. Lipovetzky, D\. Magazzeni, and C\. MuiseAn introduction to the planning domain definition language\.Synthesis Lectures on Artificial Intelligence and Machine Learning, Vol\.13,Morgan & Claypool Publishers\.Cited by:[PDDL planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px1.p1.1)\.
- Howeyet al\.\(2004\)R\. Howey, D\. Long, and M\. FoxVAL: Automatic plan validation, continuous effects and mixed initiative planning using PDDL\.InProceedings of the 16th International Conference on Tools with Artificial Intelligence \(ICTAI 2004\),pp\. 294–301\.Cited by:[Generating the generalized plan in Lean](https://arxiv.org/html/2609.27105#Sx4.SSx5.SSS0.Px2.p1.1)\.
- Hu and Levesque \(2010\)Y\. Hu and H\. J\. LevesqueA correctness result for reasoning about one\-dimensional planning problems\.InProceedings of the Twelfth International Conference on Principles of Knowledge Representation and Reasoning \(KR 2010\),pp\. 362–371\.Cited by:[Introduction](https://arxiv.org/html/2609.27105#Sx1.p4.1),[Completeness of generalized plans\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px3.p1.1)\.
- Jiménezet al\.\(2019\)S\. Jiménez, J\. Segovia\-Aguas, and A\. JonssonA review of generalized planning\.The Knowledge Engineering Review34,pp\. e5\.Cited by:[Introduction](https://arxiv.org/html/2609.27105#Sx1.p2.1),[Generalized planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px2.p1.1)\.
- McDermott \(2000\)D\. M\. McDermottThe 1998 ai planning systems competition\.AI magazine21\(2\),pp\. 35–55\.Cited by:[PDDL planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px1.p1.1)\.
- Mugdanet al\.\(2023\)E\. Mugdan, R\. Christen, and S\. ErikssonOptimality certificates for classical planning\.InProceedings of the Thirty\-Third International Conference on Automated Planning and Scheduling \(ICAPS 2023\),pp\. 286–294\.Cited by:[Formally verified planning components\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px3.p1.1)\.
- Ospanovet al\.\(2025\)A\. Ospanov, F\. Farnia, and R\. YousefzadehAPOLLO: automated LLM and lean collaboration for advanced formal reasoning\.InThe Thirty\-ninth Annual Conference on Neural Information Processing Systems,External Links:[Link](https://openreview.net/forum?id=fxDCgOruk0)Cited by:[Generating the completeness proof\.](https://arxiv.org/html/2609.27105#Sx4.SSx5.SSS0.Px3.p3.1),[LLMs for theorem proving\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px2.p1.1)\.
- Paglieriet al\.\(2026\)D\. Paglieri, L\. Cross, T\. Genewein, J\. Z\. Leibo, N\. Tomasev, and A\. S\. VezhnevetsA case study on emergent cheating and whistleblowing in autonomous research swarms\.External Links:2609\.04170,[Link](https://arxiv.org/abs/2609.04170)Cited by:[Preventing LLM cheating\.](https://arxiv.org/html/2609.27105#Sx4.SSx5.SSS0.Px4.p1.1)\.
- Pfenning and Paulin\-Mohring \(1990\)F\. Pfenning and C\. Paulin\-MohringInductively defined types in the calculus of constructions\.InMathematical Foundations of Programming Semantics,M\. Main, A\. Melton, M\. Mislove, and D\. Schmidt \(Eds\.\),New York, NY,pp\. 209–228\.External Links:ISBN 978\-0\-387\-34808\-7Cited by:[Validity Constraints](https://arxiv.org/html/2609.27105#Sx3.SSx5.p3.1)\.
- Seippet al\.\(2022\)J\. Seipp, Á\. Torralba, and J\. HoffmannPDDL generators\.Zenodo\.Note:https://doi\.org/10\.5281/zenodo\.6382173Cited by:[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.10.3),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.11.3),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.14.3),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.9.3)\.
- Silveret al\.\(2024\)T\. Silver, S\. Dan, K\. Srinivas, J\. Tenenbaum, L\. Pack Kaelbling, and M\. KatzGeneralized planning in pddl domains with pretrained large language models\.InProceedings of the Thirty\-Eighth AAAI Conference on Artificial Intelligence \(AAAI 2024\),J\. Dy and S\. Natarajan \(Eds\.\),pp\. 20256–20264\.Cited by:[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.2.2),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.4.2),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.5.2),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.6.2),[Introduction](https://arxiv.org/html/2609.27105#Sx1.p2.1),[Introduction](https://arxiv.org/html/2609.27105#Sx1.p6.1),[Generalized planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px2.p2.1)\.
- Solar\-Lezamaet al\.\(2006\)A\. Solar\-Lezama, L\. Tancau, R\. Bodik, S\. Seshia, and V\. SaraswatCombinatorial sketching for finite programs\.InProceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems,ASPLOS XII,New York, NY, USA,pp\. 404–415\.External Links:ISBN 1595934510,[Link](https://doi.org/10.1145/1168857.1168907),[Document](https://dx.doi.org/10.1145/1168857.1168907)Cited by:[Software verification\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px1.p1.1)\.
- Songet al\.\(2024\)P\. Song, K\. Yang, and A\. AnandkumarTowards large language models as copilots for theorem proving in lean\.CoRRabs/2404\.12534\.External Links:[Link](https://doi.org/10.48550/arXiv.2404.12534)Cited by:[LLMs for theorem proving\.](https://arxiv.org/html/2609.27105#Sx6.SSx2.SSS0.Px2.p1.1)\.
- Srivastavaet al\.\(2011a\)S\. Srivastava, N\. Immerman, and S\. ZilbersteinA new representation and associated algorithms for generalized planning\.Artificial Intelligence175\(2\),pp\. 615–647\.Cited by:[Introduction](https://arxiv.org/html/2609.27105#Sx1.p2.1),[Introduction](https://arxiv.org/html/2609.27105#Sx1.p4.1),[Generalized planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px2.p1.1),[Completeness of generalized plans\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px3.p1.1)\.
- Srivastavaet al\.\(2011b\)S\. Srivastava, S\. Zilberstein, N\. Immerman, and H\. GeffnerQualitative numeric planning\.InProceedings of the Twenty\-Fifth AAAI Conference on Artificial Intelligence \(AAAI 2011\),pp\. 1010–1016\.Cited by:[Generalized planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px2.p1.1)\.
- Ståhlberget al\.\(2022\)S\. Ståhlberg, B\. Bonet, and H\. GeffnerLearning general optimal policies with graph neural networks: expressive power, transparency, and limits\.InProceedings of the International Conference on Automated Planning and Scheduling,Vol\.32,pp\. 629–637\.Cited by:[Generalized planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px2.p2.1)\.
- Ståhlberget al\.\(2025\)S\. Ståhlberg, B\. Bonet, and H\. GeffnerLearning more expressive general policies for classical planning domains\.InProceedings of the Thirty\-Ninth AAAI Conference on Artificial Intelligence \(AAAI 2025\),pp\. 26697–26706\.Cited by:[Generalized planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px2.p2.1)\.
- Steinet al\.\(2026\)K\. Stein, N\. Hodel, D\. Fišer, J\. Hoffmann, M\. Katz, and A\. KollerImproved generalized planning with llms through strategy refinement and reflection\.InProceedings of the International Conference on Automated Planning and Scheduling,Vol\.36,pp\. 677–686\.Cited by:[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.10.2),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.11.2),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.14.2),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.9.2),[Introduction](https://arxiv.org/html/2609.27105#Sx1.p2.1),[Introduction](https://arxiv.org/html/2609.27105#Sx1.p3.1),[Introduction](https://arxiv.org/html/2609.27105#Sx1.p6.1),[Introduction](https://arxiv.org/html/2609.27105#Sx1.p7.1),[Generalized planning\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px2.p2.1),[Completeness of generalized plans\.](https://arxiv.org/html/2609.27105#Sx2.SS0.SSS0.Px3.p1.1),[Generating the generalized plan in Lean](https://arxiv.org/html/2609.27105#Sx4.SSx5.SSS0.Px2.p1.1),[Pipeline and Set\-up](https://arxiv.org/html/2609.27105#Sx5.SSx1.p1.1),[footnote 6](https://arxiv.org/html/2609.27105#footnote6)\.
- Taitleret al\.\(2024\)A\. Taitler, R\. Alford, J\. Espasa, G\. Behnke, D\. Fišer, M\. Gimelfarb, F\. Pommerening, S\. Sanner, E\. Scala, D\. Schreiber, J\. Segovia\-Aguas, and J\. SeippThe 2023 International Planning Competition\.AI Magazine45\(2\),pp\. 280–296\.External Links:[Document](https://dx.doi.org/10.1002/aaai.12169)Cited by:[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.12.2),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.13.2),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.3.2),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.7.2),[Table 3](https://arxiv.org/html/2609.27105#A1.T3.1.8.2),[Introduction](https://arxiv.org/html/2609.27105#Sx1.p1.1),[Results proofs\.](https://arxiv.org/html/2609.27105#Sx5.SSx2.SSS0.Px2.p4.1)\.
- Wanget al\.\(2026\)J\. Wang, J\. Zhang, Q\. Guo, L\. Guo, R\. Li, C\. Zhang, C\. Peng, C\. Wang, D\. Zhao, J\. Shi, J\. Wang, L\. Feng, M\. Shen, Q\. Li, S\. An, S\. Wang, W\. Shi, X\. Xi, X\. Li, X\. Cao, Y\. Lu, Y\. Zhao, Z\. Chen, Z\. Lin, W\. Wang, P\. Pei, and X\. CaiLongCat\-flash\-prover: advancing native formal reasoning via agentic tool\-integrated reinforcement learning\.External Links:2603\.21065,[Link](https://arxiv.org/abs/2603.21065)Cited by:[Preventing LLM cheating\.](https://arxiv.org/html/2609.27105#Sx4.SSx5.SSS0.Px4.p1.1)\.

## Appendix ADatasets

Table[3](https://arxiv.org/html/2609.27105#A1.T3)lists the datasets from which the debugging problem instances, as well as the instance generators based on which the validity constraint specifications were created\.

Table 3:The origin of the debugging tasks that we used for our experiments and the instance generators based on which we created the validity constraints\.
## Appendix BAdditional Representation Examples

Figure[5](https://arxiv.org/html/2609.27105#A2.F5)shows a side\-by\-side example of a PDDL problem instance with two spanners, two nuts and four locations \(including shed and gate\) \(left part\) and the corresponding Lean problem instance \(right part\)\.

Listing[12](https://arxiv.org/html/2609.27105#listing12)shows examples of the additional, domain\-specific lemmas about how states change \(and do not change\) that are generated symbolically based on the PDDL and provided as helper lemmas to the LLM\. Listing[13](https://arxiv.org/html/2609.27105#listing13)shows additional symbolically generated lemmas that the LLM is provided for an domain\.

\(define\(problemprob0\)

\(:domainspanner\)

\(:objects

bob\-man

spanner1\-spanner

spanner2\-spanner

nut1\-nut

nut2\-nut

loc1\-location

loc2\-location

shed\-location

gate\-location

\)

\(:init

\(atbobshed\)

\(atspanner1loc2\)

\(useablespanner1\)

\(atspanner2loc1\)

\(useablespanner2\)

\(loosenut1\)

\(atnut1gate\)

\(loosenut2\)

\(atnut2gate\)

\(linkshedloc1\)

\(linkloc1loc2\)

\(linkloc2gate\)

\)

\(:goal

\(and

\(tightenednut1\)

\(tightenednut2\)

\)

\)

\)

defproblemStatics:StaticState:=

\{

objects:=\[0,1,2,3,4,5,6,7,8\]

link\_p:=funx0x1=\>\(x0==5&&x1==6\)\|\|\(x0==6&&x1==8\)\|\|\(x0==7&&x1==5\),

location\_t:=funx0=\>\(x0==5\)\|\|\(x0==6\)\|\|\(x0==7\)\|\|\(x0==8\),

locatable\_t:=funx0=\>\(x0==0\)\|\|\(x0==1\)\|\|\(x0==2\)\|\|\(x0==3\)\|\|\(x0==4\),

man\_t:=funx0=\>\(x0==0\),

nut\_t:=funx0=\>\(x0==3\)\|\|\(x0==4\),

spanner\_t:=funx0=\>\(x0==1\)\|\|\(x0==2\)

\}

defproblemDynamic:DynamicState:=

\{

at\_p:=funx0x1=\>\(x0==0&&x1==7\)\|\|\(x0==1&&x1==6\)\|\|\(x0==2&&x1==5\)\|\|\(x0==3&&x1==8\)\|\|\(x0==4&&x1==8\),

carrying\_p:=funx0x1=\>false,

useable\_p:=funx0=\>\(x0==1\)\|\|\(x0==2\),

tightened\_p:=funx0=\>false,

loose\_p:=funx0=\>\(x0==3\)\|\|\(x0==4\)

\}

defgoalDynamic:GoalDynamic:=

\{

at\_p:=funx0x1=\>none,

carrying\_p:=funx0x1=\>none,

useable\_p:=funx0=\>none,

tightened\_p:=funx0=\>ifx0==3thensometrueelseifx0==4thensometrueelsenone,

loose\_p:=funx0=\>none

\}\}

Figure 5:Example of a PDDL definition of a problem instance from the Spanner domain \(left\) and the corresponding, converted Lean problem instance \(right\)\.lemmawalk\_statics\(var\_startvar\_endvar\_m:Obj\)\(s:State\):

\(walkvar\_startvar\_endvar\_ms\)\.statics=s\.statics:=rfl

lemmawalk\_at\_p\_eq1\(var\_startvar\_endvar\_m:Obj\)\(s:State\):

\(walkvar\_startvar\_endvar\_ms\)\.dynamic\.at\_pvar\_mvar\_end=true:=by

unfoldwalk

simp

lemmawalk\_at\_p\_ne\_var\_l\(var\_startvar\_endvar\_m:Obj\)\(s:State\)\{var\_end’:Obj\}\(h1:var\_end’≠\\neqvar\_end\)\(h2:var\_end’≠\\neqvar\_start\):

\(walkvar\_startvar\_endvar\_ms\)\.dynamic\.at\_pvar\_mvar\_end’=s\.dynamic\.at\_pvar\_mvar\_end’:=by

unfoldwalk

simp\[h1,h2\]

lemmawalk\_carrying\_p\(var\_startvar\_endvar\_m:Obj\)\(s:State\):

\(walkvar\_startvar\_endvar\_ms\)\.dynamic\.carrying\_p=s\.dynamic\.carrying\_p:=rfl

lemmarunPlan\_statics\(plan:ListPlanAction\)\(s:State\):

\(runPlanplans\)\.statics=s\.statics:=by

inductionplangeneralizingswith

\|nil=\>simp\[runPlan\]

\|consaasih=\>

simponly\[runPlan\]

rw\[ih\]

casesawith

\|walkvar\_svar\_evar\_m=\>exactwalk\_staticsvar\_svar\_endvar\_ms

\|pickup\_spannervar\_lvar\_svar\_m=\>exactpickup\_spanner\_staticsvar\_lvar\_svar\_ms

\|tighten\_nutvar\_lvar\_svar\_mvar\_n=\>exacttighten\_nut\_staticsvar\_lvar\_svar\_mvar\_ns

lemmaaction\_preserves\_wf

\{a:PlanAction\}

\{s:State\}

\(hwf:WellFormeds\)

\(hpre:actionPreas\):

WellFormed\(actionApplyas\):=by

casesawith

\|walkvar\_startvar\_endvar\_m=\>

exactwalk\_preserves\_wfvar\_startvar\_endvar\_mshwfhpre

\|pickup\_spannervar\_lvar\_svar\_m=\>

exactpickup\_spanner\_preserves\_wfvar\_lvar\_svar\_mshwfhpre

\|tighten\_nutvar\_lvar\_svar\_mvar\_n=\>

exacttighten\_nut\_preserves\_wfvar\_lvar\_svar\_mvar\_nshwfhpre

Listing 12Examples of the additional, symbolically generated, lemmas provided the LLM for generating the completeness proof for the Spanner domain\.lemmavalidPlan\_preserves\_wf

\{plan:ListPlanAction\}

\{s:State\}

\(hplan:ValidPlanplans\)

\(hwf:WellFormeds\):

WellFormed\(runPlanplans\):=by

inductionplangeneralizingswith

\|nil=\>

simpa\[runPlan\]

\|consaasih=\>

simponly\[ValidPlan\]athplan

rcaseshplanwith⟨\\langleha,has⟩\\rangle

havehwf’:=

action\_preserves\_wf\(s:=s\)hwfha

exactihhashwf’

lemmarunPlan\_append\(asbs:ListPlanAction\)\(s:State\):

runPlan\(as\+\+bs\)s=runPlanbs\(runPlanass\):=by

inductionasgeneralizingswith

\|nil=\>simp\[runPlan\]

\|consaasih=\>simp\[runPlan,ih\]

lemmavalidPlan\_append\(asbs:ListPlanAction\)\(s:State\):

ValidPlan\(as\+\+bs\)s↔\\leftrightarrowValidPlanass∧\\wedgeValidPlanbs\(runPlanass\):=by

inductionasgeneralizingswith

\|nil=\>simp\[ValidPlan,runPlan\]

\|consaasih=\>simp\[ValidPlan,runPlan,ih,and\_assoc\]

Listing 13The additional, symbolically generated, lemmas provided the LLM for generating the completeness proof for any domain\.1structureGPBuildwhere

2actions:ListPlanAction

3state:State

4location:Obj

5

6defgpFindMan\(s:State\):Obj:=

7matchs\.statics\.objects\.find?\(funo=\>s\.statics\.man\_to\)with

8\|somem=\>m

9\|none=\>0

10

11defgpFindManLocation\(s:State\)\(m:Obj\):Obj:=

12matchs\.statics\.objects\.find?\(funl=\>

13s\.statics\.location\_tl&&s\.dynamic\.at\_pml\)with

14\|somel=\>l

15\|none=\>0

16

17defgpFindNextLocation\(s:State\)\(l:Obj\):OptionObj:=

18s\.statics\.objects\.find?\(funnext=\>

19s\.statics\.link\_plnext\)

20

21defgpFindCarriedUseableSpanner\(s:State\)\(m:Obj\):OptionObj:=

22s\.statics\.objects\.find?\(funsp=\>

23s\.statics\.spanner\_tsp&&

24s\.dynamic\.carrying\_pmsp&&

25s\.dynamic\.useable\_psp\)

26

27defgpCollectAt:ListObj→\\rightarrowObj→\\rightarrowObj→\\rightarrowState→\\rightarrowGPBuild

28\|\[\],l,\_,s=\>

29\{

30actions:=\[\]

31state:=s

32location:=l

33\}

34\|sp::rest,l,m,s=\>

35ifs\.statics\.spanner\_tsp=true∧\\wedge

36s\.dynamic\.at\_pspl=true∧\\wedge

37s\.dynamic\.useable\_psp=truethen

38leta:=PlanAction\.pickup\_spannerlspm

39lets’:=actionApplyas

40letresult:=gpCollectAtrestlms’

41\{

42actions:=a::result\.actions

43state:=result\.state

44location:=l

45\}

46else

47gpCollectAtrestlms

48

49defgpTraverse:Nat→\\rightarrowObj→\\rightarrowObj→\\rightarrowState→\\rightarrowGPBuild

50\|0,l,m,s=\>

51gpCollectAts\.statics\.objectslms

52\|Nat\.succfuel,l,m,s=\>

53letcollected:=gpCollectAts\.statics\.objectslms

54matchgpFindNextLocationcollected\.statelwith

55\|none=\>

56collected

57\|somenext=\>

58leta:=PlanAction\.walklnextm

59lets’:=actionApplyacollected\.state

60letresult:=gpTraversefuelnextms’

61\{

62actions:=collected\.actions\+\+\(a::result\.actions\)

63state:=result\.state

64location:=result\.location

65\}

66

67defgpTightenAll:ListObj→\\rightarrowObj→\\rightarrowObj→\\rightarrowState→\\rightarrowGPBuild

68\|\[\],l,\_,s=\>

69\{

70actions:=\[\]

71state:=s

72location:=l

73\}

74\|n::rest,l,m,s=\>

75ifs\.statics\.nut\_tn=true∧\\wedge

76s\.dynamic\.loose\_pn=truethen

77matchgpFindCarriedUseableSpannersmwith

78\|none=\>

79gpTightenAllrestlms

80\|somesp=\>

81leta:=PlanAction\.tighten\_nutlspmn

82lets’:=actionApplyas

83letresult:=gpTightenAllrestlms’

84\{

85actions:=a::result\.actions

86state:=result\.state

87location:=l

88\}

89else

90gpTightenAllrestlms

91

92defsolve\(s:State\)\(g:Goal\):ListPlanAction:=

93letm:=gpFindMans

94letstart:=gpFindManLocationsm

95lettraversed:=

96gpTraverses\.statics\.objects\.lengthstartms

97lettightened:=

98gpTightenAlls\.statics\.objectstraversed\.locationmtraversed\.state

99traversed\.actions\+\+tightened\.actions

Listing 14:Example of an LLM\-generated generalized plan for the Spanner domain, consisting of the mainsolvefunction and helper declarations\.