1 Introduction↩︎

Embodied task planning studies how an agent should transform a high-level instruction and its surrounding world state into an executable sequence of actions [1], [2]. This problem is increasingly important as robots move from scripted demonstrations toward open-ended household and assistive settings: a command such as “attach the camera to the tripod” is not solved by emitting a verb alone, but by grounding the intended digital camera and tripod in the scene, recognizing that both are initially on the floor, selecting executable grasp and attach actions, and reaching a goal state (attached digital_camera camera_tripod) that can be verified. A practical robot stack therefore organizes itself in layers: a low-level VLA or skill controller turns short subgoals into motor actions [3], while a high-level planner decides which subgoals to issue, in what order, and against which world state. Our work targets the planning-brain layer in between, which converts a natural-language instruction and the current scene into a verified symbolic task structure that the lower layer can execute. Existing solutions to this layer are split: classical PDDL-style and neuro-symbolic planners emphasize formal executability under hand-specified domains [4], [5], while LLM-based planners [6], [7] are fluent on open-world tasks but lack a cheap, deterministic check that the produced plan is valid in the target world.

A natural interface for closing this gap is BDDL, the Behavior Domain Definition Language used in BEHAVIOR-1K and related benchmarks [8]. A BDDL specification encodes the typed objects in a scene, predicates describing the initial state, and predicates defining the goal condition. Although BDDL shares first-order logic with classical PDDL [4], it differs in two ways that matter for our setting: object types are grounded in WordNet synsets such as digital_camera.n.01, which makes the representation open-vocabulary, and BDDL specifies only the scene together with initial and goal predicates, leaving the action model to a simulator-backed library rather than requiring every action schema to be hand-authored. Unlike free-form language instructions, this structure is directly checkable, and unlike low-level robot trajectories, it abstracts away embodiment-specific control and exposes the planning problem itself. BDDL is therefore a natural interface between open-world perception and verifiable plan execution.

We therefore study BDDL-centric embodied planning: given a task description and either an open-world video or an existing task specification, can we construct a verified BDDL representation and use it to train a compact planning model? The goal is not to replace VLA control or physics simulation, but to expose a scalable layer at which task structure can simultaneously provide supervision, execution checks, and reward signals. In this formulation, BDDL is not only an offline evaluation artifact. It is the shared representation that connects data construction, symbolic execution, RL reward design, and response-length control. 1 illustrates this setting with a concrete BDDL-to-execution example.

However, the broader adoption of BDDL still faces several challenges. First, data construction must recover typed objects, initial predicates, and goals from noisy sources, whereas existing BDDL files are usually curated as benchmark metadata [8]. Second, verification must be strict enough to catch physical and symbolic errors but fast enough to score many training rollouts, unlike full simulation loops [9]. Third, compact planning must shorten responses only after executable behavior is reliable. Reasoning models often solve tasks with long outputs [10], but length pressure applied too early can remove useful planning steps and reduce correctness [11]. These challenges are coupled because the same representation must support data construction, plan execution, reward computation, and compression.

Therefore, we propose SymPlan, a three-stage pipeline centered on verified BDDL to address these challenges. First, to construct reliable BDDL specifications from complex visual tasks, SymPlan employs a video-to-BDDL parser to ground task-relevant objects, infer initial predicates, and derive goal predicates from the task description. The resulting draft is further examined by an LLM verifier, which checks syntax, object consistency, predicate feasibility, and goal executability before acceptance. Second, to make BDDL executable and informative for planning-model evaluation, SymPlan rewrites the verified specification into hierarchical planning conversations and executes them with a fast symbolic engine. This engine reports Goal-Completion, Engine-Pass, Strict-Pass, and diagnostic error traces, while the action library is expanded when new predicate requirements arise. Third, to translate symbolic verification into effective model optimization, the same engine is used to filter SFT data and provide rewards for an SFT-initialized DAPO policy [12]. We further incorporate Short-RL’s correctness-gated length penalty and introduce GroupAdapt, which uses the per-prompt group pass rate as a zero-cost difficulty signal to adapt the length tolerance for easy and hard prompts.

Taken together, SymPlan is organized around three design choices that are evaluated throughout the paper:

1. BDDL as the data interface. We formulate a pipeline that converts open-world task evidence and curated task files into verified BDDL, then into planner-facing supervision through extended-BDDL normalization, hierarchical conversations, and automated action discovery ([sec:data_synthesis,app:data,app:action_builder]).

