{"id":"47e50d35-45ad-4c2b-bb68-6d75fea71ce5","arxiv_id":"2508.21449","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"SYNTH learns STRIPS+ action models with implicit action arguments and unobserved predicates from incomplete state-action traces, with conditional completeness guarantees and 100 percent verification in experiments.","lead":"This paper presents SYNTH, an algorithm that learns lifted symbolic action models (STRIPS rules) from state-action traces in which some state predicates and some action arguments are missing. It introduces a STRIPS variant called STRIPS+, proves conditional correctness and completeness, and reports 100 percent verification across 14 planning domains.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 2's 'suitable traces' premise is uncharacterized, so the advertised completeness for the stratified fragment is not established.","rationale":"The reader's weakest_assumption identifies the same load-bearing issue: the 'suitable finite set of traces' is not characterized, and the proof sketch leans on an unsupported claim that every invalid precondition will be refuted by some observed state. My stress-test deepens this into a concrete failure mode: over-approximation of preconditions from a finite trace can silently survive training because the learned precondition Q' includes all atoms true in the observed states. The proof sketch does not rule out this failure, and the experiments' disclosed tuning of trace length/instance size (Section 7) confirms that suitability is not algorithmically guaranteed. This concern does not overturn the empirical contributions or show an error in the algorithm on the tested domains; it delimits the formal claim. The reader already assigned CONDITIONAL for this and related reasons, so I recommend no change to the verdict. The concrete test would settle whether the failure mode is real and whether the theorem's premise can be made explicit.","tokens_in":17496,"tokens_out":6627,"duration_ms":80873,"concrete_test":"Construct a stratified STRIPS+ domain in which a hidden action has no precondition involving a particular fluent C, but where C is true in every state visited by a trace from one instance, while there exists another instance with a reachable state where C is false. Run SYNTH on the first trace. If C is added to the learned preconditions, then the learned domain is not equivalent to the hidden domain on the second instance, demonstrating that Theorem 2's 'suitable T' assumption is essential and currently uncharacterized. A second part of the same test: derive a formal characterization of 'suitable' and check whether any finite trace from the constructed domain can satisfy it; if not, Theorem 2 is vacuous for this domain.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central correctness claim (Theorem 2) rests on the existence of a 'suitable finite set of traces T' that refutes every invalid candidate precondition and witnesses the determinedness of every implicit z variable. The proof sketch (Section 6.3) asserts that 'any invalid precondition will be rendered invalid through a single state in a trace' and that there are finitely many such candidates, but it does not prove that a finite set of traces from finitely many instances can, for every stratified domain, supply such a witnessing state. This matters because Q' (Section 6.2) is built by adding every lifted atom that is true in all observed state-action pairs. If an invalid precondition is true in all observed states but false in some reachable state of an unobserved instance, DL will retain that precondition, making DL strictly more restrictive than D and breaking the 'vice versa' direction of Theorem 2. The paper's own Section 7 discloses that trace length and instance size were selected until SYNTH succeeded, which suggests that the 'suitable' condition is doing substantial work and is not guaranteed by the algorithm. Without a characterization of 'suitable'—e.g., a bound or a property of T that can be checked—the theorem is conditional on an unspecified oracle and does not establish completeness for the stratified STRIPS+ fragment.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces STRIPS+, a variant of STRIPS in which some action arguments are implicit and preconditions may use a limited form of existential quantification, and studies the task of learning a lifted STRIPS+ domain from state-action traces in which both states and actions are incomplete. The proposed algorithm, SYNTH, learns for each action a stratified conjunction of conjunctive queries that determine the implicit arguments, then adds extra preconditions and effects that are valid over the observed traces. The authors claim correctness and completeness for the stratified fragment (Theorem 2) and report 100% verification rates on STRIPS+ translations of several classical planning domains, including settings with selected predicates removed from the observed states. The main weakness is that Theorem 2 is conditional on an uncharacterized notion of a 'suitable finite set of traces,' and the experiments select trace length and instance size until SYNTH succeeds, so the completeness claim is not established as stated.","tokens_in":17664,"tokens_out":3405,"duration_ms":45656,"significance":"If the central claim were established, this would be a meaningful advance: it extends lifted action-model learning from full STRIPS traces to the more realistic setting of minimal action arguments and partially observable state predicates, and the stratified-query formulation gives a tractable handle on implicit arguments. The paper is also commendable for making code and data publicly available and for grounding the semantics in a precise STRIPS+ definition. However, the advertised correctness/completeness result rests on a 'suitable traces' premise that is not characterized, and the empirical evaluation verifies only finitely many sampled state-action pairs after tuning the training data until success. The contribution is therefore currently a promising heuristic algorithm with a conditional theorem, rather than a proven complete learner for the stratified STRIPS+ fragment.","major_comments":[{"comment":"The theorem states equivalence 'for a suitable finite set of traces T' but never characterizes suitability. The proof sketch asserts that any invalid precondition will be rendered invalid through a single state in a trace and that there are finitely many such candidates, but finiteness of candidates does not imply that one finite trace set can witness every invalid precondition across all instances of the hidden domain. Without a bound or a checkable property of T (e.g., a covering condition on reachable states or a PAC-style sample bound), the completeness claim is conditional on an unspecified oracle. This is load-bearing: Section 6.2 builds Q' from atoms true in all observed states, so an invalid precondition that is true in all observed states but false in an unobserved reachable state makes the learned domain strictly more restrictive than the hidden one, breaking the 'vice versa' d","section":"Section 6.3, Theorem 2"},{"comment":"The paper states that 'Both the length of the traces and the size of the instances used to generate the traces were selected so that SYNTH outputs the correct domains.' This confirms that the uncharacterized 'suitable traces' condition is doing substantial work: the algorithm is not shown to succeed for arbitrary traces, and no failure characterization or sample-complexity bound is provided. The abstract and conclusions nevertheless claim correctness and completeness without this caveat. The authors should either characterize suitability, provide a procedure that checks it, or explicitly reframe the theoretical claim as conditional and the experimental result as a heuristic demonstration.","section":"Section 7, Analysis paragraph"},{"comment":"The empirical verification samples a finite number of state-action pairs (#SA) and reports 100% correctness, but this cannot substantiate the universal semantic equivalence asserted in Theorem 2. A finite sample can miss rare states in which the learned preconditions diverge from the hidden domain. Moreover, the verification compares the learned DL with the STRIPS+ translation D, not with the original STRIPS domain D', and the hidden domains themselves are generated by a translation process using preconditions and traces from D'. The evaluation is therefore a useful consistency check, but it does not provide evidence for the quantified 'any instance' claim in Theorem 2. Please state the verification's role as a sanity check rather than a proof of equivalence.","section":"Section 7, Verification and Table 1"}],"minor_comments":[{"comment":"The trace notation 's0, a0, s1, a2, . . .' appears to have a typo: the second action should be a1, not a2.","section":"Definition 6"},{"comment":"The variable Q is used both for the input query Q(x,y,zi) and for the local set of candidate atoms in the first line of EXPAND. This shadowing makes the pseudocode hard to read; please rename the local set, e.g., Cand.","section":"Algorithm 2"},{"comment":"The maximality condition is stated informally ('n is maximal; i.e., no other determined variables can be pushed into z...') and the lexicographic ordering of atoms is introduced only in prose. Since the greedy search depends on this ordering, the paper should state formally what maximality means and whether the returned query depends on the chosen ordering; Theorem 1 does not address order dependence.","section":"Section 6.1, Maximality"},{"comment":"There are several typographical slips, including 'exapansion' in Algorithm 2's explanation and 'lef t' in the c-Puzzle analysis. Also, the notation Q(x,y,zi) is used both for the partial query prefix and for the full conjunction; a consistent notation such as Q_{<=i} would help.","section":"Throughout"},{"comment":"The analysis says the predicate blank 'does not need to be contained in the states' for learning to succeed. This is a nice observation, but it would be useful to state precisely when a predicate can be omitted: the n-puzzle paragraph notes that the same removal fails for the n-puzzle, and the boundary between the two cases is left implicit.","section":"Section 8, c-Puzzle"}],"recommendation":"major_revision","confidential_remarks":"The core issue is the uncharacterized 'suitable traces' premise in Theorem 2. I do not think this is a reject-level flaw: the algorithm and fragment are plausible, and the issue could be addressed by adding a formal witness/sample-complexity condition or by weakening the claimed completeness to a more precise conditional statement with empirical support. The paper would also benefit from being clearer that the evaluation, while careful, is not a proof of the universal equivalence claim. If the authors can supply a checkable condition and adjust the wording of the abstract/conclusions, the paper could be acceptable for publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth a look. The paper opens a real gap in the lifted action-model learning literature: prior work (SIFT, LOCM, Balyo et al.) assumes either full STRIPS actions or full state observability, and Lamanna et al. handle partial observability only with no guarantees. This paper defines STRIPS+, where action arguments can be implicit and preconditions can be existential, and gives SYNTH, a greedy query-construction algorithm that recovers these implicit arguments from state-action traces. The motivating examples are nice, the algorithm is clearly described, and the empirical results are strong on their own terms: 100% verification on held-out instances across 14 domains, with code and data archived. The learned queries (e.g., using ¬at(y,z) to identify the blank in the sliding-tile puzzle) are genuinely elegant.\n\nThe soft spots are real but not fatal. The main one is Theorem 2. The proof sketch says 'any invalid precondition will be rendered invalid through a single state in a trace' and that there are finitely many candidates, but it never shows that a finite set of traces from finitely many instances can supply such a witnessing state for every stratified domain. This is not a minor gap: Q' is built by adding every lifted atom true in all observed state-action pairs, so if an invalid precondition is true in all observed states but false in some reachable state of an unobserved instance, the learned domain is strictly more restrictive and the 'vice versa' direction breaks. The paper's own Section 7 confirms the concern by disclosing that trace length and instance size were selected until SYNTH succeeded. So the advertised 'correctness and completeness' is really a conditional claim: given sufficiently rich traces, SYNTH recovers the domain. The condition is never characterized, not even as a checkable property.\n\nTwo smaller issues. First, verification is done against the authors' own STRIPS+ translation, not against the original STRIPS domains; so it tests the whole pipeline but not the translation step independently. Second, the incomplete-state experiments sit outside the stated theorem, which is fine but should be flagged more explicitly. The n-puzzle vs c-puzzle difference (learnable with cell coordinates, not with separate x/y when blank is removed) is a representation-sensitivity caveat; the authors mention it, but it underscores how much the fragment's expressiveness depends on the chosen predicates.\n\nI would not treat the stress-test concern as a takedown. The central algorithm is well-defined, the code is public, and the empirical reproducibility is strong. The paper is honest about the tuning of traces. What it needs is a serious revision that either proves Theorem 2 with a real characterization of 'suitable', or weakens the theorem to a 'guaranteed success given adequate traces' statement and is upfront that the guarantee is not unconditional.\n\nThis is a paper for planning and model-based RL researchers. It deserves a serious referee, not a desk reject. I'd send it to review, with the expectation that the completeness claim gets tightened.","headline":"Genuinely new variant of action-model learning with a clean algorithm and strong experiments, but the main completeness theorem rests on an uncharacterized 'suitable traces' condition that the experiments tune around.","tokens_in":18267,"tokens_out":1844,"would_cite":true,"duration_ms":20510,"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":"SYNTH recovers hidden planning domains from partial traces, proving that omitted action arguments and missing state predicates can be learned exactly.","keywords":["lifted action model learning","STRIPS+","partial observability","implicit action arguments","conjunctive queries","classical planning","state-action traces","SYNTH"],"falsifier":"Generate a trace from a hidden stratified STRIPS+ domain in which every observed state-action pair has a unique grounding for each implicit variable, but some invalid candidate precondition happens to be true in all observed applications and is never seen as false. Run SYNTH on that trace, then test the learned domain on a new instance where the same precondition is false. If the learned domain applies the action incorrectly, then the 'suitable traces' condition in Theorem 2 is doing essential work and must be characterized rather than assumed.","tokens_in":1582,"feed_emoji":"🧩","tokens_out":1913,"duration_ms":103019,"temperature":0.7,"pith_summary":"The paper tackles a realistic gap: a planning agent often observes only action labels like \"up\" and tile positions, not the full STRIPS state such as the blank cell or all action arguments a STRIPS model requires. It introduces STRIPS+, a variant where missing action arguments are left implicit and recovered by preconditions that uniquely determine them. The learning algorithm SYNTH builds those preconditions as a stratified sequence of conjunctive queries, one implicit variable at a time, then learns the remaining preconditions and effects. The paper proves completeness and, for a suitable finite set of traces from a stratified hidden domain, that the learned domain generates exactly the same state-action traces as the hidden domain. Experiments on STRIPS+ translations of thirteen standard planning domains reach 100% verification on sampled state-action pairs, including on four domains where selected state predicates are removed from the traces.","feed_headline":"SYNTH recovers hidden planning domains from partial traces","feed_subtitle":"Learning exact lifted action models from incomplete observations.","key_machinery":"The carrying object is the stratified conjunctive query Q(x,y,z), a conjunction of lifted atoms built one subquery at a time: each subquery Qi(x,y,zi) determines the value of a new implicit variable zi given x and the previously fixed z variables. SYNTH's EXPAND routine conjoins candidate atoms until TEST returns a unique grounding in every observed state-action pair, discarding queries that are invalid, not determined, or subsumed by an already-known variable. This query acts as a referring expression that recovers the hidden action arguments; the same bindings then let the algorithm read off the remaining universal and existential preconditions and the add/delete effects. Stratification is","core_discovery":"The central claim is that a lifted action model can be learned exactly from traces in which states omit some predicates and actions reveal only a minimal set of arguments. STRIPS+ makes this precise by allowing action schemas a(x) to carry implicit arguments z whose values are determined by the explicit arguments x through the precondition formula; the formula must be a simple, stratified conjunctive query, so implicit values can be computed one z variable at a time. SYNTH learns, for each observed action, a maximal valid query that denotes the same object tuple as the hidden precondition in every trace state where the action applies, then learns the remaining preconditions and the add/delet","pith_inferences":["The paper's 'suitable traces' condition is not characterized explicitly; identifying it would yield a teaching dimension or sample-complexity bound for lifted action-model learning.","The stratification restriction may be more restrictive than necessary: domains where implicit variables can only be determined jointly, rather than one at a time, fall outside the guarantee and would need a different query synthesis strategy.","The authors point toward Atari-like pixel states; if SYNTH's query synthesis generalizes to cell-color representations, it could offer a transparent, lifted alternative to neural world models in model-based RL.","Unused z variables learned by SYNTH, such as 'the other room' in Gripper, suggest the algorithm could also serve as a source of candidate state features for abstraction or options beyond the action model itself."],"forward_implications":["If Theorem 2 holds, traces collected by an agent that sees only action labels and partial state information are sufficient to reconstruct the underlying lifted STRIPS+ model exactly, not approximately.","The learned domain is interchangeable with the hidden one: any trace produced from an instance of the hidden domain is a trace of the learned instance, and vice versa.","Predicates that are artefacts of STRIPS encodings, such as blank, clear, ontable, in-lift, and on, can be dropped from observations and either recovered implicitly or replaced by quantified negated preconditions.","Because the STRIPS+ translation roughly halves the number of observed action arguments, the same traces are more compact than full STRIPS traces yet still support exact learning.","SYNTH also learns referring expressions that are valid but unused in the final model, indicating it recovers more state-dependent functions than the minimal action model needs."],"supporting_citations":[{"why":"Supplies the atom-pattern representation, the well-formed effects assumption that SYNTH inherits, and the STRIPS benchmark domains that are converted into STRIPS+ for the experiments.","marker":"(Gösgens, Jansen, and Geffner 2024)"},{"why":"Defines the PDDL :vars mechanism that directly supports treating z variables in action schemas as implicit arguments, grounding the STRIPS+ language definition.","marker":"(McDermott et al. 1998)"},{"why":"Represents the closest prior setting where action names appear without arguments; STRIPS+ extends this by recovering the arguments as implicit variables rather than assuming they are absent.","marker":"(Balyo et al. 2024)"},{"why":"Defines the partially observable state and action setting that motivates STRIPS+ and provides the comparison point where prior approaches come without guarantees.","marker":"(Lamanna et al. 2025)"}],"fun_headline_variants":["SYNTH learns exact action models from partial traces","SYNTH recovers hidden planning domains from sparse traces","Learning lifted STRIPS+ models from incomplete observations","SYNTH: exact lifted model learning from incomplete data","SYNTH masters incomplete traces to rebuild planning domains"],"cache_read_input_tokens":19840,"weakest_assumption_plain":"The whole guarantee rests on the input traces being rich enough: every hidden implicit argument must appear with all its possible denotations, and every wrong candidate precondition must be contradicted by at least one observed state-action pair; the hidden domain must also be layered so each missing argument can be pinned down one at a time.","fun_headline_variants_meta":{"raw":{"variants":["SYNTH learns exact action models from partial traces","SYNTH recovers hidden planning domains from sparse traces","Learning lifted STRIPS+ models from incomplete observations","SYNTH: exact lifted model learning from incomplete data","SYNTH masters incomplete traces to rebuild planning domains"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00019,"raw_usage":{"total_tokens":1218,"prompt_tokens":827,"completion_tokens":391,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":571,"completion_tokens_details":{"reasoning_tokens":314}},"tokens_in":571,"tokens_out":391,"duration_ms":4444,"temperature":1.0,"reasoning_tokens":314,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-05T14:18:41.444923+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Generate a trace from a hidden stratified STRIPS+ domain in which every observed state-action pair has a unique grounding for each implicit variable, but some invalid candidate precondition happens to be true in all observed applications and is never seen as false. Run SYNTH on that trace, then test the learned domain on a new instance where the same precondition is false. If the learned domain applies the action incorrectly, then the 'suitable traces' condition in Theorem 2 is doing essential work and must be characterized rather than assumed.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the PDDL :vars mechanism that directly supports treating z variables in action schemas as implicit arguments, grounding the STRIPS+ language definition."},{"cited_title":"Planning Domain Model Acquisition from State Traces without Action Parameters","cited_arxiv_id":"2402.10726","evidence_quote":"Represents the closest prior setting where action names appear without arguments; STRIPS+ extends this by recovering the arguments as implicit variables rather than assuming they are absent."},{"cited_title":"E.; and Traverso, P","cited_arxiv_id":null,"evidence_quote":"Defines the partially observable state and action setting that motivates STRIPS+ and provides the comparison point where prior approaches come without guarantees."}],"review_version":1}