Scaling Trusted Autonomy: Towards Generally Capable Verifiable Robots

Benedict Quartey

Figure 1.1: Explicit representations for the book-transfer task. A symbolic description connects the observed scene and desired goal to a sequence of task-level actions, whose physical realization requires motion planning and control. The book-and-vase extension illustrates how the same action models support a new composition. Learned policies can implement individual skills within this structure.

Figure 1.2: Learning the book-transfer behavior from demonstrations. Observation–action examples train a policy that produces robot actions. The schematic emphasizes behavior acquisition; a deployed closed-loop policy receives current observations. Comparing this output with Figure 1.1 identifies the additional task and symbolic-state information needed to use the learned behavior within a planner.

Figure 2.1: An automaton for

\mathbf{F}(k\land\mathbf{F}f)

. State 2 awaits a kitchen visit; state 1 records that the kitchen requirement has been met; state 0 accepts after a qualifying fridge visit. The direct transition from 2 to 0 permits simultaneous satisfaction. The self-loop at 2 also permits a fridge visit before the kitchen, so the formula does not prohibit such a visit. Edge labels describe proposition valuations, not physical actions.

Figure 3.1: LIMP executing the instruction “Bring the green plush toy to the whiteboard in front of it, watch out for the robot in front of the toy” . The robot dynamically detects and grounds open-vocabulary referents with spatial constraints to construct an instruction-specific semantic map, then synthesizes a task and motion plan to solve the task. In this example, the robot navigates from its start location (yellow, A), to the green plush toy (green, B), executes a pick skill then navigates to the whiteboard (blue, C), and executes a place skill. Note that the robot has no prior semantic knowledge of the environment.

Figure 3.2: [A] LIMP translates natural language instructions into temporal logic expressions, where open-vocabulary referents are applied to predicates that correspond to robot skills––note the context-aware resolution of the phrase “blue one” to the referent “blue_sofa”. [B] Vision-language models detect referents, while spatial reasoning disambiguates referent instances to generate a 3D semantic map that localizes instruction-specific referents. [C] Finally, the temporal logic expression is compiled into a finite-state automaton, which a task and motion planner uses with dynamically-generated task progression semantic maps to progressively identify goals and constraints in the environment, and generate a plan that satisfies the high-level task specification.

Figure 3.3: An instruction is first translated into a conventional LTL formula

\phi_{l}

that loosely captures the desired temporal occurrence of referent objects, then into our LTL syntax

\varphi_{l}

with predicate functions that temporally chain required robot skills parameterized by composable referent descriptors.

Figure 3.4: [A] Our spatial grounding module leverages a VLM to detect all referent occurrences from prior observations of the environment. [B] An initial semantic map with all detected referent instances is generated by backprojecting pixels in segmented referent masks unto the 3D map. [C] Each referent’s spatial comparators is resolved with respect to the origin coordinate frame of reference. [D] Failing instances are filtered out to obtain a Referent Semantic Map (RSM) that localizes the exact referent instances described in the instruction.

Figure 3.5: [A] A given instruction translated into our LTL syntax

\varphi_{l}

can be compiled into an equivalent finite-state automaton that captures the temporal constraints of the task. A path through this automaton is selected with a strategy that incrementally picks the next progression state from the initial state to the accepting state. The robot then executes the manipulation options and navigation behaviors dictated by this high-level task plan. [B] To execute navigation objectives our approach generates a task progression semantic map (TPSM) that augments the environment with state transition constraints, localizing goal (yellow) and avoidance (red) regions. Generated TPSMs are converted into 2D obstacle maps for constraint-aware continuous path planning.

Approach	Referent Resolution Accuracy (Average WER) $\downarrow$	Avoidance Constraint Resolution Accuracy (Average WER) $\downarrow$	Spatial Relationship Resolution Accuracy (Average WER) $\downarrow$
NLMap-Saycan	0.09	0.12	0.05
Code-as-Policies	0.22	0.24	0.06
Limp Single Stage Prompting	0.09	0.11	0.05
Limp Two Stage Prompting [Random Embedding]	0.08	0.11	0.03
Limp Two Stage Prompting [Similar Embedding]	0.07	0.04	0.03

Table 3.1: Performance comparison of one-shot instruction understanding and spatial resolution.

Approach	Temporal Alignment Accuracy (% of instructions) $\uparrow$					Planning Success Rate (% of instructions) $\uparrow$
	NLMD	NLMC	OKRB	CT	CST	NLMD	NLMC	OKRB	CT	CST
