Language Models as Higher-Order Planning Formalizers
Recent work provides overwhelming evidence that LLMs, even those trained to scale their reasoning trace, quickly deteriorate at planning as problems become more complex. LLM-as-Formalizers aim to address this by employing LLMs as a bridge to translate natural language descriptions into structured planning representations such as PDDL, which are then fed to a programmatic solver. We observe that its success may be overstated because planning problem descriptions in standard benchmarks often have a one-to-one mapping to PDDL, which departs from real use cases. To address this, we introduce the notion of unraveling problems where a natural yet succinct description translates into a very large PDDL representation. Using unraveling variants of four standard planning domains, we demonstrate that LLM Formalizers also do not always scale. We tackle this challenge by introducing a new paradigm, LLM-as-Higher-Order-Formalizer, where the LLM generates a high-level program that captures the recurrent logic within the description and in turn generates the larger PDDL representation. This decouples token output from the combinatorial explosion of the underlying formalization and search space, leading to improved performance for complex problems.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Language Model as Planner and Formalizer under Constraints
LLMs have been widely used in planning, either as planners to generate action sequences end-to-end, or as formalizers to represent the planning domain and problem in a formal language that can derive plans deterministica…
On the Limit of Language Models as Planning Formalizers
Large Language Models have been shown to fail to create executable and verifiable plans in grounded environments. An emerging line of work shows success in using LLM as a formalizer to generate a formal representation (e…
Characterizing Paraphrase-Induced Failures in Lean 4 Autoformalization
Lean 4 autoformalization has become increasingly popular in recent years, with frontier language models and open-weight autoformalizers now producing valid formalizations of mathematical theorems. However, these evaluati…
Dynamic Term-Modal Logics for First-Order Epistemic Planning
Many classical planning frameworks are built on first-order languages. The first-order expressive power is desirable for compactly representing actions via schemas, and for specifying quantified conditions such as $\neg\…
Order-Planning Neural Text Generation From Structured Data
Generating texts from structured data (e.g., a table) is important for various natural language processing tasks such as question answering and dialog systems. In recent studies, researchers use neural language models an…
DecoderQuestion AnsweringTable-to-Text GenerationText Generation