PaperlayerView exact revision on arXiv

Source-linked AI summary

Logic-VLA: A Temporal Logic Conditioned Vision-Language-Action Model

Celina Shiyu Wang, Yiqi Zhao, Junjie Ye, Yue Wang, Jyotirmoy V. Deshmukh

arXiv:2608.20556v1cs.ROcs.LOeess.SY

TL;DR

Natural-language instructions may underspecify safety-critical and spatiotemporal behavior requirements. Logic-VLA conditions a single VLA on STL specifications and improves requirement satisfaction over an STL-blind base policy by 24.8 to 40.7 pp while reducing nominal task success by at most 1.8 pp.

  • Problem

    Natural-language task instructions may underspecify safety-critical and spatiotemporal requirements on robot behavior.

  • Method

    Logic-VLA combines a syntax-graph STL encoder with two-stage post-training on satisfying demonstrations and matched satisfying-violating trajectories.

  • Results

    24.8 to 40.7 percentage points (pp) higher STL satisfaction than the STL-blind base policy, with nominal-task success reduced by at most 1.8 pp.

  • Takeaways & Limitations

    Formal logic can condition a single VLA to adapt to varying safety-critical and spatiotemporal requirements while minimally reducing nominal NL task success.

Abstract

from arXiv · show

Vision-language-action (VLA) models can follow natural-language (NL) task instructions, but such instructions may not precisely specify safety-critical or spatiotemporal requirements on the resulting behavior. We introduce Logic-VLA, a formal-requirement-aware VLA that conditions on Signal Temporal Logic (STL) specifications supplied at inference time. Logic-VLA uses a syntax-graph-based STL encoder pre-trained to capture temporal logic semantics. Policy adaptation proceeds in two stages: STL-conditioned supervised fine-tuning on satisfying demonstrations is followed by trajectory-level preference optimization over matched satisfying-violating rollout pairs using a flow-matching surrogate for Identity Preference Optimization. This formulation improves formal requirement satisfaction while preserving the nominal NL task. We evaluate Logic-VLA in closed-loop quadcopter navigation simulation across randomized photorealistic environments and test generalization to STL formulas unseen during training. Across the evaluation benchmarks, Logic-VLA improves STL satisfaction rate over an STL-blind base policy by 24.8 to 40.7 percentage points (pp) while reducing nominal NL task success by at most 1.8 pp, showing that a single VLA can adapt its behavior to varying formal requirements without requiring a separate policy for each specification.

I. INTRODUCTION · II. RELATED WORK · A. Vision-Language-Action Models

Logic-VLA extends a pre-trained VLA with inference-time Signal Temporal Logic conditioning so one policy can satisfy formal trajectory requirements while retaining natural-language task following. It combines syntax-graph logic encoding with two-stage post-training and improves satisfaction on closed-loop quadcopter navigation with minimal nominal-task degradation.

  • A. Vision-Language-Action Models: VLA models ground pre-trained vision-language representations in visuomotor action generation for manipulation, navigation, and other embodied tasks [1],, [8].They take an observation and natural-language instruction as inputs.
  • I. INTRODUCTION: Logic-VLA adapts a single pre-trained VLA to visual observations, an NL task, and an inference-time STL specification.The formal requirement is supplied as a policy input rather than requiring a separate policy for each requirement.
  • I. INTRODUCTION: The model fuses structured formal requirements with multimodal VLA inputs through a syntax-graph STL encoder built on TeLoGraF [6].The implementation builds on π0.5 [1].
  • I. INTRODUCTION: Post-training first uses STL-conditioned supervised fine-tuning on satisfying demonstrations, then trajectory-level preference optimization over matched satisfying–violating executions.This procedure incorporates formal trajectory requirements into a pre-trained policy.
  • A. Vision-Language-Action Models: Natural-language instructions may describe desired behavior without precisely specifying execution requirements such as obstacle-clearance margins.This motivates supplementing NL task descriptions with formal temporal requirements.
  • II. RELATED WORK · A. Vision-Language-Action Models: Related safety-aware approaches use control barrier functions and MPC as safety filters, while temporal logic synthesis enforces safety during execution [10]–.These directions address the gap between NL descriptions and precise safety requirements.

B. VLA Post-training · C. Planning and Learning with Signal Temporal Logic · III. PRELIMINARY