2. Symbolic verification as training feedback. We build a millisecond-latency symbolic engine that verifies generated plans against typed objects, initial states, and goal conditions, exposing deterministic signals for evaluation, rejection sampling, and reward design ([sec:symbolic_engine,sec:reward_design]).

3. Compact executable planning. We combine verifier-driven SFT, symbolic-reward DAPO, and correctness-gated length control so that the 8B planner preserves strict-pass executability while reducing response length on B-100 and B-1000 ([sec:reward_design,sec:length_compression,app:pass_at_k]).

2 Related Work↩︎

2.0.0.1 LLM-based task planning.

Recent work uses LLMs to generate or rank executable plans for embodied agents, either by prompting pretrained models directly [2], [6], [7], [13], [14], grounding proposals with affordances or scene structure [1], [15], or integrating planning into larger embodied systems [3], [16]–[18]. These methods show that language models can express long-horizon intent, but most rely on prompting, heuristic grounding, or downstream simulation feedback. We instead train the planner with deterministic symbolic feedback derived from the task specification.

2.0.0.2 Symbolic and simulation-based verification.

Embodied benchmarks such as VirtualHome [19], AI2-THOR [20], Habitat [9], ALFRED [21], TEACh [22], and BEHAVIOR-1K / OmniGibson [8] provide rich household tasks and simulation environments. Classical planning also offers symbolic representations such as PDDL and STRIPS for plan checking [4], [23], and task-and-motion planning connects symbolic goals to continuous feasibility [24], [25]. Recent neurosymbolic work combines LLM generation with symbolic verification [5]. Full simulation is valuable but too expensive for inner-loop RL, while hand-crafted symbolic domains can be hard to scale. Our verifier is built directly on BDDL, so it inherits typed objects, predicates, and goals from the benchmark specification and can execute candidate plans at millisecond latency.

2.0.0.3 RL and reasoning compression.

Group-based RL methods such as GRPO and DAPO have become effective for training LLM reasoning policies [12], [26], [27], building on broader work on chain-of-thought and verifier-guided reasoning [28]–[30]. Related work also applies RL to embodied or reflective reasoning [31], [32]. A separate line of work reduces verbose reasoning through long-to-short distillation, length penalties, or difficulty-aware budgets [11], [33]–[35]. These methods typically evaluate answers with string matching or language-level judges. In our setting, the final reasoning must produce a syntactically valid, verifier-accepting action sequence, so we gate length compression on symbolic correctness and use the verifier itself as the reward source.

3 Method↩︎

The central idea behind SymPlan is that verified BDDL can serve as the common interface between open-world data, executable verification, and RL training. When a curated BDDL task is available, its typed objects, initial predicates, and goal predicates can be used directly. When only a task description and video are available, a video-to-BDDL parser first grounds task-relevant objects and key frames, infers initial and goal predicates, and passes a draft specification to an LLM verifier for checking. Once verified, the same formal structure can be used to synthesize planner data, execute candidate plans, and compute training rewards. Because new tasks enter the pipeline as BDDL drafts rather than hand-authored domains, SymPlan scales naturally with the task pool: open-world videos and curated benchmarks share a single interface, and the action library itself grows on demand as new predicates are observed ([sec:data_synthesis,app:action_scaling]).

2 summarizes the BDDL-centric data construction and verification workflow, which converts task descriptions and open-world videos into verified BDDL, an expanded action library, verifier signals, error traces, and verified trajectories ([sec:data_synthesis,sec:symbolic_engine]).

3.1 Video/BDDL-to-Data Synthesis and Action Discovery↩︎

SymPlan converts curated BDDL or open-world videos into verifier-aligned planner supervision. For videos, a parser grounds task-relevant objects and key frames, infers initial and goal predicates, and drafts a BDDL specification, and an LLM verifier checks syntax, object consistency, and goal executability, and only accepted drafts enter the data factory. Each verified task is normalized to extended BDDL, a planner-facing expansion of BDDL that preserves the task-relevant objects, initial predicates, and goals while adding realistic scene distractors and their predicates to better recover a cluttered real environment. It is then rewritten into a sample with environment state, robot embodiment, short clarification dialogue, and target steps plus executable code (6).

