The authors developed a semantics-preserving conversion from PDDL, a standard planning-domain language, into Lean.
LLMs generate generalized plans with machine-checked completeness proofs
The system produced Lean-verified plans for 12 of 13 benchmark domains, proving they solve every instance covered by the supplied domain constraints.
Research Lab
Katharina Stein · Chaahat Jain · Jörg Hoffmann · Alexander Koller
Saarland University · German Research Center for Artificial Intelligence (DFKI)
Research Digest··2 min read
Stein et al.
Why this paper
From German Research Center for Artificial Intelligence (DFKI) and Saarland University
In one line
LLMs can generate generalized plans and formal proofs that the plans solve all domain instances.
What we could check
- ·No code link found
- ·No weights link found
- ·No dataset link found
- ·No compute details found
- ✓Limitations stated by the authors
- ·No benchmark numbers found
Observed from the paper text and links we have. Absence here means we did not find it, not that it does not exist.
§