The preliminary sections motivate conditioning VLA policies on formal spatiotemporal requirements: preference optimization learns from execution comparisons, while STL provides precise trajectory specifications and satisfaction semantics. Logic-VLA obtains supervision from formal temporal-logic semantics rather than imposing one global notion of safety.

  • B. VLA Post-training: Preference optimization, [18] complements supervised fine-tuning by distinguishing preferred from dispreferred executions of the same task.DPO optimizes directly against preferred and dispreferred samples relative to a reference policy, while IPO offers an alternative.
  • B. VLA Post-training: Robot-policy post-training methods extend trajectorywise preference learning to task completion, safety, and efficiency, including GRAPE [22] and flow-matching-specific FlowPRO [23].
  • B. VLA Post-training: Formal temporal-logic semantics provide supervision for post-training, avoiding bias toward a single global notion of safety.
  • C. Planning and Learning with Signal Temporal Logic: STL, specifies spatiotemporal properties of state trajectories and supplies robust semantics measuring their degree of satisfaction.It has been incorporated into optimization-based, and sampling-based planning, robot learning, specification-conditioned reinforcement learning [29], and generative models [6],.
  • C. Planning and Learning with Signal Temporal Logic: Deployment-time approaches enforce formal requirements through additional optimization, reasoning, planning, monitoring, replanning, or STL-aware safety filtering.Examples include robust-semantics-guided generative-policy sampling [33], hierarchical STL frameworks [34], and time-varying Control Barrier Functions.
  • III. PRELIMINARY: An off-the-shelf VLA πθ maps high-dimensional observations and an NL task to sampled action chunks, while an execution rule selects applied actions as unknown dynamics evolve the system.
  • III. PRELIMINARY: NL task completion does not guarantee formal compliance, such as maintaining a prescribed distance from a table or returning to base before a deadline.These requirements can be difficult to express and evaluate precisely using natural language alone.

A. Signal Temporal Logic · B. Problem Formulation

The paper treats Signal Temporal Logic (STL) formulas as formal trajectory requirements and formulates post-training a VLA to satisfy deployment-time STL constraints while preserving nominal natural-language task performance. Logic-VLA adds STL conditioning and adapts a pretrained base policy under nonconflicting requirements using in-domain trajectory data.

  • A. Signal Temporal Logic: STL formulas provide formal requirements on system trajectories, with predicates expressing spatial relations such as obstacle avoidance.STL also derives disjunction, implication, eventually, and globally operators from its core operators.
  • A. Signal Temporal Logic: STL satisfaction is evaluated at a trajectory time, and robust semantics quantify both whether a formula is satisfied and how strongly it is satisfied.A trajectory satisfies ϕ when ρϕ(s, τ0) > 0, with larger robustness indicating stronger satisfaction; evaluation requires a sufficient termination horizon Hϕ.
  • B. Problem Formulation: The formal problem seeks an adaptation ˜θ = A(θ) that preserves the base policy’s natural-language task behavior while adding deployment-time STL conditioning.The base VLA has fixed natural-language and environment distributions, and its dynamics operate within the environment distribution.
  • B. Problem Formulation: Logic-VLA post-trains a pretrained VLA so inference conditions jointly on observations, natural-language tasks, and STL requirements while producing trajectories satisfying both requirements.The STL requirement must not conflict with the natural-language specification.
  • B. Problem Formulation: Post-training must avoid degrading natural-language performance, learn STL spatiotemporal semantics reliably, and optimize global long-horizon trajectory requirements.These challenges motivate adapting behavior without substantially altering the base policy’s rollout distribution or reducing trajectory-level requirements to inadequate local objectives.
  • B. Problem Formulation: The method assumes an in-domain dataset of trajectory, action, natural-language, and observation sequences that supports efficient offline STL monitoring during post-training.Data can come from the base model’s training set or approximately in-distribution rollouts from the base policy.
  • B. Problem Formulation: Problem feasibility requires that the test-time STL requirement and natural-language specification are nonconflicting.The paper states this compatibility condition explicitly as Assumption III.3.
  • B. Problem Formulation: The proposed policy augments the pretrained VLA with an STL conditioning pathway, while the post-training procedure adapts parameters from θ to ˜θ.This defines Logic-VLA as the requirement-conditioned policy produced by the adaptation procedure A.

IV. LOGIC-VLA · A. Logic-Conditioned Supervision Construction