When new goal predicates are not covered by the current action set, an automatic action builder proposes and compiles the missing callable actions (7).

Cold-start SFT uses symbolic rejection sampling with Gemma-4-31B-IT as the teacher: for each prompt we draw \(K\) rollouts, keep the shortest strict-pass trajectory when any sample passes, and otherwise exclude the prompt. This yields the compact checkpoint D-SFT that initializes RL.

3.2 Symbolic Verification Engine↩︎

Given a generated plan \(y\) consisting of an action sequence \(\langle a_1, a_2, \ldots, a_n \rangle\), the symbolic engine executes each action against a state representation derived from the BDDL task specification [8].

3.2.0.1 State representation.

Each task defines an initial state \(s_0\) (a set of predicates over objects, e.g.(ontop candle table)) and a goal state \(g\) (a conjunction of target predicates). The engine maintains a state \(s_t\) that is updated by each action’s effects. For example, in the gift-basket task, a valid plan may first open a basket, then pick a candle from the table, and finally place it in the basket. If the model skips the open action and directly places an object into a closed basket, the goal may still become partially satisfied, but the violated precondition is recorded in the error set. This is the difference between matching the final goal and producing an executable plan.

3.2.0.2 Execution and verification.

For each action \(a_t\), the engine checks whether its preconditions are satisfied in \(s_t\). If satisfied, the state is updated according to the action’s predefined effects (set/clear specifications). If violated, the action is logged as an error but execution continues to provide maximum feedback. After all actions execute, the engine computes:

• Goal Completion Rate (GCR): \(\mathrm{GCR} = |\{g_i \in g : g_i \text{ satisfied}\}| / |g|\)

• Error set \(\mathcal{E}\): all precondition violations encountered during execution.

• Engine Pass (EP): \(\mathrm{GCR} = 1.0\) (all goals met, errors permitted).

• Strict Pass (SP): \(\mathrm{EP} \wedge |\mathcal{E}| = 0\) (all goals met, no errors).

3.3 SFT-Initialized RL with Multi-Granular Symbolic Rewards↩︎

Training proceeds in two stages. The cold-start rejection-sampling procedure of 3.1 produces D-SFT, which is the sole initialization for RL. The same symbolic verifier that labels supervised trajectories also supplies the RL reward.

3.3.0.1 Optimizer and symbolic reward.

The reward must distinguish three cases that a binary success signal would conflate: a plan that reaches only part of the goal, a plan that reaches the goal after illegal actions, and a strict-pass plan that is both goal-complete and error-free. We therefore shape the answer reward with three symbolic signals from the engine: progress (GCR), legality (precondition errors), and goal completion (EP). We adopt DAPO [12], an extension of GRPO [26] with dynamic sampling, asymmetric clipping (Clip-Higher, \(\epsilon_{\text{low}}{=}0.2\), \(\epsilon_{\text{high}}{=}0.28\)), token-level policy-gradient aggregation, and overlong reward shaping. KL regularization is disabled since the SFT initialization already acts as a strong prior. The total reward is \(R(y)=R_{\text{fmt}}(y)+R_{\text{ans}}(y)+R_{\text{len}}(y)\), where \(R_{\text{fmt}}\) is a binary tag penalty and \(R_{\text{len}}\) is the gated length term of 3.4. The answer reward in 1 combines a continuous base \((-0.5+2.5\,\mathrm{GCR})\), a hard error penalty of \(-1\) when any precondition is violated, and a \(+0.5\) engine-pass bonus: \[R_{\text{ans}} = (-0.5 + 2.5\,\mathrm{GCR}) - \mathbf{1}_{|\mathcal{E}|>0} + 0.5\cdot\mathbf{1}_{\text{EP}}. \label{eq:answer95reward}\tag{1}\] For example, a partial plan receives graded credit through GCR, an engine-pass-only plan loses one point for the illegal action, and a strict-pass plan receives both full goal credit and the EP bonus. The continuous base retains variance on hard prompts that a binary is_successful signal would filter out via DAPO’s dynamic sampling, while the \(\geq\!1\) gap between strict-pass and engine-pass-only outcomes prevents a “conservatism trap” in which a model trades goal coverage for cleanliness. Full reward-landscape analysis is in 8.1.

