Teaching Robots to Follow Rules Without Retraining: STL-Constrained Action Distribution Shaping

Paper: 2603.17969 Authors: Sadık Bera Yüksel, Derya Aksaray Categories: cs.RO, cs.AI

The Gap

Robotics foundation models (think RT-2, OpenVLA, and theirkin) are impressive generalists. You give them a natural language instruction and they produce actions. But they’re trained to be statistically plausible, not formally correct. There’s no mechanism inside them that says “you must visit zone A before zone B, and never enter zone C after time step10.” They might do it by luck. They might not.

Prior work on safe robot control mostly lives in two camps. The first camp is formal methods — temporal logic planers, model predictive control with constraints, barrier functions. These work beautifully when you have a hand-crafted model of the world, but they don’t plug into a neural foundation model that speaks in latent embedings. The second camp is RLHF-style finetuning or constrained RL — you can nudge a model toward safer behavior, but you’re retraining, which is expensive, britle, and requires you to anticipate every spec at training time.

The gap: nobody had a clean way to take a frozen, pretrained robotics foundation model and enforce rich, time-dependent formal specifications at inference time without touching the weights.

Problem: Foundation models lack formal temporal guarantees
    |
    v
Assumption: Forward dynamics can be approximated over a finite horizon
    |
    v
Method: At each step, solve a constrained optimization over the action
        distribution to find the minimal perturbation satisfying STL
    |
    v
Evidence: Simulation across multiple envs + complex STL specs
    |
    v
Conclusion: Hard STL constraints can be enforced at runtime
             without retraining the base model

The Increment

One sentence: Before this paper, you had to choose between a capable foundation model and formal safety guarantees — after it, you can have both, at inference time, with no retraining.

Core Mechanism

The framework sits as a thin layer on top of a pretrained robotics foundation model. At each timestep, the base model produces its usual action distribution — a probability distribution over possible next actions. Instead of sampling directly from this, the framework intercepts it.

The key operation is a constrained optimization. The framework takes the current state, the remaining time horizon, and the STL specification. It rolls out the forward dynamics — essentially simulating “if I take actions drawn from this distribution, where do I end up?” — over the remaining horizon. It then checks whether the STL formula is satisfiable given those projected trajectories. If the base model’s distribution already satisfies the constraint, great sample from it. If not, find the closest distribution (in KL-divergence or similar sense) that does satisfy the STL feasibility constraint, and sample from that instead.

The STL feasibility constraint is the hard part. STL (Signal Temporal Logic) lets you write specs like “reach goal A within10 steps, then reach goal B within 20 steps, and never enter the obstacle region.” The framework converts this into a constraint on the action distribution by propagating the dynamics forward and checking the robustness value of the STL formula — a real-valued measure of how well a trajectory satisfies the spec. The optimization finds the minimal distribution shift that keeps this robustness non-negative.

Base Model
    |
    v
[Action Distribution p(a|s,lang)]
    |
    v
+----------------------------------------+
| Specification-Aware Optimizer             |
|                                           |
|  STL spec + current state + horizon       |
|                                    |
|      v                                    |
|  Forward dynamics rollout                |
|  (simulate trajectories under p)          |
|                                    |
|      v                                    |
|  STL robustness check                     |
|  feasible? --yes-> pass through p        |
|      |                                    |
|      no                   |
|      v                    |
|  Solve: min KL(q||p) s.t. STL(q) >= 0    |
|      |                                    |
|      v                                    |
|  Modified distribution q*(a|s)            |
+------------------------------------------+
    |
    v
Sample action -> execute

Think of it like a GPS with a co-pilot. The foundation model is your driver — experienced, capable, handles most situations. The STL optimizer is the co-pilot with a rulebook. Most of the time the co-pilot says nothing and the driver does their thing. But when the driver is about to miss a required checkpoint or wander into a restricted zone, the co-pilot doesn’t grab the wheel and drive for them — they nudge the steering just enough to stay on the legal route. The driver’s style is preserved; only the trajectory is corrected. The rulebook (STL) is expressive enough to say things like “you must pass checkpoint A before checkpoint B, and you can never enter the school zone between8am and 3pm.” The co-pilot reasons ahead — “if we keep going this way, we’ll miss checkpoint A” — and adjusts early, not at the last second.

Key Concepts