NLMap-Saycan	88%	96%	100%	32%	41%	75%	96%	100%	35%	38%
Code-as-Policies	58%	68%	100%	35%	38%	46%	68%	100%	38%	38%
Limp Single Stage Prompting	79%	64%	100%	68%	74%	63%	60%	100%	62%	62%
Limp Two Stage Prompting [Random Embedding]	83%	68%	100%	76%	85%	79%	68%	100%	57%	72%
Limp Two Stage Prompting [Similar Embedding]	88%	80%	100%	76%	92%	79%	76%	100%	65%	79%

Table 3.2: Performance comparison of one-shot temporal alignment and plan success rate.

Figure 4.1: A robot can invalidate the map it just used. Instruction 1 moves the ball from under the table to beside the conifer. If instruction 2 is grounded against the original world

W_{0}

, the ball is still represented under the table. Realm instead promotes the evolved world

W_{1}

, preserves the ball’s identity, regenerates the representations used for grounding and planning, and carries the task forward to

W_{2}

. The images are Gaussian renders from the simulated garden sequence; the final panel illustrates the planned terminal configuration. The displayed instructions are abbreviated; Section 4.5 gives the evaluated wording.

Requirement	Meaning
Local change	An action changes the owned object without moving unrelated rows.
Stable identity	One object ID connects grounding, prediction, twin geometry, and later reuse.
Persistent history	A successor is added without overwriting the world from which it came.
Split authority	The planned action fixes predicted object geometry; evidence updates appearance and exposed scene content.
Validated promotion	A reconciled candidate replaces the current prediction only after spatial, visual, and lineage checks.
Synchronized views	Grounding, planning, rendering, and twin artifacts are generated from one named state.

Table 4.1: Design requirements for an evolving robot world.

Figure 4.2: One persistent world, rebuilt for each instruction. At timestep

t

, Realm renders grounding views from the current Gaussian world

W_{t}

and constructs grounded objects, task-progression semantics, digital-twin geometry, and collision geometry. Together these instruction-specific abstractions produce a task-and-motion plan, which can then be rendered against the same state for inspection. Its validated endpoint predicts physical change ( known ); rendering and re-observation construct the reconciled visual evidence ( inferred ); and commit locally updates, validates, and grants

W_{t+1}

authority for future use ( trusted ). The next instruction regenerates its own abstractions from

W_{t+1}

, not from the original capture.

Figure 4.3: How the world evolves. Realm predicts the spatial consequence specified by the plan, renders that prediction to reconcile visual consequences as registered multi-view evidence, then commits by locally updating affected Gaussian support, validating the result, and granting it authority for the next instruction. The four panels show one calibrated view from the clean garden run: parent evidence, the predicted Gaussian render, a geometry-constrained synthetic re-observation, and the committed Gaussian world.

Selector	Rows	Prec./IoU	Recall
Legacy positive voting	724	0.387891	1.000
Stricter positive voting	521	0.519845	1.000
Lower depth tolerance	315	0.670623	1.000
OBB filter	281	0.646528	1.000
Footprint filter	648	0.496164	1.000
Scale/anisotropy filter	721	0.432294	1.000

Table 4.2: Ownership selector analysis for the garden ball.

Figure 4.4: Ownership defines what the action moves. The legacy 724-row selector attaches background support to the ball. The combined 254-row selector remains object-local. Across the seven selector variants, the combined rule improves mask precision/mean IoU from 0.388 to 0.741 while preserving measured recall on the garden ball.

Quantity	Stage 1	Stage 2
Owner rows transformed in prediction	254	254
Non-moved rows exact in prediction	6,124,832	6,137,002
Disocclusion seeds	12,170	3,551
Masked L1 before	0.138485	0.134815
Masked L1 after	0.121646	0.131212
Outside L1 before	0.022277	0.029291

Table 4.3: Spatial and visual continuity across the two world transitions. Row counts describe rigid prediction; image errors compare the predicted and reconciled renders against synthetic targets on validation views. Geometry and opacity drift is measured after restoring the action-owned parameters.

Figure 4.5: Sequential world evolution across two instructions. The ball moves from its observed pose beneath the table to promoted

W_{1}

beside the conifer and then to promoted

W_{2}

on the table. Reconciliation improves held-out changed-region consistency at both stages. Each prediction moves the same 254 owned rows and preserves all other rows exactly; stored history recovers the ancestors. Fifteen detections across rendered views of

W_{1}