In the experimental section we evaluate three SFT-initialized variants under a unified naming scheme: DAPO (plain symbolic-reward baseline), DAPO + Short-RL (adds the lazy length penalty), and DAPO + Short-RL + GroupAdapt (our full method, see 3.4).

3.4 Correctness-Gated Length Compression↩︎

Following Short-RL [11], response length is regularized only after the model reaches stable correctness. GroupAdapt keeps this correctness gate but replaces the fixed length tolerance with a task-adaptive one. Its key signal is the current group pass rate: for each prompt, DAPO already samples a group of rollouts, and the fraction of strict-pass rollouts directly reflects how well the current policy handles that prompt. This signal is zero-cost because it is produced by the RL batch itself, requiring no extra difficulty classifier, simulator call, or manual task label.

3.4.0.1 Accuracy gate.

Let \(a_b\) be the current batch SP rate and \(a^*\) its running best. The length reward is gated: \(R_{\text{len}}=0\) whenever \(\neg\,\text{SP}(y)\) or \(a_b<a^*-\epsilon_{\text{acc}}\). Hence the model first learns what to plan before being pushed to plan concisely.

3.4.0.2 Group-adaptive tolerance.

For each prompt \(t\) with group size \(G{=}8\), let \(\rho_t = G^{-1}\sum_{i=1}^{G}\mathbf{1}[\mathrm{SP}(y_i)]\) be the instantaneous strict-pass rate in the current DAPO batch. We set \(\delta_{\text{base}}{=}200\) tokens as the easy-task budget and use a binary easy/hard schedule with threshold \(\tau{=}0.5\): \[\delta_t = \begin{cases} \delta_{\text{base}} & \rho_t \ge \tau \quad (\text{easy})\\ 2\,\delta_{\text{base}} & \rho_t < \tau \quad (\text{hard}) \end{cases} \label{eq:adaptive95tolerance}\tag{2}\] Short-RL uses a fixed \(200\)-token budget for every prompt. GroupAdapt keeps this \(200\)-token tolerance for easy prompts, but gives hard prompts \(400\) tokens of slack. Thus difficult tasks first receive a wider length tolerance, and as their group pass rate improves beyond \(\tau\), they are automatically reassigned to the easy budget.

3.4.0.3 Length reward.

When the accuracy gate is open, \(R_{\text{len}}\) in 3 rewards being within \(\delta_t\) tokens of the shortest known SP length \(\ell^{\min}_t\) for task \(t\) and otherwise decays linearly up to the observed range \(\Delta_t=\ell^{\max}_t-\ell^{\min}_t+\varepsilon\): \[R_{\text{len}}= \begin{cases} 0.5 & \ell(y)\le\ell^{\min}_t+\delta_t\\[2pt] 0.5-\dfrac{\ell(y)-\ell^{\min}_t}{\Delta_t} & \text{otherwise.} \end{cases} \label{eq:len95reward}\tag{3}\] Per-task references \((\ell^{\min}_t,\ell^{\max}_t)\) are updated online using only SP responses, so the compression target always reflects achievable quality. Early in training the gate is closed and the answer reward drives correctness, and once SP stabilizes, the gate opens and GroupAdapt matches Short-RL on easy tasks while protecting hard tasks with a wider \(400\)-token tolerance. When a hard prompt’s group pass rate improves, it automatically moves back to the easy budget. 3 summarizes this SFT-initialized RL workflow.

4 Experiments↩︎

4pt

4.1 Setup↩︎

4.1.0.1 Research questions.

The experiments evaluate four claims: whether symbolic rejection-sampling distillation improves compact planners, how close the distilled planner is to larger open and frontier models, whether SFT-initialized symbolic-reward RL can improve one-sample Strict-Pass, and whether Short-RL plus GroupAdapt can reduce length without sacrificing correctness.

4.1.0.2 Benchmarks and splits.

We evaluate on two benchmarks from BEHAVIOR-1K [8]: Behavior-100 (B-100, 100 tasks, 200 paired single-/dual-arm episodes) and Behavior-1000 (B-1000, 1,000 tasks). To better reflect realistic robot embodiments, each evaluated task is instantiated in single-arm and dual-arm settings when available. For B-1000 we reserve a held-out 97-task, 194-episode test set, which also serves as the RL validation set. The remaining B-1000 tasks form the training pool and are augmented by LLM-based BDDL perturbation to 2,117 training episodes (6.3). For RL analysis, both B-100 and the B-1000 held-out split are in-domain embodied evaluations under the same extended-BDDL planning setting. Following Short-RL [11], we also report out-of-domain mathematical reasoning on AIME24, AIME25, AMC23, and MATH500 as a secondary check for whether length control damages non-embodied reasoning, and it is not an optimization target or a core claim of this paper.