Logic-VLA constructs STL-conditioned supervision from a finite bank of sampled formulas, while allowing inference-time requirements outside that bank. The supervision supports imitation of satisfying executions and preference learning from matched satisfying–violating rollouts.

  • A. Logic-Conditioned Supervision Construction: The supervision construction generates satisfying demonstrations and matched satisfying–violating trajectory pairs for the two post-training stages.These two complementary supervision forms are built from the rollout dataset D and candidate formula bank Φ.
  • A. Logic-Conditioned Supervision Construction: The candidate formula bank Φ is sampled from a distribution over well-formed STL formulas, including their syntax and predicate and temporal parameters.At inference, the requirement ϕ is likewise sampled from the distribution and need not belong to Φ.
  • A. Logic-Conditioned Supervision Construction: Stage 1 learns specification-conditioned behavior by imitating executions that satisfy the given STL requirement.The resulting demonstrations associate rollouts with the STL specifications they satisfy.
  • A. Logic-Conditioned Supervision Construction: Stage 2 uses paired satisfying and violating executions to teach which behavior is preferred under the same task and specification.The preference dataset is constructed at the trajectory level rather than from isolated action chunks.
  • A. Logic-Conditioned Supervision Construction: Each STL-conditioned context includes an action chunk extracted at action-window index τ.The context uses a specification ϕ(j) from the candidate bank that is satisfied by rollout i.
  • A. Logic-Conditioned Supervision Construction: The paired rollouts correspond to the same nominal task and comparable environment and initial conditions, with one rollout clearly violating the same STL formula.This matching provides the basis for contrasting satisfying and violating behavior under a shared requirement.

B. Logic Encoder

The logic encoder represents STL specifications as syntax graphs and pre-trains their embeddings with robust semantics so they capture predicate, temporal, and logical structure. The resulting representation is projected into specification tokens appended to the VLA’s multimodal conditioning stream.

  • STL encoder: Logic-VLA encodes each STL formula as a directed syntax graph whose nodes represent Boolean, temporal, and comparison operators, with operand-to-parent edges.The graph backbone is adopted from TeLoGraF [6].
  • STL encoder: Unlike TeLoGraF [6], the encoder represents only symbolic requirements rather than object geometry or the initial state.Predicate nodes encode signal identity, thresholds, comparisons, and temporal bounds needed to express the requirement.
  • STL encoder pre-training: Robust-semantics pre-training teaches the formula encoder to represent predicate thresholds, temporal bounds, and logical composition that determine satisfaction or violation.Trajectory–formula pairs supervise an auxiliary robust-semantics prediction objective; the trajectory encoder and prediction head are discarded afterward, while the pretrained encoder is fine-tuned with the policy.
  • Downstream conditioning: The pretrained formula representation is projected into Nspec specification tokens and appended after image and natural-language tokens in the VLM prefix.Bidirectional attention allows perceptual representations to condition on the specification.

C. Architecture and Two-Stage Post-training

Logic-VLA appends a semantically pretrained STL representation to π0.5’s vision-language prefix without changing the backbone architecture. It then adapts the policy through STL-conditioned supervised fine-tuning followed by trajectory-level preference optimization over satisfying–violating rollout pairs.

  • Architecture: Logic-VLA uses π0.5 [1] as its backbone, appending the latent STL representation to the vision-language prefix while retaining the pretrained backbone architecture.The post-training recipe is also applicable to other flow-matching policies.
  • Stage 1: STL-conditioned supervised fine-tuning: Stage 1 optimizes π0.5’s conditional flow-matching objective on demonstrations from trajectories satisfying their associated STL requirements.This adapts the policy to imitate satisfying behavior while conditioning on the STL formula.
  • Stage 2: trajectory-level preference optimization: Stage 2 trains on matched satisfying–violating rollout pairs sharing the same natural-language task and STL requirement, learning their STL-dependent preference ordering.Both candidates are evaluated under a shared conditioning context across temporal windows.
  • Stage 2: trajectory-level preference optimization: Because exact likelihood ratios are expensive for flow-matching policies, Stage 2 uses a likelihood-ratio surrogate following Identity Preference Optimization and.The preference margin is optimized toward a finite target with a Huberized IPO-style objective.
  • Stage 2: trajectory-level preference optimization: A one-sided preferred-rollout anchor activates when satisfying-rollout fitting worsens relative to the frozen Stage-1 reference, preserving the satisfying behavior learned in Stage 1.The complete Stage 2 objective combines the preference term with the anchor weighted by λ ≥ 0.

V. EVALUATION

The evaluation examines Logic-VLA through three questions: whether it improves STL requirement satisfaction while preserving nominal NL task performance, generalizes to unseen STL formulas, and benefits from its design choices.

  • Q1: Requirement satisfaction and task preservation: The evaluation first tests whether Logic-VLA improves STL requirement satisfaction while preserving the nominal NL task against STL-conditioned imitation and robust-semantics optimization.
  • Q2: Specification generalization: It then evaluates whether the learned policy generalizes to STL formulas unseen during post-training.
  • Q3: Ablative design choices: Finally, the evaluation investigates the effects of ablative design choices, including pre-training the STL encoder.

A. Experimental Setup