• Signal Temporal Logic (STL): A formal language for writing time-dependent rules over continuous signals. Instead of just “avoid obstacles,” you can say “reach the goal within 15 seconds AND always stay 0.5m from walls AND if you enter zone X, leave within 3 seconds.” Each formula has a robustness value — a real number that tells you not just whether the rule is satisfied, but by how much. Positive robustness = satisfied with margin. Zero = barely satisfied. Negative = violated. This real-valued property is what makes STL amenable to gradient-based optimization.

• Distribution shaping vs. action filtering: A naive safe approach would be to just reject any action that looks unsafe and resample. That’s action filtering — it’s myopic (only looks one step ahead) and can get stuck. Distribution shaping is different: you modify the entire probability distribution over actions so that the expected future trajectory satisfies the spec. It’s proactive rather than reactive, and it reasons over the full remaining horizon.

• Forward dynamics propagation: To check whether a distribution satisfies an STL spec, you need to know where the robot will end up. The framework uses the robot’s dynamics model to simulate forward — “if I sample actions from this distribution for the next N steps, what’s the distribution over future states?” This is the bridge between the action space and the temporal logic constraint. The quality of this propagation is a key assumption: if your dynamics model is wrong, your STL satisfaction guarantees weaken.

Framework Shift

Before (mainstream approach):        After (this paper):

  Train model with safety in mind      Pretrain model freely
         |                                    |
         v                                    v
  Hope specs are covered by data       Freeze model weights
         |                                    |
         v                                    v
  Deploy, cross fingers                At runtime: intercept
         |                             action distribution
  OR                                          |
         v                                    v
  Retrain with constrained RL          Solve STL-constrained
  (expensive, spec must be known       optimization over
   at train time)                      distribution
         |                                |
         v                                    v
  New spec? Retrain again.             New spec? Just swap
                       the STL formula.
                              |
                                              v
                       Execute with guarantees

From reactivetraining to runtime constraint injection, the core shift is: specs become a runtime parameter, not a training-time commitment.

Expert Assessment

Problem choice: This is a real gap, not a manufactured one. The tension between neural foundation models and formal guarantees is one of the central unsolved problems in robot learning right now. The paper is well-positioned — it’s not trying to solve all of safeRL, just the specific slice of “I have a frozen model, I have a spec, make it work.” That’s a tractable and practically relevant framing.

Method maturity: The core idea — constrained optimization over the action distribution at inference time — is clean and principled. It’s not brute force. The use of STL robustness as a differentiable constraint is a well-established trick borrowed from the formal methods community, and the authors apply it sensibly. That said, the forward dynamics propagation is a significant assumption. If the dynamics model is approximate (which it always is in practice), the guarantees degrade. The paper could be more upfront about how sensitive the method is to dynamics model error.

Experimental integrity: Simulation-only is the obvious limitation, and the authors acknowledge it. The choice of environments and STL specs seems reasonable for a first paper, but the baselines are thin — it’s mostly “base model without our wrapper” rather than comparison against other runtime safety methods (e.g., control barrier functions, shield synthesis). That makes it hard to know if this is the best way to solve the problem or just a working way.

Writing quality: The related work section is where the paper loses most altitude. It lists prior work without clearly articulating why each approach fails on this specific problem. A reader unfamiliar with the STL literature will struggle to understand why you can’t just use a CBF here. Rewriting that section with sharper contrast would make the contribution feel more inevitable and less incremental.

Verdict: weak accept — solid idea with clean execution, but the experimental comparison is too thin to fully trust the claims, and the dynamics model sensitivity deserves more honest treatment.

Takeaways

The most transferable idea here is the “distribution shaping as a runtime constraint layer” pattern. If you’re working with any pretrained generative model that needs to satisfy hard constraints at deployment time — not just robotics, but code generation with correctness specs, or language models with regulatory constraints — this framing is worth stealing. The specific machinery (STL robustness + KL-constrained optimization) is modular enough to swap in different constraint languages.

The second concrete takeaway: STL robustness as a differentiable objective is underused outside the formal methods community. If you have time-dependent constraints in any sequential decision problem, expressing them as STL and using the robustness value as a loss term or constraint is a practical technique that doesn’t require deep expertise in formal verification.

One honest caveat: the dynamics propagation assumption is load-bearing. Before applying this in a new domain, ask yourself how good your forward model is. If it’s poor, the “hard guarantees” soften into “soft suggestions,” and you’d be better off with a simpler approach.