{"id":"b1ccb35f-63e9-43f5-8048-df50cc786ff5","arxiv_id":"2508.18507","paper_version":1,"verdict":"UNVERDICTED","confidence":"LOW","novelty_score":7.0,"correctness_risk":"unknown","formal_verification":"none","parameter_count":0,"one_line_summary":"Language models can write Python policies for PDDL that are provably sound without external verifiers, and LMPlan solves more benchmark problems than existing planners.","lead":"This paper uses language models to write Python programs that act as generalised policies for PDDL planning, claiming these policies are provably sound without an external verifier. If true, the LMPlan system could make LLM-based planning more reliable and scale to problems with hundreds of objects.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Soundness guarantee may be circular: policy and its proof may come from the same LM, with no external verifier.","rationale":"The reader's weakest assumption correctly identifies the independence of the soundness check as load-bearing. My analysis agrees: the abstract's phrase 'without reliance on external verifiers' creates a tension with 'provably sound.' Since the full text is not available, we cannot resolve this ambiguity, so the verdict of UNVERDICTED with low confidence is appropriate. I would not change the verdict; the concern is real but unconfirmed, and the paper might well include a legitimate separate verifier (e.g., a Python program that checks the policy against all reachable states using logical inference). The concrete test will settle it once the full text is examined.","tokens_in":677,"tokens_out":1937,"duration_ms":25425,"concrete_test":"Read the full paper's soundness section (likely §4 or the methodology after the policy generation). Determine whether the generated policy is accompanied by a certificate that is checked by a separate, trusted algorithm (e.g., a symbolic executor, a theorem prover, or a certified PDDL semantics interpreter). If such a checker exists and is independent of the LM, the claim of provable soundness stands; if the LM itself certifies its own output, the claim is unsupported.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The abstract claims 'provably sound relative to the PDDL domain without reliance on external verifiers.' In formal planning, a generalised policy's soundness means that for every reachable state, the policy selects an applicable action and the resulting trajectory eventually achieves the goal. Establishing this over an entire domain (potentially infinite state space) requires a proof, e.g., via loop invariants or well-founded measures. If the LM both generates the policy and generates the proof of soundness, with no independent, mechanically checked validation, the guarantee is only as strong as the LM's reasoning—which is known to be fallible. If the paper instead uses some built-in checker (e.g., a static analyzer for the generated Python code), then that checker is an external verifier (even if not a PDDL planner), contradicting the 'without reliance on external verifiers' phrasing. Thus the central claim is either circular or ambiguous. Full text is unavailable, so this remains a live concern rather than a confirmed flaw.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes LMPlan, a framework that prompts language models to generate Python programs acting as generalised policies for PDDL planning domains. The central claim is that these policies are provably sound relative to the PDDL domain without reliance on external verifiers. Experiments reported in the abstract claim that the approach solves more PDDL problems than existing PDDL planners and recent LM-based methods under fixed time and memory constraints, and can handle problems with several hundred relevant objects. The abstract also reports a surprising robustness to substituting meaningless symbols for natural-language predicates (e.g., '(at dog kitchen)' vs '(p2 o1 o3)').","tokens_in":902,"tokens_out":2074,"duration_ms":26876,"significance":"If the soundness and scalability claims hold, the work would be a significant step toward using LMs for reliable automated planning: synthesizing executable, provably correct generalised policies from PDDL domains and scaling to large object sets. The observed robustness to semantic recoding is also scientifically interesting, as it bears on whether LMs genuinely reason over semantics or exploit structural patterns. However, the abstract alone provides no proof sketch, no verifier description, and no experimental details, so the significance is currently prospective rather than established.","major_comments":[{"comment":"The central claim 'provably sound ... without reliance on external verifiers' is ambiguous and potentially circular. If the same LM that generates the policy also generates its soundness certificate, the guarantee is only as strong as the LM's reasoning and is not an independent proof. If, instead, the framework uses a static analyzer, type checker, or similar mechanism to check invariant annotations, then that checker is an external verifier, contradicting the stated 'without reliance on external verifiers.' The abstract must specify exactly what the soundness proof consists of, which component checks it, and how it covers all reachable states of the PDDL domain.","section":"Abstract"},{"comment":"The empirical claim that 'our policies can solve more PDDL problems than PDDL planners and recent LM approaches' is not assessable without naming baselines, domains, exact problem counts, time/memory limits, and results. There are no error bars or repeated-run information. As presented, the claim is unsupported. A table with baseline names and per-domain solved counts, plus resource settings, is necessary to evaluate the comparison.","section":"Abstract (experiments)"},{"comment":"The phrase 'can solve planning problems with several hundreds of relevant objects' is undefined. Does 'solve' mean finding any plan, proving unsolvability, or achieving goal reachability? Are these empirical successes or guaranteed by the soundness theorem? The distinction between soundness (provable) and coverage (empirical solve rate) must be made explicit to interpret the scalability claim.","section":"Abstract (scalability)"}],"minor_comments":[{"comment":"The term 'provably sound' should be accompanied by a precise definition of soundness for a generalised policy: applicable action at every reachable state, progress toward the goal, and eventual goal achievement. Without this definition, the claim is hard to interpret.","section":"Abstract"},{"comment":"The observation about meaningless symbols is intriguing but stated without experimental detail. If this is a key finding, include control conditions, number of domains, and whether the effect is consistent across LMs and prompts.","section":"Abstract"},{"comment":"The phrase 'generalised policies' is used without clarifying how the generated Python program is instantiated as a policy over PDDL states, especially in regard to grounding predicates and action parameters.","section":"General"}],"recommendation":"uncertain","confidential_remarks":"The decisive issue is the soundness certification mechanism. If the full paper provides a machine-checkable certificate that is independent of the LM's own output, the central claim may be defensible. If not, the paper's headline would be misleading. Since only the abstract is available for review, I cannot resolve this. I recommend that the editor obtain the full manuscript and specifically ask the authors to state, in the text, who or what checks the soundness proof and whether that checker is a trusted external component."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"One thing to know: this is a real idea with a strong headline, but you cannot verify the headline from the abstract alone. The paper proposes generating Python programs as domain-general policies for PDDL problems via an LLM, claims these policies are provably sound relative to the domain, and reports beating PDDL planners on competition benchmarks. That would be a meaningful step for LLM-based planning, where soundness is usually the weak point.\n\nWhat's new: the specific package—LM-generated programmatic policies plus a soundness claim plus the symbol-rewriting observation. That last bit is genuinely surprising and worth chasing down; if LMs plan better on scrambled predicates, the 'semantic reasoning' story needs revision.\n\nWhere it's soft: the abstract doesn't tell us how soundness is established. If the same LM produces both the policy and the proof, the guarantee is not independent; if there is a separate checker, then it's an external verifier in all but name. Either way, the phrase 'without reliance on external verifiers' is doing a lot of work and needs a precise definition. I'm not calling this a hidden flaw—abstracts omit details—but it's the first thing I'd ask the authors. Also missing: benchmark specifics, baseline construction, and any sense of variance. Those are standard for a systems paper, and the abstract's 'solve more' claim needs those numbers before it means anything.\n\nMy guess is the full paper has more substance—the authors know what they're claiming, and the symbol-rewriting result suggests they ran real experiments. But the abstract alone can't support the strongest conclusions.\n\nRecommendation: give this to a competent referee. It's the kind of paper where a good referee will either expose a circular soundness argument or confirm a real advance. Both outcomes are useful. I wouldn't desk-reject it.","headline":"Programmatic LLM policies with a soundness claim is a genuine idea, but the abstract can't establish the guarantee and the benchmark evidence is unverified—worth referee time, not blind trust.","tokens_in":1330,"tokens_out":1702,"would_cite":false,"duration_ms":20020,"reading_group":"maybe","serious_thinker":"unclear","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Language models can write Python programs that act as provably sound generalised policies for PDDL planning domains, solving more benchmark problems than classical planners and scaling to hundreds of objects.","keywords":["PDDL","generalised policies","language models","programmatic policies","automated planning","soundness","LLM planning","symbolic reasoning"],"falsifier":"Take a policy generated by this method for a published PDDL domain, run it on all instances in the test split, and check whether any action violates a precondition or the final state fails to satisfy a goal. One such failure disproves the soundness claim. Alternatively, inspect the internal certificate: if the text that certifies soundness was written by the same LM that wrote the policy, ask an independent validator to confirm the certificate's logic; any mismatch falsifies the no-external-verifier guarantee.","tokens_in":628,"feed_emoji":"🧩","tokens_out":3926,"duration_ms":44086,"temperature":0.7,"pith_summary":"This paper claims that prompting a language model to generate Python programs, rather than plans or free-form text, produces generalised policies for PDDL planning domains that are provably sound without any external verifier. On competition benchmarks, these programmatic policies solve more problems than classical PDDL planners and prior LM-based planners under fixed time and memory, and the resulting system, LMPlan, handles instances with several hundred relevant objects. The authors also report that rewriting natural-language predicates into arbitrary symbols sometimes improves planning performance, a result they say challenges the view that LMs reason over word semantics or memorise solutions from training data.","feed_headline":"LMs write Python programs that provably solve PDDL planning","feed_subtitle":"Prompted once, the programs beat classical planners and scale to hundreds of objects.","key_machinery":"PDDL is the standard formal language for specifying planning domains and problems. The key mechanism is prompting an LM to generate a Python program that acts as a generalised policy — a program that, given any problem instance in a domain, returns an action sequence reaching a goal. The claimed soundness is established within the same pipeline that produces the policy, without calling an external verifier.","core_discovery":"The central claim is that an LM, when prompted to output a Python program encoding a generalised policy for a PDDL domain, can produce a policy whose soundness is guaranteed by a mechanism inside the same pipeline, with no external verifier needed. The paper reports that these policies solve more benchmark problems than traditional PDDL planners and recent LM approaches, and that LMPlan scales to several hundreds of objects. It also reports the surprising observation that replacing English predicate and object names with arbitrary symbols can improve planning performance, suggesting that in this setup the LM operates over the structural syntax of the formal problem rather than relying on wor","pith_inferences":["An implication the authors leave implicit: the 'no external verifier' guarantee is only as strong as the internal certification mechanism; in practice a second, independent LM could be used as a cross-check, but the paper does not appear to require this.","A testable extension: replicating the symbol-rewriting experiment across multiple LMs and domains would clarify whether the improvement is a general property of LM planning or specific to the training distribution of these models.","A further inference: if the soundness certificate is produced by the same LM that writes the policy, a natural stress test is to see whether a weaker or different LM can still verify the policy; failures would indicate the guarantee's limits.","The structural-syntax finding also suggests that prompt design for planning may benefit more from explicit formal scaffolding than from natural-language explanations, which could inform future prompting strategies for other reasoning tasks."],"forward_implications":["PDDL users could obtain per-domain policies directly from an LM without hand-coding control knowledge, provided the soundness guarantee holds.","LM-generated policies could complement classical planners, since they scale to hundreds of objects where search-based planners may struggle.","The arbitrary-symbols result suggests LM planning can work even when domain encodings strip away natural-language semantics, making the approach robust to non-semantic or adversarial renaming.","If soundness is genuinely internal, LM-based planning becomes a program-synthesis task rather than a search problem, which may open new optimisation strategies.","The method could be applied to other formal languages that share PDDL's structured syntax, such as SMT-LIB or ASP, if the prompting scheme transfers."],"supporting_citations":[],"fun_headline_variants":["LMs craft sound PDDL policies as Python code","No verifier? LMPlan proves its own PDDL plans","LMs solve PDDL with provably sound code","Symbols beat words: LMs plan on pure syntax","LMPlan: sound PDDL policies from a single prompt"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The load-bearing premise is that the soundness proof (or certificate) is genuinely independent of the language model that wrote the policy; if the same LM both produces the policy and certifies it, the 'provably sound' guarantee lacks an outside check.","fun_headline_variants_meta":{"raw":{"variants":["LMs craft sound PDDL policies as Python code","No verifier? LMPlan proves its own PDDL plans","LMs solve PDDL with provably sound code","Symbols beat words: LMs plan on pure syntax","LMPlan: sound PDDL policies from a single prompt"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00083,"raw_usage":{"total_tokens":3435,"prompt_tokens":690,"completion_tokens":2745,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":434,"completion_tokens_details":{"reasoning_tokens":2661}},"tokens_in":434,"tokens_out":2745,"duration_ms":22196,"temperature":1.0,"reasoning_tokens":2661,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T16:25:51.944903+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a policy generated by this method for a published PDDL domain, run it on all instances in the test split, and check whether any action violates a precondition or the final state fails to satisfy a goal. One such failure disproves the soundness claim. Alternatively, inspect the internal certificate: if the text that certifies soundness was written by the same LM that wrote the policy, ask an independent validator to confirm the certificate's logic; any mismatch falsifies the no-external-verifier guarantee.","supporting_citations":[],"review_version":1}