Planning anything with rigor: general-purpose zero-shot planning with llm-based formalized programming

This document introduces LLMFP, a framework for using Large Language Models (LLMs) to solve complex planning tasks by converting them into optimization problems solvable by formal planners like SMT solvers. It details the five-step process of LLMFP, which involves LLMs defining the problem, formulating variables, generating code, formatting results, and performing self-assessment and modification. The paper presents experimental results across nine diverse planning problems, demonstrating LLMFP's superior performance and zero-shot generalization capability compared to existing LLM-based approaches, highlighting its robustness to task variations and the effectiveness of its individual components. While acknowledging limitations in handling ambiguous descriptions and extremely large problem spaces, the authors propose LLMFP as a promising general-purpose framework for rigorous planning with LLMs.