Logic-VLA is evaluated for closed-loop quadcopter navigation across randomized photorealistic warehouses and templated STL requirements. The setup compares STL-aware training methods using satisfaction, robustness, and nominal navigation success metrics.

  • Environment and tasks: The study uses six ordered-target navigation tasks across ten randomized photorealistic warehouse environments with 3,000 collision-free, dynamically feasible reference trajectories.Evaluation uses a DJI Mavic 2 Pro quadcopter model in NVIDIA Isaac Sim 5.1.
  • Evaluation procedure: The evaluation bank contains 1,224 distinct formulas spanning 87 STL structures, organized into 1,449 formula-groups with 8,886 satisfying rollouts and 13,494 preference-pair instances.Formula groups share the same task, environment, and formula while keeping trajectory initial states locally neighboring within the initial-state distribution.
  • Metrics: Each evaluation entry uses 10 closed-loop rollouts and reports STL satisfaction rate, mean and standard-deviation robust semantics, minimum robust semantics, and nominal navigation success.A rollout counts as nominally successful when it reaches all target regions in the prescribed order; zero robust semantics counts as satisfaction.
  • Compared methods: Compared methods include the STL-blind Base, STL-SFT on satisfying demonstrations, Smooth Robust Semantics with 1× or 2× robust-loss weight, and Logic-VLA with preference optimization.Logic-VLA performs STL-SFT first, then optimizes matched satisfying-violating trajectory pairs using an IPO margin and preferred-trajectory anchor.

B. Requirement Satisfaction and Generalization

Logic-VLA achieves the highest STL satisfaction across all three settings while preserving nominal-task success comparable to the base and STL-SFT policies. It improves satisfaction over the STL-blind base policy by 24.8 to 40.7 percentage points.

  • STL-conditioned supervised fine-tuning substantially improves satisfaction over the STL-blind base policy in all three settings.
  • Direct smooth robust-semantics optimization further increases requirement satisfaction but produces a pronounced trade-off with nominal NL task performance.The trade-off arises because maximizing robust semantics changes policy behavior beyond what is necessary for satisfying STL requirements.
  • 24.8 to 40.7 percentage points: Logic-VLA improves STL satisfaction over the STL-blind base policy across all three settings while retaining comparable nominal-task success.It achieves the highest observed STL satisfaction among the evaluated policies.
  • Satisfying–violating rollout pairs provide preference supervision about favored executions that positive-only imitation cannot provide.

C. Ablation Studies

Ablations show that semantic pre-training and structured syntax-graph encoding strengthen STL-conditioned policy learning. Structured encoding provides a larger satisfaction gain than textual prompting on seen specifications while retaining comparable task success.

  • Ablation setup: The ablations compare semantic STL-encoder initialization and structured syntax-graph encoding against direct textual prompting under Seen and Unseen Parameter test settings.Results are reported in Figure 3 using the same evaluation setup as Section V-B.
  • Effect of STL encoder pre-training: Semantic initialization raises STL satisfaction from 46.7% to 61.7% on seen specifications under otherwise matched STL-SFT settings.The comparison is between randomly initialized and semantically pre-trained STL encoders, with all encoder parameters remaining trainable during policy fine-tuning.
  • Structured STL encoding vs. prompting: Structured syntax-graph encoding increases STL satisfaction from 66.5% to 82.0% on seen specifications versus textual prompting, while retaining comparable task success.The prompting baseline appends a textual formula rendering to the natural-language instruction and uses the same two-stage post-training procedure.
  • Structured STL encoding vs. prompting: Direct prompting communicates useful requirement information, but explicitly encoding predicates, temporal operators, and logical composition provides a stronger conditioning signal.This interpretation follows the empirical comparison between structured encoding and the prompting baseline.

VI. CONCLUSION

Logic-VLA is a temporal-logic-conditioned VLA that combines semantic STL encoding with two-stage post-training. In closed-loop quadcopter navigation, it improves STL satisfaction while minimally reducing nominal NL task success versus an STL-blind base policy.

  • VI. CONCLUSION: Logic-VLA combines a semantically pre-trained syntax-graph encoder with two-stage post-training using satisfying demonstrations and matched satisfying-violating trajectory pairs.The two-stage procedure adapts the VLA using both demonstrations and trajectory-level preference information.
  • VI. CONCLUSION: In closed-loop quadcopter navigation, Logic-VLA substantially improves STL satisfaction while minimally reducing NL task success compared with an STL-blind base policy.The conclusion reports this tradeoff at the level of the overall navigation evaluation.
  • VI. CONCLUSION: The results show that formal logic can effectively condition a single VLA to adapt its behavior to formal requirements.This conclusion follows from the reported improvement in formal satisfaction with minimal loss of nominal task success.
Loading 2608.20556v1…