Organizations: School of Advanced Manufacturing and Robotics, Peking University, Beijing 100871, China. · School of Integrated Circuits, Peking University, Beijing 100871, China.
Many robotic tasks are temporally extended and demand precise specifications of subgoals, constraints, and their temporal ordering. Yet human operators typically communicate such tasks in natural language, which is inherently ambiguous, underspecified, and context dependent. Translating human instructions into formal task specifications, such as Linear Temporal Logic (LTL), is therefore essential for verifiable and safe robotic execution. Existing LLM-based translators attempt to bridge this gap through open-ended reasoning or post-hoc constraint enforcement, but the former may violate domain constraints, whereas the latter can disrupt the reasoning needed for novel instructions. This paper proposes Self-Constrained Reasoning (SCR), a framework that mitigates this trade-off by internalizing structural knowledge into the model's decision-making process rather than imposing it as an external filter. By combining a structural constraint representation with a hierarchical decision-making formulation, SCR guides reasoning within a formally grounded space while preserving adaptability to unseen instructions. Experiments show that SCR improves both domain-constraint satisfaction and generalization, providing an effective and interpretable approach for translating human intent into verifiable specifications for robotic execution.
Figures & tables
Figure 1: Challenges and methodologies in linear temporal logic translation. (A) A demonstration of translating a natural language instruction into a formal ltl expression to guide autonomous systems. (B) Challenges in ltl translation: domain constraints and generalization. (C) Comparative performance and pitfalls of two mainstream methods for existing challenges. Experiments demonstrate that while constraint-based methods improve adherence to domain constraints, they often fail to generate proper reasoning, leading to a decrease in the model’s generalization ability. Conversely, reasoning-based methods enhance generalization capabilities but tend to overlook specific domain constraints during the process. (D) Our approach effectively balances domain-specific constraints with generalization capabilities, demonstrating robust performance even when presented with novel and increasingly complex task specifications. Furthermore, the method ensures strict adherence to grammatical rules to guarantee executability, while enforcing textual alignment between the output and human intent.
Figure 2: Overview of the proposed framework. The pipeline extracts an ltl - scfg from parallel corpora (top) and utilizes it to constrain the rl agent’s action space during hierarchical translation (bottom).
Figure 3: Extracted ltl - scfg rules across domains. The tables display the mapping between formal ltl operators ( e.g. , F,G,¬ ) and their lexical realizations in different datasets.
Figure 4: Recursive translation showcases. The diagrams illustrate the step-by-step derivation for CleanUp (top) and Drone (bottom) tasks. The agent recursively selects operators (red blocks) and decomposes the nl instruction, yielding a structured and interpretable translation trace.
Table 4: Safety violation comparison across different models and tasks using pf ( pf ), ua ( ua ), and overall sv ( sv ) metrics (%).
Figure 5: Human evaluation and multi-dimensional interpretability analysis. The top row displays boxplots of evaluation scores across the Drone, Cleanup, and Pick domains, along with the Overall performance; red stars indicate mean values. The bottom row presents radar charts comparing our framework against baselines across six qualitative metrics: Comprehensibility, Trust, Transparency, Fidelity, Interactivity, and Decision-support.
Figure 6: Illustration of application experiment environments. (A) The room cleaning environment features a rectangular wood-grain floor divided into four semantic rooms, each labeled by its color. A red room marks the upper-left corner, a yellow room the lower-left, a green room the middle-right, and a blue room the bottom-center. These colored rooms serve as coordinate waypoints for robot navigation. (B) The cargo delivery environment is set in an outdoor pedestrian area bordered by greenery. The layout includes several key coordinates: starting point I on the right, and waypoint J (labeled Landmark 1, {L1} ) marked by a rectangular stone pedestal in the upper-left. Landmark 2 ( {L2} ) is located at point M on the left lawn’s edge, with an additional waypoint K near the bottom. To reach M from I, the agent must pass through either J or K. (C) The manipulation environment features a gray metallic tabletop with a white rectangular storage basket in the upper-right. Scattered across the table are several objects labeled by color: two red fruits (Apple and Tomato), one yellow Pear, and two green fruits (Avocado and Cucumber). (D) The household environment features a kitchen countertop setup with a microwave on the left and a piece of salmon placed on top. The environment involves the following object states: the salmon can be in either a cold or hot state ( { , } ), while the microwave can be toggled between an active or inactive status ( { , } ).
Figure 7: Translation and execution experiments for the robot room cleaning task. (A) Upon receiving the natural language instruction S , the algorithm translates it into an ltl formula. Subsequently, a verification automaton and a system automaton are constructed, and a feasible execution path (indicated by the blue shaded path) is identified by computing their synchronous product. (B) The sequence illustrates the robot’s execution trajectory from t=0 s to t=9.3 s. Following the trajectory plan, the robot first enters the blue room ( t=3.0 s) and then proceeds to the final objective, the green room ( t=9.3 s), verifying the effectiveness of the algorithm in handling logical instructions and motion planning.
Figure 8: Translation and execution experiments for the robot cargo delivery task. (A) The system translates the natural language instruction S into an ltl formula. By constructing a verification automaton and a system automaton, a feasible execution plan Iq0→Kq0→Mq1 is identified within the synchronous product (highlighted by the blue shaded path), which strategically bypasses the forbidden waypoint J ( L1 ). (B) The sequence frames illustrate the humanoid robot’s real-world trajectory from t=0 s to t=30.0 s. To satisfy the safety constraint G¬L1 , the robot selects the path through waypoint K ( t=15.0 s) and successfully arrives at landmark L2 at point M ( t=30.0 s), demonstrating the algorithm’s precision in extracting logical constraints and planning safe motion.
Figure 9: Translation and execution experiments for the manipulation task. (A) The system translates the natural language instruction S into the ltl formula φ3 . The synchronous product P is obtained from the verification automaton Aφ3 and the labeled fts T . Only the key segments of the system automaton and the synchronous product are illustrated; opaque states within the system automaton denote that those states are unobserved ( i.e. , without s flag). A feasible execution strategy is identified within the product (highlighted by the blue shaded path), which guides the robot to sequentially interact with non-red objects while satisfying the logical constraints. (B) The trajectory plan and sequence frames illustrate the robotic arm’s real-world execution from t=0 s to t=83.4 s. The robot selectively picks the avocado ( t=20.4 s), pear ( t=35.7 s), and cucumber ( t=61.9 s), successfully reaching the accepting state q2 and completing the task while leaving the red fruits untouched.
Figure 10: Translation and execution experiments for the household task. (A) The system translates the natural language instruction S into an ltl formula. By constructing a verification automaton and a system automaton that model the object states, a feasible execution plan s0,q0→s1,q1→s2,q2 is identified within the synchronous product (highlighted by the blue shaded path). This plan guides the agent to successfully heat the food while ensuring the appliance is properly shut off. (B) The sequence frames illustrate the virtual agent’s execution trajectory from t=0 s to t=8.33 s. Following the generated plan, the agent opens the microwave to insert the salmon ( t=2.23 s), activates it to warm the food ( t=3.40 s), and ultimately deactivates and closes the microwave ( t=8.33 s). This sequence successfully reaches the accepting state q2 , demonstrating the algorithm’s effectiveness in managing interactions within new action spaces.
Translating natural language instructions into machine-interpretable formal specifications enables robots and autonomous systems to plan, reason, and formally verify their behavior. However, existing translation models typically generate a specification for every input, even when the result is unreliable or fails to capture the user's intent, creating risks in safety-critical applications. Inspired by selective conformal prediction, we propose a selective translation framework that not only generates formal specifications but also determines when they can be trusted. Reliability is scored by two complementary black-box signals, the fidelity of the specification back-translated into natural language and the dispersion of repeated translations under exact semantic equivalence, which fail on different errors and jointly separate incorrect translations more sharply than either alone. Conformal risk control calibrates this score into a decision that accepts a specification or abstains, with a distribution-free bound on the rate at which incorrect specifications are accepted for execution, and a conformal anomaly detector on instruction embeddings screens out-of-distribution inputs before any translation is attempted. The proposed framework is general across formal specification languages, with experiments on Signal Temporal Logic (STL), Linear Temporal Logic (LTL), and geometric Spatio-Temporal Logic (SpaTiaL) demonstrating improved translation reliability, robustness under the evaluated cross-tier shifts, and effective uncertainty-aware abstention. This work establishes a foundation for trustworthy natural language interfaces by enabling AI systems to recognize when generated specifications may not be reliable.
Yixuan Wang, Licheng Luo, Yu Fu +3
University of California, Riverside, Riverside, CA, USA · City University of Hong Kong, Hong Kong SAR, China
Natural-language robot instructions often specify more than a coarse task goal: they may impose spatial, temporal, and logical requirements that must remain satisfied throughout execution. We present STeP, a specification-based agentic framework that uses Signal Temporal Logic (STL) as an explicit interface between high-level language reasoning and low-level robot execution. Rather than encoding such requirements implicitly in a learned policy, STeP formalizes them as task specifications that can be decomposed across multi-stage manipulation, enforced during execution, monitored online, and used as structured feedback for replanning. We evaluate STeP on standard LIBERO and LIBERO-PRO, and introduce LIBERO-Constrained, a new benchmark for manipulation tasks with spatial, temporal, and logical requirements, together with real-world tabletop experiments. On LIBERO-PRO, STeP retains 54%-89% success across five of six evaluated perturbation settings, substantially outperforming VLA and code-as-policy baselines under distribution shift. On LIBERO-Constrained, STeP achieves 80% safe success across 49 task-constraint instances; on real-world tasks, it improves safe success over a specification-free model-based baseline across all four task categories, with gains of up to 45 percentage points. These results support explicit formal specifications as a practical interface between foundation-model reasoning and reliable robot execution.
Executing Linear Temporal Logic (LTL) instructions with learned robot policies faces two practical challenges: demonstrations may cover individual behaviors without containing the temporal compositions requested at deployment, and semantic success predicates often provide little useful motor guidance through quantitative robustness. We address these challenges by separating behavior learning from temporal composition. From the same offline demonstrations, we train an unconditioned multimodal diffusion policy and a semantic predictor that estimates which semantic outcomes are likely to follow a proposed action sequence. These predictions provide a learned guidance signal without requiring hand-designed robustness measures for semantic task objectives. At deployment, an LTL automaton tracks instruction progress and scores the policy's proposed actions according to their predicted semantic outcomes. Neither learned component receives the specification during training, allowing demonstrated behaviors to be reused in longer, previously unseen temporal compositions without retraining. For additional runtime safety constraints with informative continuous margins, an optional robustness-based controller locally refines the selected actions. Experiments in a navigation environment, CALVIN manipulation, and on a real robot demonstrate reliable execution of complex temporal instructions and additional safety constraints, with substantial improvements over temporal-logic baselines.
Moritz Zoellner, Anastasios Manganaris, Ahmed H. Qureshi +1