4.1.0.3 Metrics.

We report Strict-Pass (SP: all goals met with zero precondition errors), Engine-Pass (EP: all goals met while allowing execution errors), average Goal Completion Ratio (GCR), and average output length. SP is the primary correctness metric because it requires both goal satisfaction and executable action sequences. Full per-embodiment breakdowns are in 9.2.

4.1.0.4 Baselines.

We compare against a one-sample baseline suite spanning frontier API models (DeepSeek-V4-Flash/Pro, Gemini-3.1-Pro, Kimi-K2.6, GLM-5.1, GPT-5.4) and a broad set of open-weight models, including Gemma-4-31B-IT and the Qwen3 / Qwen3.5 / Qwen3.6 families from 8B to 122B active parameters.

4.1.0.5 Decoding protocol.

Unless a vendor API forces a different setting, all models are decoded at temperature 0.6 and top-\(p\) 0.9 with thinking/reasoning mode enabled when available. Unless stated otherwise, evaluations use the default Guided prompt on the extended-BDDL scene representation. For RL checkpoint evaluations, each table entry and curve point is averaged over three decoding seeds, and non-RL baseline rows use the one-sample protocol. We discuss prompt sensitivity as a limitation rather than making prompt engineering a main experimental axis.

4.1.0.6 Training and SFT initialization.

The RL stage in this paper is scoped to a single initialization, the compact supervised checkpoint D-SFT (Qwen3-8B-Gemma-Distill-SFT), obtained by symbolic rejection sampling from Gemma-4-31B-IT. We use the same prompt and symbolic engine as in evaluation. The SFT-initialized DAPO configuration uses group size \(G{=}8\), and full hyperparameters are in 8.

4.2 Main Results: Baseline Comparison↩︎

1 shows a consistent gain from reusing symbolic verification as training feedback. D-SFT raises Qwen3-8B from 77.3 to 92.3 SP on B-1000 and from 72.0 to 87.0 SP on B-100, and symbolic-reward DAPO further reaches 96.2 and 94.3 SP. Adding Short-RL keeps this accuracy while compressing responses, and the default GroupAdapt configuration reaches the best B-1000 SP and GCR among the 8B variants. The B-100 result is slightly below Short-RL at the final checkpoint, so we interpret GroupAdapt as a correctness-preserving compression strategy rather than a uniform per-dataset accuracy improvement.

4.3 Ablations and Length Analysis↩︎

2 shows that most of the length reduction comes from the correctness-gated Short-RL objective: final output length drops from 999/1253 tokens to 194/242 tokens on B-1000/B-100 while SP is maintained or improved. GroupAdapt then changes how this pressure is applied. Larger \(\tau\) values mark more rollout groups as hard, giving still-unstable prompts temporary \(400\)-token slack before they return to the standard \(200\)-token budget after their group pass rate improves. This explains why \(\tau{=}0.75\) yields the strongest final embodied SP with only a small length increase. We keep \(\tau{=}0.5\) as the default because it is the natural half-pass split selected before the final checkpoint comparison and gives the most balanced trajectory in 4. The math columns are included only as an OOD side-effect check following Short-RL: length-adapted variants are not optimized for mathematical derivations, but GroupAdapt recovers part of Short-RL’s math drop on AIME24, AIME25, and MATH500.

5 Conclusion↩︎

This paper presented SymPlan, a BDDL-centric pipeline for turning open-world or curated task evidence into verifiable planner training. By using verified typed objects, initial predicates, and goal predicates as a shared interface, SymPlan connects data construction, symbolic verification, SFT filtering, and RL reward design. The system constructs or accepts BDDL specifications, rewrites them into hierarchical planning conversations, expands the callable action set through predicate-guided action discovery, and verifies generated plans with deterministic GCR, Engine-Pass, Strict-Pass, and error signals.

