Language Model Planners do not Scale, but do Formalizers?

TL;DR

While LLM planners struggle with complex problems, LLM formalizers significantly outperform them, especially with divide-and-conquer strategies and higher-order formalization to handle exponential complexity.

Contribution

The paper demonstrates that LLM formalizers outperform planners in complex domains, introduces a divide-and-conquer formalization technique, and proposes a new paradigm using higher-order formalizers to manage exponential problem complexity.

Findings

LLM formalizers retain perfect accuracy in BlocksWorld with large state spaces.

Divide-and-conquer formalization improves robustness against problem complexity.

Higher-order formalizers effectively handle exponential formalization challenges.

Abstract

Recent work shows overwhelming evidence that LLMs, even those trained to scale their reasoning trace, perform unsatisfactorily when solving planning problems too complex. Whether the same conclusion holds for LLM formalizers that generate solver-oriented programs remains unknown. We systematically show that LLM formalizers greatly out-scale LLM planners, some retaining perfect accuracy in the classic BlocksWorld domain with a huge state space of size up to $10^{165}$. While performance of smaller LLM formalizers degrades with problem complexity, we show that a divide-and-conquer formalizing technique can greatly improve its robustness. Finally, we introduce unraveling problems where one line of problem description realistically corresponds to exponentially many lines of formal language such as the Planning Domain Definition Language (PDDL), greatly challenging LLM formalizers. We tackle this challenge by introducing a new paradigm, namely LLM-as-higher-order-formalizer, where an LLM generates a program generator. This decouples token output from the combinatorial explosion of the underlying formalization and search space.