associate to one stable object ID.

Figure 5.1: Predicate-Action Skills . Conditioned on current observations

\mathbf{o}

, we model skills as a joint generative process over an action trajectory

\mathbf{x}

and a predicate-belief trajectory

\mathbf{z}

by learning the coupled distribution

p(\mathbf{x},\mathbf{z}\mid\mathbf{o})

. Starting from noise (

\mathbf{x}_{T}

,

\mathbf{z}_{T}

), our model iteratively refines both modalities to produce paired action–outcome rollouts

(\mathbf{x}_{0},\mathbf{z}_{0})

. The resulting predicate-belief trajectory

\mathbf{z}_{0}

provides an online symbolic interface for monitoring skill execution and planning-based skill composition using off-the-shelf planners.

Figure 5.2: Architectures and baselines. (a) Pacts uses a single conditional generative model to sample joint action–predicate rollouts, refined together via DDPM denoising or flow matching. To disentangle joint modeling from multi-task learning, we include a multi-task baseline (b) that shares the same observation encoder but predicts predicates and actions with separate heads trained with a combined loss. Standalone baselines isolate each component: (c) a generative action-only generator that generates actions, and (d) a predicate-only model predicts predicates from observations.

Figure 5.3: Evaluation environments. We evaluate Pacts across (a) PushBarrier , a controlled 2D compositional environment for systematic ablations and planner-based skill sequencing; (b) Kitchen and (c) Coffee Preparation from RoboMimic/MimicGen, which test joint action–predicate modeling under realistic 3D visual manipulation with simulator predicate oracles; and (d) a real-world cube packing task, where a robot packs four colored cubes into a container.

Setting	Approach	Policy Evaluation	Predicate Classification Evaluation
(Objective + Backbone)		Max Reward $\uparrow$	F1 $\uparrow$	Recall $\uparrow$	Precision $\uparrow$	Accuracy $\uparrow$	Observations
DDPM + UNet	Action-Only Generator + Predicate-Only Predictor	0.83 $\pm$ 0.09	$0.9476\text{\,}$	$0.9547\text{\,}$	$0.9471\text{\,}$	$79.40\text{\,}\%$	2403
	Multi-task Baseline (Shared Encoder)	0.77 $\pm$ 0.13	$0.9764\text{\,}$	$0.9712\text{\,}$	$0.9834\text{\,}$	$89.39\text{\,}\%$	2705
	Predicate Action Skill ( Pacts )	1.00 $\pm$ 0.00	$0.9885\text{\,}$	$0.9924\text{\,}$	$0.9849\text{\,}$	$93.78\text{\,}\%$	2234
DDPM + Transformer	Action-Only Generator + Predicate-Only Predictor	0.45 $\pm$ 0.10	$0.9364\text{\,}$	$0.9355\text{\,}$	$0.9561\text{\,}$	$84.18\text{\,}\%$	2800
	Multi-task Baseline (Shared Encoder)	0.33 $\pm$ 0.08	$0.8684\text{\,}$	$0.8705\text{\,}$	$0.8679\text{\,}$	$85.43\text{\,}\%$	2800

Table 5.1: Single-policy rollout evaluation on PushBarrier. We compare Pacts to action-only, predicate-only, and shared-encoder multi-task baselines when learning a single policy for the full task. This isolates whether joint action–outcome modeling degrades action performance and whether it improves predicate prediction in the absence of any skill segmentation or planning. Policy metrics are mean

\pm

standard error over seven seeded rollouts

Setting	Approach	Policy	Predicate Classification
(Objective + Backbone)		Max Reward $\uparrow$	F1 $\uparrow$	Recall $\uparrow$	Precision $\uparrow$	Accuracy $\uparrow$	Observations
DDPM + UNet	Action-Only Generator + Predicate-Only Predictor	0.93 $\pm$ 0.02	$0.9194\text{\,}$	$0.9095\text{\,}$	$0.9479\text{\,}$	$83.98\text{\,}\%$	10476
DDPM + UNet	Predicate Action Skill ( Pacts )	0.96 $\pm$ 0.02	$0.9340\text{\,}$	$0.9271\text{\,}$	$0.9537\text{\,}$	$90.74\text{\,}\%$	10246
DDPM + Transformer	Action-Only Generator + Predicate-Only Predictor	0.97 $\pm$ 0.02	$0.9451\text{\,}$	$0.9360\text{\,}$	$0.9643\text{\,}$	$88.36\text{\,}\%$	10087
DDPM + Transformer	Predicate Action Skill ( Pacts )	0.93 $\pm$ 0.04	$0.9185\text{\,}$	$0.9050\text{\,}$	$0.9531\text{\,}$	$88.03\text{\,}\%$	10103
CFM + UNet	Action-Only Generator + Predicate-Only Predictor	0.99 $\pm$ 0.01	$0.9467\text{\,}$	$0.9407\text{\,}$	$0.9574\text{\,}$	$88.26\text{\,}\%$	10243