Empirically, the pipeline turns the 8B planner into a competitive symbolic executor while keeping its responses short. The final GroupAdapt configuration reaches 97.3 SP on B-1000 with an average response length of 207 tokens, compared with 96.2 SP and 999 tokens for DAPO without length adaptation. The threshold ablation further shows that giving low-pass-rate rollout groups temporary slack is a useful safeguard: harder prompts can first stabilize under a wider budget and later return to the shorter budget as their group success rate improves.

The main technical lesson is that verifier reuse simplifies the entire pipeline. The same symbolic engine that certifies SFT trajectories also supplies dense RL rewards, separating partial goal progress, illegal-but-goal-complete plans, and strict executable success. On top of this reward, Short-RL and GroupAdapt provide a controlled path from accurate planning to concise planning: compression is delayed until correctness stabilizes, and the current group pass rate adapts the length tolerance without extra difficulty classifiers or simulator calls. The appendix pass@\(k\) analysis suggests that the compact planner still has consistency headroom, motivating symbolic-reward RL as a way to convert sampled correct behaviors into more reliable one-sample planning.

Limitations↩︎

SymPlan is a planning model rather than a low-level control policy. Its action space is intentionally abstract: for example, a task such as making coffee is evaluated at the level of symbolic planning steps, not decomposed into fine-grained manipulation primitives. Learning such low-level skills would require separate robot-control training.

A second limitation concerns deployment: a real robot must scan a scene and quickly construct the task-relevant BDDL objects and initial predicates from perception, while the goal can often be derived from the user’s instruction rather than scanned from the scene. Robust real-time scene-to-BDDL construction with diverse cameras and viewpoints therefore remains an open problem.

Finally, our main experiments use the Guided prompt for consistency with D-SFT training, but forbid-style prompts may be more helpful than rule-style prompts for stronger models, and prompt choice therefore remains an evaluation variable rather than a core claim of the method.

The appendix follows the same pipeline order as the main paper: 6 details data construction, 7 describes the symbolic engine and action library, 8 collects RL training details, and 9 reports additional evaluation analyses.

6 Data Construction Details↩︎

This appendix summarizes the conversion from raw BDDL to planner-facing conversations. Each sample is built by parsing objects, initial predicates, and goals, identifying the robot type, selecting the corresponding action library and system prompt, and rewriting the formal goal into a natural-language request. Distractor objects are retained to test whether the model identifies task-relevant objects. This section first describes video-to-BDDL conversion (6.1), then shows the model-facing sample format (6.2), and finally summarizes data augmentation (6.3). 7 gives one concrete example.

6.1 Video-to-BDDL Construction↩︎

When the source is a video or other visual scene evidence, SymPlan uses the task description as a prior for deciding what to look for. The instruction specifies the target objects and related context objects that should be grounded, while the video supplies evidence for where those objects are and what states or relations they currently satisfy. The conversion has three stages. First, the task description is parsed into a search plan over relevant object categories, such as target objects, tools, containers, surfaces, and the agent. Second, the visual front end follows the Set-of-Mark visual prompting style [36] to select frames that expose these objects and ground them as BDDL instances, in the spirit of open-vocabulary detection references such as [37], and observable initial predicates are then created from spatial and state evidence, including room membership, support, containment, open/closed state, cleanliness, and similar task-relevant properties. Third, the task instruction is converted into goal predicates over the same typed objects. The resulting BDDL is accepted only after an LLM-as-a-judge verifier [38], [39] confirms syntax, object coverage, initial-state consistency, and goal executability, matching the four content axes used by the symbolic engine.

5 summarizes this construction pipeline. The important design choice is that the same verified BDDL serves three roles: it is rewritten into the planner prompt, it defines the target condition for training examples, and it is reused unchanged by the symbolic engine when executing generated action code.

6.1.0.1 Quantitative evaluation.

Following the pipeline in 5, we apply it to 50 BEHAVIOR-1K task videos from our evaluation suite and report four indicators in 3.

4pt

The engine and the verifier accept the large majority of drafts at 100% and 74%, with 36/50 drafts agreeing with the released BDDL on core semantics, and on 32/50 the judge prefers our BDDL with respect to the natural-language instruction. The 14/50 disagreements are dominated by scene-decoration objects (sauces, packaging, room decor) declared in the released BDDL but not required by the instruction, suggesting that the construction is grounded in the written task rather than memorising static curation choices.

