{"id":"6f113d31-11c2-4eb3-ae82-9822538f4f2a","arxiv_id":"2412.09879","paper_version":4,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"On simple planning domains, state-of-the-art LLMs can generate complete, solvable PDDL that often outperforms direct plan generation, but natural-language descriptions and complex domains sharply reduce accuracy.","lead":"Large language models were asked to translate descriptions of simple planning games into PDDL, a formal language for planners. The best models often wrote correct formalizations and beat models that tried to plan directly, but performance fell when descriptions sounded more natural.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The formalizer-vs-planner comparison uses only a zero-shot, unverified planner baseline; a validated LLM-Modulo planner could close the gap, so the comparative conclusion needs that control.","rationale":"The reader's weakest_assumption identifies exactly the same load-bearing concern: the superiority claim is evaluated against a minimal zero-shot planner without a validation loop, and the paper itself acknowledges that a stronger baseline is likely. I agree that this is the most important gap because the paper's central contribution is comparative—'formalizing is often superior to planning'—not merely a demonstration that strong models can emit PDDL. If a validated planner baseline closes the gap, the practical recommendation changes from 'use formalization' to 'use any method with a verification loop.' The concern is not fatal: the paper's abstract carefully says 'those directly generating plans,' and its Limitation is honest. But the missing control means the comparative claim is currently under-supported, which justifies the reader's CONDITIONAL verdict. I do not see a different, more severe internal inconsistency. The abstract's overstatement about 'most large enough models' is real but secondary, and the lexical-robustness claim is already weakened by the authors' own data; neither changes the verdict. My concrete test is deliberately minimal: it reuses the paper's own VAL-based correctness metric and tests only whether adding cheap validation to the planner baseline removes the formalizer's advantage. If the test is run and the advantage persists, the central claim is substantially stronger.","tokens_in":22967,"tokens_out":5914,"duration_ms":70269,"concrete_test":"Implement an LLM-Modulo planner baseline on Heavily Templated and Natural BlocksWorld-100: for each of the 100 problems, let gpt-4o and o3-mini each sample up to 10 candidate plans, validate every candidate with VAL against the ground-truth domain and problem files, and return the first valid plan. Compare correctness rates to the formalizer columns in Table 2 (gpt-4o: 89/100 and 60/100; o3-mini: 94/100 and 68/100). If the validated planner reaches or exceeds these numbers, the paper's comparative conclusion would need substantial qualification.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central comparative claim—that LLM-as-formalizer often outperforms LLM-as-planner—is measured against a deliberately minimal planner baseline: zero-shot, single attempt, no external validation (Section 3; prompts in Appendix B). The paper's own Limitation section concedes that an LLM-Modulo-style planner with symbolic validation 'will likely lead to a stronger baseline.' This is load-bearing because the formalizer pipeline effectively includes a deterministic validation/solver loop, while the planner baseline gets none. The observed advantage could therefore reflect the presence of a verification step rather than the value of formalization as such. The comparison is also already model- and task-dependent: on Barman-100, o3-mini as planner achieves 19/100 while its formalizer correctness is 0/100, and on Heavily Templated BlocksWorld-100, o3-mini as planner (96/100) slightly exceeds its formalizer correctness (94/100). Without testing a planner that can generate multiple candidates and validate them, the headline 'formalizing is often superior' remains an unresolved comparison against a weak strawman. The paper is transparent about this limitation, but the empirical gap it creates is not closed.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper evaluates whether LLMs can be used as 'formalizers' that translate natural-language descriptions of planning environments into complete PDDL domain and problem files, which are then solved by a deterministic planner. The authors construct four IPC-style benchmarks (BlocksWorld, Mystery BlocksWorld, Logistics, Barman) with three levels of description naturalness (Heavily Templated, Moderately Templated, Natural), and compare LLM-as-formalizer against a zero-shot LLM-as-planner baseline across several open and closed models. The main claims are that (i) sufficiently large closed models can generate solvable and correct PDDL, (ii) formalizing often outperforms direct plan generation, (iii) more natural descriptions decrease performance, and (iv) the formalizer approach is robust to lexical perturbations. The paper also provides a manual error analysis of syntax and semantic errors. The empirical results are grounded in VAL-validated plans and the code/data are released, but the headline comparison rests on a deliberately weak planner baseline and on single-run measurements without confidence intervals.","tokens_in":23081,"tokens_out":5075,"duration_ms":54206,"significance":"If the results hold, the paper is a useful systematic contribution to the emergent LLM-as-formalizer paradigm. Its strengths are that it moves beyond partial PDDL generation to whole domain and problem files, introduces and validates a naturalness continuum for descriptions, uses deterministic VAL-based correctness checking rather than only string/plan matching, and includes a detailed error taxonomy with hand-annotated examples. The finding that natural descriptions degrade formalization quality, and that models exhibit different error profiles, is actionable for future work. The public release of code and data supports reproducibility. However, the comparative superiority claim is not yet fully established because the planner baseline is minimal and the error analysis is based on small samples; the abstract's generalization to 'most large enough models' overstates what the data show.","major_comments":[{"comment":"The central comparative claim—that LLM-as-formalizer often outperforms LLM-as-planner—is measured against a zero-shot, single-attempt planner baseline that receives no validation or correction loop. The formalizer pipeline, in contrast, benefits from a deterministic planner and, in principle, the ability to detect unsolvable PDDL. The paper's own Limitation section concedes that a Kambhampati et al. (2024) style LLM-Modulo baseline, which adds symbolic validation to the planner, would 'likely lead to a stronger baseline.' This is load-bearing: the observed advantage could reflect the presence of an external solver/validator rather than the value of formalization as such. The authors should either add such a validated-planner control (e.g., allowing the planner to propose multiple candidates and checking them with VAL) or substantially soften the 'formalizing is often superior' conclusion to 'formalizing is superior to unverified zero-shot plan generation.'","section":"Section 3 and Section 8, Tables 2–5"},{"comment":"All results are reported from a single run per model/dataset combination, with no confidence intervals, seeds, or repeated sampling. This makes small differences unreliable; for example, on Heavily Templated BlocksWorld-100, o3-mini as planner achieves 96/100 while its formalizer correctness is 94/100, and on Barman-100, several planner scores exceed formalizer scores (e.g., DeepSeek-R1 planner 22 vs. formalizer 2). The paper's conclusion that formalizing is 'often' superior is based on point estimates that could change with reruns. At minimum, the authors should state that measurements are single-run and provide, for a few representative conditions, repeated-run estimates or bootstrap intervals to quantify variance.","section":"Section 5 and Tables 2–5"},{"comment":"The abstract states that 'most large enough models can effectively formalize descriptions as PDDL, outperforming those directly generating plans.' The data in Tables 2–4 show that this holds only for a few closed models (gpt-4o, o3-mini, DeepSeek-R1, and partially gpt-4o-mini). Llama-3.1-405B and all DeepSeek-R1-Distill variants achieve zero solvability on BlocksWorld and Logistics, and Gemma models are highly variable (near-perfect on Mystery BlocksWorld but poor on BlocksWorld-100). The generalization 'most large enough models' is not supported. The authors should restrict the claim to the specific models that performed well, or rephrase to 'some large closed models.'","section":"Abstract and Section 5.1"},{"comment":"The paper repeatedly describes the task as generating 'the complete representation' or 'entire PDDL,' but footnote 2 states that 'it is minimally necessary to provide the action space, the identifiers and parameters of the actions in DF.' The model therefore receives the action schemas (names and parameter lists) and only needs to fill in preconditions/effects and the problem file. This is a meaningful reduction of the formalization burden and should be stated clearly in the abstract and main text, not only in a footnote. The claim of 'complete representation' is accurate with respect to the full DF/PF content, but readers may infer that the model invents action names and parameters from scratch, which is not the case.","section":"Section 4.1 and footnote 2"},{"comment":"The Natural descriptions were generated with gpt-4o assistance and then gpt-4o is later evaluated on those descriptions. Although the authors manually verified correctness and naturalness, this creates a potential confound: gpt-4o may perform better on its own paraphrases than on independently written natural text, which could inflate the gpt-4o results and the naturalness-degradation finding. The authors should add a control using human-authored natural descriptions (or descriptions generated by a different model) for at least one dataset, or explicitly discuss why this confound is unlikely to affect the main conclusions.","section":"Section 4.1 (Natural dataset generation)"}],"minor_comments":[{"comment":"The paper claims zero-shot prompting, but the planner prompts in Listings 13–16 include a concrete example plan in the instruction ('Here is what the output should look like: (PICK-UP A)...'). This is a form of one-shot formatting example. The authors should clarify whether the formalizer prompts also contain such examples, and discuss whether the example output influenced behaviors such as the DeepSeek-R1 pattern matching noted in Section 5.6.","section":"Appendix B"},{"comment":"The error analysis is based on a random sample of only 20 errors per model/dataset, which is small for drawing conclusions about common error types. The counts are presented as deterministic values without noting sampling uncertainty; a sentence acknowledging the small sample size and the lack of inter-annotator agreement (if only one annotator) would be appropriate.","section":"Section 5.5 and Tables 8–9"},{"comment":"Barman-100 results are relegated to the appendix (Figure 7) with only a sentence in Section 5.1; since Barman is the most complex domain and shows a reverse trend (planner outperforming formalizer for several models), it deserves at least a brief discussion in the main text rather than a dismissal as 'close-to-zero performance for all models.'","section":"Figure 3 and Figure 7"},{"comment":"There are a few typographical and formatting issues: 'Mystery BlocksWorld' is sometimes written as 'MysteryBlocksWorld' (e.g., Tables 3, 8); the text in Figure 1 is not fully legible; and Table 1's 'This work' row could be more explicit that the action-space prompt is given. These do not affect the scientific content.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The paper is a solid empirical contribution that fits the scope of cs.CL, and the authors are transparent about their limitations. My main concern is that the headline 'formalizer often outperforms planner' comparison is against a strawman baseline; adding an LLM-Modulo-style validated-planner control would either strengthen or substantially qualify the claim. The single-run reporting and the gpt-4o-assisted dataset are secondary but should be addressed. No concerns about scientific integrity; the code/data release is a positive feature."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This is a genuinely useful benchmark paper. It's the first to test LLMs on generating the complete PDDL domain and problem files, not just fragments, across three naturalness levels, with 100 problems per domain and VAL-validated plans. The natural descriptions were human-verified, and the error analysis—syntax vs semantic, DF vs PF, fine-grained action errors—is a real addition. Code and data are public.\n\nThe soft spots are about the comparative claim. The planner baseline is zero-shot, single-attempt, with no verification loop, while the formalizer gets a deterministic solver. The authors admit that a Kambhampati-style LLM-Modulo planner 'will likely lead to a stronger baseline.' That means the headline 'formalization often outperforms direct planning' is really 'formalization plus solver beats raw zero-shot generation.' The direction already flips: on Barman, o3-mini as planner gets 19/100 while its formalizer correctness is 0/100; on Heavily Templated BlocksWorld, o3-mini planner (96) edges out formalizer (94). So the comparative conclusion is not load-bearing; it's an open question.\n\nAlso, the abstract overstates. 'Most large enough models can effectively formalize' is only true for the strongest closed models; almost all open models fail. And the claim that Llama-405B cannot generate solvable PDDL appears without a reported run in any table. 'Robust to lexical perturbation' is a stretch: gpt-4o drops from 89 correct on Heavily Templated BlocksWorld to 70 on Mystery BlocksWorld. No repeated runs, so no confidence intervals, but that is a minor point for this kind of study.\n\nNone of this kills the paper. The benchmark and the absolute capability numbers stand, and the authors are transparent about most of these limitations. The paper deserves a serious referee: the dataset is worth having, and the overclaims are fixable with a validated planner baseline and more careful wording.\n\nRecommendation: send to review.","headline":"Useful full-PDDL benchmark, but the formalizer-vs-planner comparison runs against a weak zero-shot baseline, so the headline advantage is overstated.","tokens_in":23695,"tokens_out":3681,"would_cite":true,"duration_ms":36620,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Language models solve more planning problems by writing PDDL than by planning","keywords":["LLM-as-formalizer","PDDL generation","classical planning","natural language descriptions","BlocksWorld","Mystery BlocksWorld","LLM-as-planner","neuro-symbolic planning"],"falsifier":"Run the same 100 BlocksWorld problems with a planner loop that lets gpt-4o propose a plan, checks it with VAL, returns the error message, and lets the model revise for a few rounds; if that loop reaches or exceeds the formalizer's 60/100 correctness, the paper's claim that formalization is the better methodology would be undercut.","tokens_in":22658,"feed_emoji":"🧩","tokens_out":6262,"duration_ms":61959,"temperature":0.7,"pith_summary":"The paper asks whether a language model is better used as a formalizer than as a planner. As a formalizer, the model translates a natural-language description of a planning environment into a complete PDDL domain file and problem file, which a deterministic planner then solves. The authors benchmark this on four IPC planning domains with descriptions at three levels of naturalness. They find that models large enough to write PDDL often get more correct plans this way than by generating plans directly: gpt-4o as formalizer solves 60 of 100 blocks problems versus 33 of 100 as planner. Performance drops as descriptions become more natural and omit implied facts, and error analysis traces failures to syntax errors in weaker models and semantic errors in the domain or problem file in stronger ones.","feed_headline":"Ask LLMs to write PDDL, and they plan better","feed_subtitle":"On 100 BlocksWorld problems, gpt-4o as formalizer solves 60; as direct planner, 33.","key_machinery":"The central machinery is the PDDL pair (domain file plus problem file) written by the LLM and solved by an external planner. The domain file defines predicates, action preconditions, and effects; the problem file defines objects, initial state, and goal. Solvability is tested with the dual-bfws-ffparser planner and correctness with VAL against ground-truth files. To probe how descriptions matter, the paper builds three naturalness levels—Heavily Templated, Moderately Templated, and Natural—and adds Mystery BlocksWorld, a renamed version of BlocksWorld used as a wug test to reveal reliance on memorized names.","core_discovery":"The central claim is that LLM-as-formalizer—generating the complete PDDL domain file and problem file from a natural-language description, then handing those files to a deterministic planner—is a viable and often better methodology than asking the LLM to produce the plan itself. The evidence: on BlocksWorld-100, gpt-4o as formalizer attains 60/100 correct plans on Natural descriptions and 89/100 on Heavily Templated ones, versus 33/100 and 29/100 as planner; formalization also handles the renamed predicates and actions of Mystery BlocksWorld, where direct planning finds nothing. But the advantage is not universal: o3-mini and DeepSeek-R1 are as good or better planners on some settings, and on the harder Barman domain nearly everything fails. The paper also claims naturalness is the main limit: human-like descriptions that omit implied preconditions such as 'clear' reduce solvability and correctness across models.","pith_inferences":["If the planner baseline is strengthened with a feedback loop that validates candidate plans and lets the model retry, the formalizer's advantage probably shrinks; the paper itself names this as a likely stronger baseline.","A commonsense-recovery pre-pass that makes implied facts such as 'clear' explicit before PDDL generation could close much of the natural-description gap documented in the error analysis.","Because full PDDL generation turns the initial state into a prediction target, previous partial-PDDL results likely overstated readiness; deployment decisions should concentrate on problem-file errors.","A natural extension is to test the same formalizer-versus-planner comparison on partially observable or longer-horizon environments, where the deterministic solver's guarantees may interact differently with description naturalness."],"forward_implications":["Formalizer gains are largest on simple, fully observed domains, which is exactly where direct planners fail most; users should prefer generating a complete model over generating a plan in such settings.","Templated descriptions overestimate ability, so evaluations that use only templated inputs will look better than real deployments where users describe environments loosely.","Models that cannot write low-resource formal languages, such as Llama up to 405B, cannot use this methodology at all, pointing to syntax-level code generation as a bottleneck.","Semantic errors persist even in strong models, especially in the problem file's initial and goal states, so future work should target semantic verification rather than only syntactic correctness.","The formalizer advantage is not universal: reasoning-oriented models such as o3-mini and DeepSeek-R1 can plan as well or better, so the choice between formalizer and planner should be made per model, per domain, and per description naturalness."],"supporting_citations":[{"why":"Supplies the PlanBench-style planning benchmark, the Mystery BlocksWorld control domain, and the templated descriptions reused as Heavily Templated inputs.","marker":"Valmeekam et al. (2024a)"},{"why":"Closest prior work that generates the domain file and problem goal; it is the baseline this paper extends to full domain and problem file prediction.","marker":"Guan et al. (2023)"},{"why":"Defines the solvability and correctness metrics that score whether generated PDDL is syntactically usable and whether the resulting plan is right.","marker":"Zuo et al. (2024)"},{"why":"Provides VAL, the validator that checks whether a planner's plan is executable in the ground-truth domain and reaches the goal state.","marker":"Howey et al. (2004)"},{"why":"Provides Planning.Domains' dual-bfws-ffparser, the solver used to measure whether generated PDDL is solvable at all.","marker":"Muise (2016)"},{"why":"Earlier LLM-as-formalizer work that predicts only part of the problem file; its BlocksWorld usage anchors the benchmark design here.","marker":"Liu et al. (2023a)"},{"why":"Describes the stronger planner baseline that combines LLM proposals with symbolic validation, which the paper concedes may beat the naive planner baseline.","marker":"Kambhampati et al. (2024)"},{"why":"Evidence that LLMs struggle to generate formal plans directly, motivating the formalizer-versus-planner comparison.","marker":"Silver et al. (2024)"}],"fun_headline_variants":["LLM-to-PDDL beats direct planning: 60 vs 33 on BlocksWorld","Formalize the domain, then plan: LLM-based PDDL wins","PDDL formalization lifts LLM planning: 60% vs 33%","Write PDDL, not plans: LLM formalizer outperforms","Naturalness limits LLM PDDL formalization accuracy"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The headline comparison assumes that the LLM-as-planner baseline is a single zero-shot pass with no checking or retries; if a planner baseline is allowed to validate its plans and revise, the formalizer's advantage may shrink or vanish.","fun_headline_variants_meta":{"raw":{"variants":["LLM-to-PDDL beats direct planning: 60 vs 33 on BlocksWorld","Formalize the domain, then plan: LLM-based PDDL wins","PDDL formalization lifts LLM planning: 60% vs 33%","Write PDDL, not plans: LLM formalizer outperforms","Naturalness limits LLM PDDL formalization accuracy"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000241,"raw_usage":{"total_tokens":1499,"prompt_tokens":900,"completion_tokens":599,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":516,"completion_tokens_details":{"reasoning_tokens":498}},"tokens_in":516,"tokens_out":599,"duration_ms":6462,"temperature":1.0,"reasoning_tokens":498,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T16:36:57.811961+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the same 100 BlocksWorld problems with a planner loop that lets gpt-4o propose a plan, checks it with VAL, returns the error message, and lets the model revise for a few rounds; if that loop reaches or exceeds the formalizer's 60/100 correctness, the paper's claim that formalization is the better methodology would be undercut.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Closest prior work that generates the domain file and problem goal; it is the baseline this paper extends to full domain and problem file prediction."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides Planning.Domains' dual-bfws-ffparser, the solver used to measure whether generated PDDL is solvable at all."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Evidence that LLMs struggle to generate formal plans directly, motivating the formalizer-versus-planner comparison."}],"review_version":1}