Table 5.2: Single-policy rollout evaluation on RoboMimic (Kitchen_d0 + Coffee_d0). We evaluate Pacts and baselines on two RoboMimic manipulation tasks under realistic visual and geometric complexity, training a single policy per task (no planning or composition). Results are averaged across Kitchen and Coffee Preparation, weighting each environment equally. Policy metrics report mean

\pm

SE over seven seeded rollouts, with standard errors propagated across environments. Predicate classification metrics are macro-averaged across predicates within each environment, then averaged across environments.

Figure 5.4: Predicate–action coherence of predicted belief rollouts. We measure how well Pacts ’s predicted predicate-belief rollout matches the predicate outcomes realized after executing its open-loop action chunks. The x-axis reports lookahead

h

steps into the chunk. We plot (left) CrossCons

(h)

(thresholded agreement; higher is better), (middle) CrossBrier

(h)

(Brier score; lower is better), and (right) CrossNLL

(h)

(log loss; lower is better). Horizontal lines are dataset-statistics baselines: constant

\hat{p}{=}0.5

(dotted) and a base-rate/majority predictor from label frequencies (dashed). These baselines ignore both observations and planned actions; outperforming them shows that the predicted rollouts carry information beyond fixed label frequencies. Across objectives and backbones, Pacts maintains high agreement and low losses over the horizon.

Figure 5.5: Skill recomposition and adversarial recovery in PushBarrier. Left to right: starting from the initial state, the planner synthesizes a sequence for a novel subgoal ( open_door

\rightarrow

align_t_block ). After open_door succeeds, an adversarial perturbation ( Gremlin ) closes the door, which invalidates the current plan while aligning the

T

block. Using online predicate-belief estimates to check effects, the system triggers replanning, re-invokes open_door , and then resumes align_t_block to reach the goal.

Figure 6.1: The three trust interfaces and their complementary contributions. LIMP exposes a grounded task and motion plan; PACTS jointly generates actions and predicted predicate trajectories; REALM supplies an evolving spatial representation for subsequent tasks.

Field	Examples	Role
Identity	state ID, logical time, revision type	Distinguishes observed, predicted, reconciled-synthetic, and reconciled-real worlds.
Authority	status, current-state index	Identifies the one state from which subsequent views may be generated.
Persistent state	Gaussian checkpoint, object registry	Stores renderable scene content, stable objects, poses, and ownership.
Derived views	digital twin, planning cloud, grounding/render bundle	Supplies instruction-specific geometry and observations bound to the state.
Action evidence	plan, trajectory binding, released pose	Explains the intervention used to predict the successor.
Observation evidence	calibrated RGB-D, masks, provenance	Explains the appearance and disocclusion information used in reconciliation.

State	Revision	Status	Direct evidence
t0000-observed	observed	historical	6,125,086 Gaussian rows from the captured garden.
t0001-predicted	predicted	historical	254 moved rows; 6,124,832 inactive rows exact.
t0001-reconciled-syn.	reconciled-synthetic	historical	12,170 seeds; improved held-out masked L1; preserved action geometry.
t0002-predicted	predicted	historical	254 moved rows; 6,137,002 inactive rows exact.
t0002-reconciled-syn.	reconciled-synthetic	current	3,551 seeds; improved held-out masked L1; final task views agree.

Scaling Trusted Autonomy: Towards Generally Capable Verifiable Robots

Abstract

Figures & tables

Appendix

Neuro-Symbolic Planning

Learning Structured Robot Policies from Vision-Language Models via Synthetic Neuro-Symbolic Supervision

Agentic Harnesses: LLM-Driven Verification Layers for Robot Autonomy

Verifiable Foundation Models for Robot Safety

Abstract

Neuro-Symbolic Planning

Explore similar work

Learning Structured Robot Policies from Vision-Language Models via Synthetic Neuro-Symbolic Supervision

Agentic Harnesses: LLM-Driven Verification Layers for Robot Autonomy

Verifiable Foundation Models for Robot Safety