The example in 6 illustrates a typical disagreement of this kind. Both BDDLs cover the three Easter eggs, the basket, the lawn, and a tree, and both place the eggs inside the basket initially. The video-derived goal places all three eggs next to the same tree, which matches the natural-language instruction verbatim. The released goal instead places one egg next to a scrub, which is a curation artifact rather than a planning requirement, and the judge accordingly counts this case toward our Instruction Alignment Win Rate. This kind of mismatch supports our design choice of treating the natural-language task as authoritative when the visual evidence and the released BDDL disagree.

6.2 Data Sample↩︎

7 illustrates the conversion from a raw BDDL task to the model-facing conversation format. The formal BDDL goal is used during data construction, but it is not exposed verbatim to the model, and instead, it is rewritten as a natural-language request in the dialogue.

6.3 Data Augmentation↩︎

We augment the B-1000 training partition with two GPT-4o-based strategies, summarized in ¿tbl:tab:aug95strategies?. Each augmented BDDL is checked for tool consistency, and invalid drafts are excluded from the training set. Training pairs each task definition with one robot embodiment, while evaluation uses both single-arm and dual-arm settings, and the resulting split sizes are reported in [tab:data95stats].

7 Symbolic Engine and Action Library↩︎

This section documents the execution layer behind the symbolic feedback used in the main paper. We first replay one verified plan (7.1), then describe action-set scaling (7.2), predicate resolution (7.3), and the complete action library (7.4).

7.1 Symbolic Engine Replay↩︎

After the planner emits action code, the symbolic engine executes the code against the same BDDL state and goal. 8 illustrates this replay on a compact grocery-store task. The symbolic panels show the initial state and the verified final state, while the visual schematic gives a human-readable view of the task and generated high-level steps.

7.2 Action Set Scaling↩︎

4 summarizes the action-set expansion from the 14-action B-100 engine to the 34-action B-1000 engine. Predicate gap analysis on B-1000 identifies 23 uncovered predicate requirements, and after consolidation and LLM review, these become 20 accepted action additions with full resolved-goal coverage.

Concretely, auto-discovery first normalizes B-1000 goal predicates through alias, regex, composite, and handled-format rules. Predicates that cannot be mapped to the existing B-100 action effects are counted as uncovered requirements. The proposal stage groups semantically equivalent requirements, infers action names and arguments from predicate morphology and goal co-occurrence patterns, and uses LLM review to check the proposed action semantics. A proposed action is accepted only if its emitted effect resolves at least one previously uncovered requirement without introducing invalid arguments or conflicting state updates. Coverage is computed after validation as the fraction of normalized goal-predicate requirements supported by either the original action set or the accepted additions. The reduction from 23 uncovered requirements to 20 additions is due to consolidation: several requirements share the same action schema after normalization.

6pt

7.3 Predicate Resolution Rules↩︎

The rules used for predicate resolution during the gap analysis are detailed in 5.

3pt

7.3.0.1 Mapping to the implementation.

The three stages described in 3.1 (gap analysis, LLM-assisted proposal, symbolic code synthesis) are realized by a six-phase implementation: scan and classify operationalize gap analysis by partitioning the observed goal predicates into covered / format-variant / truly missing buckets, while infer and propose operationalize LLM-assisted proposal by combining morphology-based parameter / verb inference, goal co-occurrence mining, and optional LLM review, and validate and emit operationalize symbolic code synthesis by scoring the proposed set against a reference library and emitting engine code, tool prompts, and allowed-function patches. This factorization is an engineering detail and is orthogonal to the paper’s claims, and it only affects the ease of extending the action library to new predicate families.

7.4 Complete Action List↩︎

[tab:base_actions,tab:b1000_actions] present the complete action library, separating the base B-100 actions from the B-1000 additions.

2.5pt

2.5pt

8 Training and RL Details↩︎

This section contains the RL configuration and reward details that support [sec:reward_design,sec:length_compression]. We list the shared DAPO hyperparameters in 8 and the reward ordering in 8.1.

3pt

8.1 Reward Landscape Details↩︎

9 lists the reward values produced by the multi-granular symbolic reward (3.3) for representative plan outcomes. The ordering ensures that complete, error-free plans (Strict Pass) always receive the highest reward, while partial successes are rewarded proportionally.

4pt

9 Additional Evaluation Analysis↩︎

This section collects analyses that support but are not required for the main comparison: additional RL curves (9.1), embodiment-specific behavior (9.2), task-horizon statistics (9.3), and pass@\(k\) headroom (9.4).

9.1 Additional RL Curves↩︎

9 complements the main SP/length curves by reporting Goal Completion Ratio and engine error rate. GCR shows whether methods preserve partial task progress, while the error-rate curves show whether higher SP comes from cleaner executable plans rather than merely satisfying goals with invalid intermediate actions.

9.2 Single-arm vs.Dual-arm Comparison↩︎

10 summarizes the single-arm and dual-arm setup, and 11 reports the comparison on B-1000.

3pt

On B-1000, dual-arm settings usually reduce executable command count, while changes in error rate and goal completion remain more model-dependent. This suggests that embodiment mainly affects coordination burden and plan efficiency rather than the semantic difficulty of the task itself.

2.5pt

9.3 Task Complexity Analysis↩︎

To characterize benchmark difficulty, we analyze the distribution of executable command count (the number of primitive robot actions in each generated plan) on B-100 and B-1000. This metric reflects task complexity: more commands correspond to multi-step tasks with more objects or longer action sequences. Command count is distinct from response-token length: it measures the symbolic action horizon rather than verbal verbosity.

10 summarizes the executable command count for GPT-5.4 with per-bin histograms and summary statistics. The model produces a median of 19 commands on B-100 (average 23.8, P90 = 45) and a median of 14.5 commands on B-1000 (average 18.6, P90 = 32), showing a heavier B-100 action-horizon distribution. The right-skewed tails indicate that some tasks require substantially longer symbolic action sequences than the median case.

9.4 Pass@\(k\) Analysis: RL Headroom↩︎

To assess how much reinforcement learning can still improve the distilled checkpoint D-SFT, we perform a pass@\(k\) analysis on both B-100 and B-1000 using the guided extended-BDDL multi-sample evaluation. For each task occurrence we draw \(n{=}10\) independent samples with temperature \(0.6\) and \(\text{top-}p{=}0.9\), and evaluate each with the symbolic engine. We then compute pass@\(k\) using the unbiased estimator in 4 from Chen et al. [40]: \[\text{pass@}k = \mathbb{E}_{\text{tasks}}\!\left[ 1 - \frac{\binom{n-c}{k}}{\binom{n}{k}} \right] \label{eq:pass95at95k}\tag{4}\] where \(n\) is the total number of samples per task occurrence and \(c\) is the number of strict-passing samples.

12 shows that D-SFT has non-trivial consistency headroom even after distillation. Strict pass@1 is already high, but pass@10 rises to 97.0% on B-100 and 99.0% on B-1000, leaving 11.6 and 7.6 points of recoverable one-sample reliability, respectively. This is the kind of gap that group-based symbolic RL is designed to close.

6pt

9.4.0.1 Consistency analysis.

13 breaks down how reliably D-SFT solves each task occurrence across the same \(n{=}10\) samples. B-100 has a larger “sometimes pass” bucket than B-1000, suggesting that the smaller but structurally richer split still contains more prompts where the policy can solve the task but does not do so consistently.

5pt

9.4.0.2 Length–correctness relationship.

Across the B-1000 multi-sample run, failing responses remain on average noticeably longer than strict-passing ones for the same prompt. We do not interpret this gap as evidence that verbosity directly causes errors: harder tasks naturally induce both longer outputs and more failures. Rather, we take it as a practical signal that length cannot be reduced uniformly across samples: trimming long correct plans is unlikely to help, while trimming long failing plans may amount to truncating genuinely needed reasoning. This observation directly motivates the correctness-gated compression used in the final RL stage.

9.4.0.3 GroupAdapt threshold.

The same consistency view also motivates the group-adaptive tolerance in 2 . During DAPO, each prompt is represented by a rollout group of size \(G{=}8\). We therefore treat groups with at least half of the rollouts passing as easy (4–8 / 8), and the remaining groups as hard (0–3 / 8). Reliable prompts can be compressed under the Short-RL budget, while less reliable prompts keep wider length slack until their pass rate improves. The resulting two-level schedule keeps \(\delta_{\text{base}}{=}200\) on easy groups and widens to \(400\) tokens on hard groups (2 ). The main configuration uses \(\tau{=}0.5\), and the ablation in 4 additionally evaluates \(\tau\in\{0.25,0.75\}\).

References↩︎

---

1.  Corresponding author.↩︎