Paper deep dive
From LLM-Generated Specifications to Learned Quadruped Locomotion
Merve Atasever, Keyan Azbijari, Cagan Bakirci, Alfredo Reina Corona, Tolga Izdas, Richard Yang, Erdem Biyik, Jyotirmoy V. Deshmukh
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 9/13/2026, 4:46:15 AM
Summary
This paper proposes a pipeline where Large Language Models (LLMs) generate Parametric Signal Temporal Logic (PSTL) specifications for quadruped robot locomotion, which are then instantiated using expert trajectories and used to train reinforcement learning policies. The study compares GPT-5.5 and Qwen 3.6 in both gait-aware and gait-agnostic settings, demonstrating that LLM-generated STL specifications can outperform hand-engineered rewards and direct LLM-generated reward code (Text2Reward), particularly in high-speed regimes.
Entities (11)
Relation Signals (7)
Qwen 3.6 → achieves → 100% survival
confidence 96% · Gait-aware Qwen 3.6 specifications achieved 100% survival and command success across all tested speeds
GPT-5.5 → generates → PSTL specifications
confidence 95% · GPT-5.5 and Qwen 3.6 independently propose STL templates
Qwen 3.6 → generates → PSTL specifications
confidence 95% · GPT-5.5 and Qwen 3.6 independently propose STL templates
Expert Trajectories → usedtoinstantiate → PSTL parameters
confidence 94% · We instantiate the parameters of the generated PSTL templates using expert trajectories
PSTL specifications → usedtotrain → Quadruped locomotion policy
confidence 93% · specifications that are subsequently used for policy learning
PSTL specifications → convertedto → Reward functions
confidence 92% · The resulting specifications are then transformed into smooth, finite-history reward functions
Text2Reward → outperformedby → Qwen 3.6
confidence 90% · Text2Reward achieved 0% for both metrics at ≥1.9 m/s
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Quadruped robot locomotion policies are often trained using reinforcement learning, which in turn relies heavily on hand-crafted reward functions. Designing reward functions requires substantial manual engineering, and it is often unclear which local rewards will induce the desired global behavior. Shaped rewards from formal specifications in languages like Signal Temporal Logic (STL) can make rewards more interpretable, but writing STL specifications itself still requires domain expertise. We study whether large language models (LLMs) can fill this gap by generating Parametric Signal Temporal Logic (PSTL) specifications that are subsequently used for policy learning. Given a natural language locomotion objective and a constrained specification grammar, GPT-5.5 and Qwen 3.6 independently propose STL templates for command tracking, safety, and gait structure. We instantiate the parameters of the generated PSTL templates using expert trajectories and retain only specifications that are consistent with demonstrated expert behavior. The resulting specifications are then transformed into smooth, finite-history reward functions and used to train a quadruped locomotion policy with Proximal Policy Optimization (PPO) in MuJoCo XLA (MJX). We evaluate both \emph{gait-aware} and \emph{gait-agnostic} settings. The former specifies walking-trot, trot, and bound regimes, while the latter allows contact patterns to emerge from the task objective. We compare against hand-engineered rewards, Text2Reward-style LLM-generated reward code, and an expert-switching oracle. Gait-aware Qwen 3.6 specifications achieved 100\% survival and command success across all tested speeds (0.3--2.1 m/s) and matched the target gait at high speeds, whereas Text2Reward achieved 0\% for both metrics at $\geq 1.9$ m/s. Videos: this https URL
Tags
Links
- Source: https://arxiv.org/abs/2609.07111v1
- Canonical: https://arxiv.org/abs/2609.07111v1
Trouble viewing inline? Open PDF directly →
Full Text
42,655 characters extracted from source content.
Expand or collapse full text
From LLM-Generated Specifications to Learned Quadruped Locomotion Merve Atasever1, Keyan Azbijari1, Cagan Bakirci1, Alfredo Reina Corona1, Tolga Izdas1, Richard Yang2, Erdem Biyik1, Jyotirmoy V. Deshmukh1 Affiliation: Affiliation: 1Department of Computer Science University of Southern California Los Angeles, CA, USA atasever, azbijari, cbakirci, reinacor, izdas, biyik, jdeshmuk@usc.edu Affiliation: Affiliation: 2University of Florida Gainesville, FL, USA yangrichard@ufl.edu Abstract Quadruped robot locomotion policies are often trained using reinforcement learning, which in turn relies heavily on hand-crafted reward functions. Designing reward functions requires substantial manual engineering, and it is often unclear which local rewards will induce the desired global behavior. Shaped rewards from formal specifications in languages like Signal Temporal Logic (STL) can make rewards more interpretable, but writing STL specifications itself still requires domain expertise. We study whether large language models (LLMs) can fill this gap by generating Parametric Signal Temporal Logic (PSTL) specifications that are subsequently used for policy learning. Given a natural language locomotion objective and a constrained specification grammar, GPT-5.5 and Qwen 3.6 independently propose STL templates for command tracking, safety, and gait structure. We instantiate the parameters of the generated PSTL templates using expert trajectories and retain only specifications that are consistent with demonstrated expert behavior. The resulting specifications are then transformed into smooth, finite-history reward functions and used to train a quadruped locomotion policy with Proximal Policy Optimization (PPO) in MuJoCo XLA (MJX). We evaluate both gait-aware and gait-agnostic settings. The former specifies walking-trot, trot, and bound regimes, while the latter allows contact patterns to emerge from the task objective. We compare against hand-engineered rewards, Text2Reward-style LLM-generated reward code, and an expert-switching oracle. Gait-aware Qwen 3.6 specifications achieved 100% survival and command success across all tested speeds (0.3–2.1 m/s) and matched the target gait at high speeds, whereas Text2Reward achieved 0% for both metrics at ≥1.9≥ 1.9 m/s. Videos: https://stl-locomotion.github.io/ Index Terms: quadrupedal locomotion, reinforcement learning, signal temporal logic, large language models, reward design I Introduction Deep RL has enabled quadruped robots to learn agile locomotion from simulations and expert demonstrations, but performance still depends strongly on reward engineering [1, 2, 3, 4, 5, 6, 7]. A typical locomotion reward is a weighted sum of instantaneous tracking, posture, smoothness, contact, and energy terms. Although such rewards can produce performant policies, selecting various reward components and coefficients requires substantial domain knowledge and empirical tuning, with design choices often justified through ablations rather than first principles [8, 4, 9]. Moreover, the resulting numerical, local rewards do not explicitly describe the global temporal behavior it is intended to induce. This is especially problematic for multi-gait locomotion: walking, trotting, and bounding differ not only in speed, but also in contact timing and support patterns. Alternatives such as inverse RL and preference-based RL reduce reliance on manually specified rewards by inferring objectives from demonstrations or human feedback, but introduce an additional reward-learning or optimization stage [10, 11, 12, 13, 14, 15]. Our approach also uses expert trajectories, but only to calibrate and validate an explicit set of symbolic, global specifications whose structure is proposed by an LLM. Another approach is to describe desired behavior explicitly using formal logic and convert specification-satisfaction into a learning signal. Prior work on logic-guided RL has leveraged Linear Temporal Logic (LTL) and Signal Temporal Logic (STL) for reward shaping and policy learning, while also exploring the inference of temporal-logic specifications from demonstrations, particularly in navigation and manipulation tasks. [16, 17, 18, 19, 20, 21]. Formal specifications have similarly been incorporated into planning and control for legged robots, including locomotion over cluttered terrain, stability constraints, and STL-informed control for bipedal walking and push recovery [22, 23, 24, 25, 26]. For quadrupeds, however, comparable continuous temporal-logic formulations remain limited. Existing logic-driven gait-learning approaches largely employ discrete logical rules or reward machines defined over foot-contact propositions and operating primarily on contact-level logic and step-wise signals [27, 28]. Signal Temporal Logic or STL [29] is well suited to this problem because it expresses bounded time-horizon properties directly over real-valued trajectories and associates each specification with a quantitative robustness value measuring its margin of satisfaction or violation [30, 31]. These quantitative semantics makes it possible to use STL not merely as a post hoc verifier, but as a dense reward signal for RL [17, 32, 33, 19]. Unlike conventional rewards, an STL specification can explicitly encode temporal relationships such as how long a condition should persist, how events should be ordered, or how contact patterns should evolve over a finite horizon. In our previous work, we manually defined parametric STL templates for quadruped safety, command tracking, and gait behavior and calibrated their numerical thresholds from expert rollouts [34]. While this formulation improves interpretability and gait control relative to heuristic rewards, it leaves the burden of manual specification design unresolved. Recent LLM-based reward-design methods address a closely related problem by generating executable dense reward functions directly from natural-language task descriptions [35, 36]. In parallel, language models have increasingly been used to translate natural language requirements into temporal logic representations [37]. We combine these ideas differently. Instead of asking an LLM to produce the numerical reward itself, we ask it to propose a symbolic temporal specification. Expert trajectories are then used to fit the specification parameters and reject candidates that disagree with demonstrated behavior. The retained specifications are subsequently converted into dense learning signals through STL robustness. We investigate this design using Google’s Barkour quadruped. GPT-5.5 and Qwen 3.6 are prompted with the same locomotion objective and STL grammar, but are not provided numerical thresholds [38, 39]. Each model proposes Parametric STL (PSTL) specifications. We fit the values of these parameters from expert trajectories and retain only specifications that are consistent with those trajectories. During policy learning, we compute smooth trailing-window STL robustness online and use it as a PPO reward [40, 41]. We evaluate the approach in both gait-aware (multi-gait) locomotion, where speed regimes activate gait-specific specifications, and gait-agnostic locomotion, where no gait is prescribed and the robot is free to discover its own contact pattern. Contributions. 1. We introduce a pipeline in which LLMs generate the structure of interpretable locomotion specifications while expert data grounds their numerical parameters. 2. We propose a simple expert-consistency filter: a generated specification is discarded when its median robustness on expert data is negative, preventing systematically violated LLM suggestions from entering the reward. 3. We evaluate both gait-aware and gait-agnostic formulations to study how explicitly prescribing gait structure affects the learned locomotion behavior. 4. We benchmark against a heuristic reward, Text2Reward, and an expert-switching oracle. Fig. 1: Barkour vb robot in MJX. I Background and Problem Setting We consider Barkour vb in MJX [6, 42, 7]. At each control step (Δt=0.02 t=0.02 s), the policy receives commanded linear and angular velocities (vxcmd,vycmd,ωzcmd)(v_x^cmd,v_y^cmd, _z^cmd), proprioceptive observations, the previous action, and a short observation history, and outputs 12 normalized joint-position commands. A PD controller maps these commands to actuator torques. The goal is to learn a policy πθ(at∣ot) _θ(a_t o_t) that tracks commands while remaining stable and energy efficient. An STL predicate has the form f(x(t))≥0f(x(t))≥ 0. Boolean operators combine predicates and temporal operators [a,b]G_[a,b] and [a,b]F_[a,b] respectively constrain predicate satisfaction to be globally true over the time interval [a,b][a,b] or true at some point during the interval. Quantitative semantics assign a robustness ρφ(x,t)∈ℝρ (x,t) to formula φ : positive values indicate satisfaction, and negative values indicate violation [30, 31]. Parametric STL (PSTL) replaces numerical constants in predicates or temporal intervals by parameters that can be fit from data [43]. We evaluate each temporal specification over the trailing window t=[t−H,t]W_t=[t-H,t], and the resulting specification-level robustness values are subsequently combined using the smooth aggregation described in the next section [44]. I LLM-Generated STL Reward Pipeline I-A Specification Generation The LLM receives (i) a natural-language description of Barkour locomotion and (i) an allowed STL grammar. We explicitly ask for template structure only: thresholds and temporal constants remain symbolic so that they can be estimated from expert data rather than invented by the language model. GPT-5.5 and Qwen 3.6 are queried independently with the same prompt. For the multi-gait setting, the prompt describes three forward-speed regimes: walking-trot (0≤vxcmd≤0.70≤ v_x^cmd≤ 0.7 m/s), trot (0.7<vxcmd≤1.70.7<v_x^cmd≤ 1.7 m/s), and bound (vxcmd>1.7v_x^cmd>1.7 m/s). Generated formulas can refer to shared tracking/safety signals and regime-specific contact statistics. Typical template families include examples shown below11 1 Complete sets of generated specifications and prompts are available on the project website: https://stl-locomotion.github.io/. Let the trailing evaluation window at time t be defined as t=t−H,…,t,W_t=\t-H,…,t\, (1) where H denotes the robustness horizon. For an STL formula of the form μG_Wμ, where μ is a predicate, the robustness at time t is computed as ρμ(t)=mink∈tρμ(k).ρ^G_Wμ(t)= _k _tρ^μ(k). (2) Thus, the robustness is determined by the worst predicate margin observed within the trailing temporal window. Example 1. Torque limits: For Barkour vb, the actuators provide a peak output torque of 1818 Nm (τmaxτ ) at each joint, hence motor torque limits must be bounded by this limit [6]. φτ=(⋀j=112|τj|≤τmax). _τ=G_W ( _j=1^12| _j|≤τ ). (3) The corresponding robustness is ρτ(t)=mink∈tminj∈1,…,12(τmax−|τj(k)|). _τ(t)= _k _t _j∈\1,…,12\ (τ -| _j(k)| ). (4) Example 2. Torso orientation: Roll and pitch are constrained using φϕ _φ =(|ϕ|≤ϕmax), =G_W (|φ|≤ _ ), (5) φθ _θ =(|θ|≤θmax). =G_W (|θ|≤ _ ). (6) Example 3. Center-of-mass (CoM) height: A minimum center-of-mass height is specified as φz=(zcom≥zmin). _z=G_W (z_com≥ z_ ). (7) Example 4. Support contacts: To require a minimum number of feet in contact with the ground, we use φc=(nc≥nmin), _c=G_W (n_c≥ n_ ), (8) where ncn_c denotes the number of active foot contacts. Example 5. Linear velocity tracking: For each commanded linear velocity component i∈x,yi∈\x,y\, tracking is specified as φvi=(|vi−vicmd|≤ϵv,i). _v_i=G_W (|v_i-v_i^cmd|≤ _v,i ). (9) The numerical parameters ϕmax _ , θmax _ , zminz_ , nminn_ , and ϵv,i _v,i are not generated by the LLM. The LLM determines only the symbolic structure of each STL specification, while the numerical parameters are subsequently estimated from expert trajectories. The resulting specification-level robustness values are then aggregated to construct the reward used for PPO training. Multi-Gait vs Gait-Agnostic Policies Using the same gait for low speed and high speed motion may be inefficient or infeasible for quadrupeds [45, 46]. To determine transition velocity thresholds between speed regimes, we leverage the Froude number which is used to characterize gait transition speeds of different-sized quadrupeds: Fr=v2gh,Fr= v^2gh, where Fr is the Froude number, v is the linear velocity of the robot’s torso, g is the acceleration due to gravity, and h is the maximum leg length [47]. Building on bio-inspired robotics gait design methodologies and reported gait structures that Barkour vb achieved to succeed, we leverage three speed regimes (modes): walking-trot, trot, and bound, selected based on commanded forward velocity |vxcmd(t)||v_x^cmd(t)|. Using the Barkour robot’s leg length of 0.41m0.41~m and the reference Froude numbers of 0.150.15 and 0.740.74 [48], we establish the respective gait transition velocity thresholds at 0.7m/s0.7~m/s and 1.7m/s1.7~m/s. Here, diagonal legs move together for mid-speed regime (trot), whereas forelegs make contact approximately in phase, followed by the hind legs to achieve high speeds (bound). While the multi-gait setting aims to learn a single policy that adapts its gait structure across speed regimes (walking-trot → trot → bound), the gait-agnostic setting does not enforce any target gait. We therefore use separate prompts for the two settings. I-B Robustness Reward For active retained specifications, we aggregate multiple robustness terms using the soft-min sminβsp(z1,…,zK):=∑k=1Kπkzksmin^sp_β(z_1,…,z_K):= _k=1^K _kz_k, where πk=e−βzk∑j=1Ke−βzj. _k= e^-β z_k _j=1^Ke^-β z_j. For the final reward shaping, each grouped robustness is normalized as tanh(μ) (μ) to map to a value in [−1,1][-1,1], preventing large robustness magnitudes from dominating the reward. The final scalar reward is: rt=wsafetanh(μsa)+wtracktanh(μtr)+wpatterntanh(μpa)r_t=w_safe\, ( _sa)+w_track\, ( _tr)+w_pattern\, ( _pa) (10) This decomposition makes the generated reward inspectable: during an evaluation we can report both the scalar RL reward and the robustness of each retained formula. I-C Data Grounding and Expert-Consistency Filtering We collect 50 expert trajectories per regime, each containing 500500 time steps, and compute the signals required by every generated template. Numerical parameters for PSTL templates are estimated from expert data statistics using quantiles appropriate to the predicate direction: upper quantiles for error ceilings and lower quantiles for safety floors. Moreover, LLMs can propose technically sound but incompatible or overly strict requirements. We take advantage of expert trajectories to filter these specifications. Let Rφ=ρφ(x(i),t)|i=1,…,50,t∈iR_ = \ρ (x^(i),t)\; |\;i=1,…,50,\;t _i \ (11) denote the set of robustness values obtained for specification φ across all expert trajectories and valid evaluation times. We retain φiffQ0.50(Rφ)≥0, Q_0.50(R_ )≥ 0, (12) i.e., the specification is removed if its median robustness is negative. Equivalently, a formula that is violated on more than half of the expert evaluation points is not used for reward construction. We refer to this step as expert-consistency filtering. Fig. 2: Overall Pipeline. IV Experimental Design IV-A Training and Baselines All learned policies use the same Barkour MJX environment, policy architecture, PPO implementation, command distribution, and domain-randomization scheme; only the reward source changes. We use friction randomization in [0.6,1.4][0.6,1.4] and actuator gain perturbations, following the existing training setup. During training, a new velocity command is randomly sampled every 10 s. The initial command range is set to vycmd∈[−0.2, 0.2]m/sv_y^cmd∈[-0.2,\,0.2]\,m/s, ωcmd∈[−0.2, 0.2]rad/sω^cmd∈[-0.2,\,0.2]\,rad/s, and the forward-velocity range is gradually expanded to vxcmd∈[0.0, 1.9]m/sv_x^cmd∈[0.0,\,1.9]\,m/s as part of the curriculum for learning the locomotion at higher speeds. Details of the training procedure and domain randomization are provided in the GitHub repository. We compare the following methods: (1) Heuristic-reward uses the standard hand-engineered locomotion reward in the original Barkour paper [6], (2) human-STL is the manually structured STL reward from the previous work and serves as an ablation for whether the LLM can replace manual specification design, (3 & 4) GPT-STL and Qwen-STL are each trained from the specifications generated by the corresponding LLM, (5) Text2Reward adapts direct LLM-generated reward code [35] (implemented using GPT-5.5 as the underlying language model), (6) Expert-switching oracle selects the corresponding specialized expert for the ground-truth commanded speed regime. It is not a learned unified controller and is reported as an oracle reference rather than a directly comparable training method. IV-B Evaluation We evaluate forward commands vxcmd∈0.3,0.5,0.7,1.0,1.3,1.6,1.9,2.0,2.1v_x^cmd∈\0.3,0.5,0.7,1.0,\\ 1.3,1.6,1.9,2.0,2.1\ m/s with zero lateral/yaw command, using 20 rollouts of 500 steps per command and excluding the first 50 steps for tracking metrics. We leverage four evaluation metrics: cost of transportation (CoT), survival rate, success rate, and gait match. We measure energy efficiency using cost of transportation Emgd Em\,g\,d where E is the total energy consumed, m is the robot mass, g is gravitational acceleration, and d is the planar distance traveled during the rollout. For episodes where the robot fails to survive, this metric is computed only up to the timestep of early termination. Lower CoT indicates better transport efficiency. A rollout is counted as survived if the robot does not terminate early due to falling or violating the environment termination conditions. We define success based on velocity tracking accuracy after the warm-up phase. Let vxcmdv_x^cmd be the commanded forward velocity, and let vxloc(t)v_x^loc(t) denote the robot’s forward velocity in its local body frame. The average post-warm-up forward speed for rollout k is v¯x(k)=1T−50∑t=51Tvxloc,k(t). v_x^(k)= 1T-50 _t=51^Tv_x^loc,k(t). A rollout is considered successful if |v¯x(k)−vxcmd|≤0.15|vxcmd|, | v_x^(k)-v_x^cmd |≤ 0.15\,|v_x^cmd|, i.e., the average forward speed stays within ±15%± 15\% of the commanded velocity. Gait match is a qualitative label based on the dominant contact pattern: Success denotes a dominant pattern matching the prescribed gait, Partial denotes intermittent matching, and Fail denotes a different dominant pattern. For each LLM, robustness horizon H is selected using validation performance from 1,5,10,20,30\1,5,10,20,30\. V Results and Discussion Table I shows that GPT-GA and Text2Reward-GA (GA denotes gait-agnostic) achieve the strongest quantitative performance in the gait-agnostic setting. They maintain command success and survival across the full evaluated velocity range while yielding the lowest cost of transport (CoT) for most commands. In contrast, the heuristic-reward policy loses tracking accuracy at the two highest speeds, and Qwen-GA loses both survival and success from 1.61.6 m/s onward. Despite the strong tracking performance of GPT-GA and Text2Reward-GA, visual inspection reveals a critical discrepancy between their quantitative results and their actual locomotion quality. The policies learn a bound-like contact pattern and exploits it across the entire tested speed range. At a low commanded velocity of vxcmd=0.3v_x^cmd=0.3 m/s, the robot continues to move its legs at a high cadence, producing pronounced vertical body oscillations. While this behavior yields a 100%100\% average velocity-tracking success rate, the resulting low-speed motion is visibly unnatural and undesirable. This highlights a fundamental limitation of evaluating locomotion solely through command success: high quantitative scores do not guarantee dynamically appropriate control. (Videos of the policies are provided on the project website). This limitation underscores the value of the multi-gait formulation. When explicit gait structures are prescribed, the results in Table I exhibit a markedly different pattern. Human-STL is the most consistent overall gait-aware controller. Qwen-MG matches its command/survival performance and desired bound behavior at high speed but fails to reproduce several prescribed lower-speed gaits. GPT-MG captures the low/mid-speed target gaits better but loses command tracking at 1.9 m/s and above. Text2Reward-MG is energy-efficient where it works but fails completely at high speeds. Ultimately, these results demonstrate that no single reward formulation universally dominates across both task settings and all evaluation criteria. GPT-5.5 vs Qwen 3.6: The relative performance of the two LLM-generated specification sets depends strongly on whether gait structure is prescribed. In the gait-agnostic setting, GPT-GA is more robust at high speeds: it survives all tested commands and tracks commands accurately, while Qwen-GA terminates from 1.6,m/s1.6,m/s onward. The comparison reverses in the multi-gait setting. Qwen-MG tracks commands throughout the full 0.30.3-2.1,m/s2.1,m/s range and generally matches or improves upon GPT-MG in CoT, whereas GPT-MG fails the command-success criterion at 1.9,m/s1.9,m/s and above. Thus, the quality of an LLM-generated specification cannot be characterized independently of the control setting in which it is used. Why the Text2Reward comparison matters: Both Text2Reward and our approach begin from language-model knowledge, but the intermediate representation differs. Text2Reward directly commits to numerical executable reward code from current-step signals. Our pipeline first exposes the proposed behavior as symbolic temporal constraints, then fits thresholds from expert data. This comparison lets us ask whether exposing the LLM output as an STL specification changes the learned behavior relative to directly generating reward code. The clearest difference between STL specification generation and direct reward-code generation appears in the high-speed regime. Text2Reward-MG terminates in every rollout at 1.9, 2.0, and 2.1 m/s, whereas Qwen-MG achieves 100% survival and command success at all three commands and exhibits the desired bound contact pattern. This advantage is regime-specific: Qwen-MG does not reproduce the prescribed gait at several lower-speed commands. The comparison indicates that the STL intermediate representation can produce a more effective high-speed learning signal than the evaluated Text2Reward baseline, while also showing that successful command tracking does not guarantee recovery of all intended gait structures. TABLE I: Gait-agnostic locomotion results across commanded forward velocities. Lower CoT is better; higher survival and success are better. Each entry reports mean ± standard deviation over 20 rollouts. vxv_x (m/s) CoT ↓ Survival ↑ Success ↑ Heuristic 0.3 1.20±0.001.20± 0.00 100%100\% 100%100\% 0.5 1.00±0.001.00± 0.00 100%100\% 100%100\% 0.7 1.00±0.001.00± 0.00 100%100\% 100%100\% 1.0 1.20±0.001.20± 0.00 100%100\% 100%100\% 1.3 1.30±0.001.30± 0.00 100%100\% 100%100\% 1.6 1.40±0.001.40± 0.00 100%100\% 100%100\% 1.9 1.40±0.001.40± 0.00 100%100\% 100%100\% 2.0 1.40±0.001.40± 0.00 100%100\% 5%5\% 2.1 1.40±0.001.40± 0.00 100%100\% 0%0\% GPT-GA 0.3 1.16±0.011.16± 0.01 100%100\% 100%100\% 0.5 1.02±0.011.02± 0.01 100%100\% 100%100\% 0.7 0.99±0.010.99± 0.01 100%100\% 100%100\% 1.0 0.95±0.010.95± 0.01 100%100\% 100%100\% 1.3 0.95±0.010.95± 0.01 100%100\% 100%100\% 1.6 0.95±0.010.95± 0.01 100%100\% 100%100\% 1.9 0.94±0.010.94± 0.01 100%100\% 100%100\% 2.0 0.95±0.010.95± 0.01 100%100\% 100%100\% 2.1 0.97±0.010.97± 0.01 100%100\% 100%100\% Qwen-GA 0.3 1.39±0.021.39± 0.02 100%100\% 100%100\% 0.5 1.17±0.021.17± 0.02 100%100\% 100%100\% 0.7 1.10±0.021.10± 0.02 100%100\% 100%100\% 1.0 0.94±0.010.94± 0.01 100%100\% 100%100\% 1.3 0.96±0.010.96± 0.01 100%100\% 100%100\% 1.6 1.04±0.121.04± 0.12 0%0\% 0%0\% 1.9 1.13±0.071.13± 0.07 0%0\% 0%0\% 2.0 1.12±0.121.12± 0.12 0%0\% 0%0\% 2.1 1.19±0.121.19± 0.12 0%0\% 0%0\% Text2Reward-GA 0.3 0.91±0.010.91± 0.01 100%100\% 100%100\% 0.5 0.80±0.000.80± 0.00 100%100\% 100%100\% 0.7 0.75±0.000.75± 0.00 100%100\% 100%100\% 1.0 0.74±0.000.74± 0.00 100%100\% 100%100\% 1.3 0.79±0.000.79± 0.00 100%100\% 100%100\% 1.6 0.87±0.000.87± 0.00 100%100\% 100%100\% 1.9 1.00±0.011.00± 0.01 100%100\% 100%100\% 2.0 1.07±0.011.07± 0.01 100%100\% 100%100\% 2.1 1.14±0.011.14± 0.01 100%100\% 100%100\% Gait-aware vs gait-agnostic locomotion: The effect of explicitly prescribing gait structure is not uniform across methods. For Qwen-STL, the multi-gait formulation substantially extends the range of successful locomotion: Qwen-GA fails from 1.6,m/s1.6,m/s onward, while Qwen-MG maintains successful command tracking across the complete evaluation range. GPT-STL and Text2Reward show the opposite trend: their gait-agnostic policies succeed across the complete range, whereas the multi-gait version fails at the high-speed commands. These results suggest that adding gait-specific structure can improve high-speed locomotion, but its benefit depends on the particular reward or specification produced by the language model. Effect of robustness horizon: To understand the impact of the STL robustness evaluation horizon on policy learning, we conduct an ablation study over the window size H∈1,5,10,20,30H∈\1,5,10,20,30\ for both gait-agnostic and multi-gait formulations (Tables I and IV). Across most configurations, shorter temporal horizons (H∈1,5H∈\1,5\) yield significantly more stable and successful locomotion policies. As the trailing window expands to H=20H=20 and H=30H=30, performance generally degrades. In the gait-agnostic setting, GPT-GA maintains a perfect 100%100\% success rate and optimal cost of transport (CoT ≤1.00≤ 1.00) for H≤10H≤ 10, but command tracking success collapses to 44%44\% at H=20H=20. Similarly, in the multi-gait setting, Qwen-MG achieves perfect command tracking and high efficiency (CoT of 1.281.28) at H=1H=1, yet its performance degrades as the window size increases, dropping to a 27.8%27.8\% success rate at H=30H=30. While GPT-MG exhibits a minor improvement in success rate at longer horizons in the multi-gait task, its overall performance remains well below Qwen-MG’s peak. Furthermore, even when success and survival rates remain completely invariant to the horizon size, as seen with Qwen-GA, energy efficiency consistently worsens at longer horizons. These results show that a longer robustness horizon is not always beneficial. Because the robustness of G (always) specifications depends on the worst value in the window, larger H can keep past violations in the reward longer and make credit assignment harder, whereas short horizons provide a more immediate learning signal. VI Conclusion We presented an LLM-assisted formal reward-design pipeline for quadruped locomotion. Instead of asking a language model to directly choose reward code and numerical coefficients, GPT-5.5 and Qwen 3.6 propose parametric STL structures; expert trajectories determine their parameters and filter out systematically violated suggestions; and smooth STL robustness provides the PPO reward. The resulting framework supports both gait-aware multi-gait control and a gait-agnostic setting in which locomotion style is allowed to emerge. These comparisons allow us to study what is gained and what remains difficult when temporal logic is inserted between language-model generation and policy learning. A notable limitation is that our evaluations are currently confined to simulation (MJX). Despite employing domain randomization over friction and actuation parameters, the empirical sim-to-real transferability of these learned multi-gait behaviors has yet to be established on a physical quadruped. TABLE I: Multi-gait locomotion results across commanded forward velocities. Lower CoT is better; higher survival, command success, and gait success are better. Gait success measures whether the desired gait associated with the commanded speed regime is successfully exhibited. vxv_x CoT ↓ Survival ↑ Success ↑ Gait Match ↑ Expert Oracle 0.3 0.92±0.020.92± 0.02 100%100\% 100%100\% Success 0.5 0.90±0.010.90± 0.01 100%100\% 100%100\% Success 0.7 0.96±0.010.96± 0.01 100%100\% 100%100\% Success 1.0 1.08±0.011.08± 0.01 100%100\% 100%100\% Success 1.3 1.27±0.011.27± 0.01 100%100\% 100%100\% Success 1.6 1.34±0.021.34± 0.02 100%100\% 100%100\% Success 1.9 1.33±0.011.33± 0.01 95%95\% 0%0\% NA 2.0 1.35±0.011.35± 0.01 95%95\% 0%0\% NA 2.1 1.36±0.011.36± 0.01 100%100\% 0%0\% NA Human-STL 0.3 2.10±0.102.10± 0.10 100%100\% 100%100\% Success 0.5 1.50±0.001.50± 0.00 100%100\% 100%100\% Success 0.7 1.20±0.001.20± 0.00 100%100\% 100%100\% Success 1.0 1.20±0.001.20± 0.00 100%100\% 100%100\% Success 1.3 1.10±0.001.10± 0.00 100%100\% 100%100\% Success 1.6 1.00±0.001.00± 0.00 100%100\% 100%100\% Success 1.9 1.10±0.001.10± 0.00 100%100\% 100%100\% Success 2.0 1.10±0.001.10± 0.00 100%100\% 100%100\% Success 2.1 1.10±0.001.10± 0.00 100%100\% 100%100\% Success GPT-MG 0.3 1.96±0.041.96± 0.04 100%100\% 100%100\% Success 0.5 1.62±0.031.62± 0.03 100%100\% 100%100\% Success 0.7 1.45±0.031.45± 0.03 100%100\% 100%100\% Success 1.0 1.27±0.021.27± 0.02 100%100\% 100%100\% Success 1.3 1.17±0.011.17± 0.01 100%100\% 100%100\% Success 1.6 1.26±0.011.26± 0.01 100%100\% 100%100\% Partially 1.9 1.27±0.011.27± 0.01 100%100\% 0%0\% NA 2.0 1.28±0.011.28± 0.01 100%100\% 0%0\% NA 2.1 1.28±0.021.28± 0.02 100%100\% 0%0\% NA Qwen-MG 0.3 1.97±0.051.97± 0.05 100%100\% 100%100\% Fail 0.5 1.42±0.031.42± 0.03 100%100\% 100%100\% Fail 0.7 1.22±0.021.22± 0.02 100%100\% 100%100\% Fail 1.0 1.18±0.011.18± 0.01 100%100\% 100%100\% Fail 1.3 1.10±0.011.10± 0.01 100%100\% 100%100\% Fail 1.6 1.09±0.011.09± 0.01 100%100\% 100%100\% Success 1.9 1.15±0.021.15± 0.02 100%100\% 100%100\% Success 2.0 1.19±0.011.19± 0.01 100%100\% 100%100\% Success 2.1 1.22±0.011.22± 0.01 100%100\% 100%100\% Success Text2Reward-MG 0.3 1.10±0.021.10± 0.02 100%100\% 100%100\% Success 0.5 0.82±0.010.82± 0.01 100%100\% 100%100\% Success 0.7 0.83±0.010.83± 0.01 100%100\% 100%100\% Success 1.0 1.04±0.011.04± 0.01 100%100\% 100%100\% Fail 1.3 1.01±0.011.01± 0.01 100%100\% 100%100\% Fail 1.6 0.98±0.010.98± 0.01 100%100\% 100%100\% Fail 1.9 1.05±0.151.05± 0.15 0%0\% 0%0\% NA 2.0 1.06±0.181.06± 0.18 0%0\% 0%0\% NA 2.1 1.05±0.171.05± 0.17 0%0\% 0%0\% NA TABLE I: Ablation of STL robustness window size H for gait-agnostic policies. Metrics are averaged across all evaluated commanded forward velocities. Method H CoT ↓ Survival ↑ Success ↑ GPT-GA 1 0.99 100% 100% 5 0.99 100% 100% 10 1.00 100% 100% 20 1.15 100% 44% 30 1.14 100% 67% Qwen-GA 1 1.111.11 55.6%55.6\% 55.6%55.6\% 5 1.111.11 55.6%55.6\% 55.6%55.6\% 10 1.261.26 55.6%55.6\% 55.6%55.6\% 20 1.291.29 55.6%55.6\% 55.6%55.6\% 30 1.551.55 55.6%55.6\% 55.6%55.6\% TABLE IV: Ablation of STL robustness window size H for multi-gait policies. Metrics are averaged across all evaluated commanded forward velocities. Method H CoT ↓ Survival ↑ Success ↑ GPT-MG 1 1.40 100% 55.6% 5 1.60 100% 55.6% 10 1.37 100% 55.6% 20 1.40 100% 66.7% 30 1.36 99.4% 66.7% Qwen-MG 1 1.281.28 100%100\% 100%100\% 5 1.321.32 100%100\% 77.8%77.8\% 10 2.082.08 88.3%88.3\% 60.6%60.6\% 20 14.2514.25 77.8%77.8\% 54.4%54.4\% 30 3.593.59 77.8%77.8\% 27.8%27.8\% References [1] P. Dayan and B. W. Balleine (2002) Reward, motivation, and reinforcement learning. Neuron 36 (2), p. 285–298. Cited by: §I. [2] J. Tan, T. Zhang, E. Coumans, A. Iscen, Y. Bai, D. Hafner, S. Bohez, and V. Vanhoucke (2018) Sim-to-real: learning agile locomotion for quadruped robots. arXiv preprint arXiv:1804.10332. Cited by: §I. [3] J. Lee, J. Hwangbo, L. Wellhausen, V. Koltun, and M. Hutter (2020) Learning quadrupedal locomotion over challenging terrain. Science robotics 5 (47), p. eabc5986. Cited by: §I. [4] J. Eschmann (2021) Reward function design in reinforcement learning. Reinforcement learning algorithms: Analysis and Applications, p. 25–33. Cited by: §I. [5] R. T. Icarte, T. Q. Klassen, R. Valenzano, and S. A. McIlraith (2022) Reward machines: exploiting reward function structure in reinforcement learning. Journal of Artificial Intelligence Research 73, p. 173–208. Cited by: §I. [6] K. Caluwaerts, A. Iscen, J. C. Kew, W. Yu, T. Zhang, D. Freeman, K. Lee, L. Lee, S. Saliceti, V. Zhuang, et al. (2023) Barkour: benchmarking animal-level agility with quadruped robots. arXiv preprint arXiv:2305.14654. Cited by: §I, §I, §IV-A, Example 1. [7] K. Zakka, B. Tabanpour, Q. Liao, M. Haiderbhai, S. Holt, J. Y. Luo, A. Allshire, E. Frey, K. Sreenath, L. A. Kahrs, et al. (2025) Mujoco playground. arXiv preprint arXiv:2502.08844. Cited by: §I, §I. [8] J. Hare (2019) Dealing with sparse rewards in reinforcement learning. arXiv preprint arXiv:1910.09281. Cited by: §I. [9] G. Kim, Y. Lee, and H. Park (2025) A learning framework for diverse legged robot locomotion using barrier-based style rewards. In 2025 IEEE International Conference on Robotics and Automation (ICRA), p. 10004–10010. Cited by: §I. [10] J. Fu, K. Luo, and S. Levine (2017) Learning robust rewards with adversarial inverse reinforcement learning. arXiv preprint arXiv:1710.11248. Cited by: §I. [11] A. Y. Ng S. Russell et al. (2000) Algorithms for inverse reinforcement learning.. In Icml, Vol. 1, p. 2. Cited by: §I. [12] S. Arora and P. Doshi (2021) A survey of inverse reinforcement learning: challenges, methods and progress. Artificial Intelligence 297, p. 103500. Cited by: §I. [13] P. F. Christiano, J. Leike, T. Brown, M. Martic, S. Legg, and D. Amodei (2017) Deep reinforcement learning from human preferences. Advances in neural information processing systems 30. Cited by: §I. [14] D. Youm, H. Jung, H. Kim, J. Hwangbo, H. Park, and S. Ha (2023) Imitating and finetuning model predictive control for robust and symmetric quadrupedal locomotion. IEEE Robotics and Automation Letters 8 (11), p. 7799–7806. Cited by: §I. [15] T. Li, J. Won, J. Cho, S. Ha, and A. Rai (2023) Fastmimic: model-based motion imitation for agile, diverse and generalizable quadrupedal locomotion. Robotics 12 (3), p. 90. Cited by: §I. [16] M. Hasanbeig, D. Kroening, and A. Abate (2020) Deep reinforcement learning with temporal logics. In International Conference on Formal Modeling and Analysis of Timed Systems, p. 1–22. Cited by: §I. [17] X. Li, C. Vasile, and C. Belta (2017) Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), p. 3834–3839. Cited by: §I, §I. [18] H. Liao (2020) A survey of reinforcement learning with temporal logic rewards. Cited by: §I. [19] X. Li, C. Vasile, and C. Belta (2017) Reinforcement learning with temporal logic rewards. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), p. 3834–3839. Cited by: §I, §I. [20] P. Kapoor, A. Balakrishnan, and J. V. Deshmukh (2020) Model-based reinforcement learning from signal temporal logic specifications. arXiv preprint arXiv:2011.04950. Cited by: §I. [21] A. Puranic, J. Deshmukh, and S. Nikolaidis (2021) Learning from demonstrations using signal temporal logic. In Conference on Robot Learning, p. 2228–2242. Cited by: §I. [22] S. Feng, X. Xinjilefu, W. Huang, and C. G. Atkeson (2013) 3D walking based on online optimization. In 2013 13th IEEE-RAS International Conference on Humanoid Robots (Humanoids), p. 21–27. Cited by: §I. [23] Y. Zhao, U. Topcu, and L. Sentis (2016) High-level planner synthesis for whole-body locomotion in unstructured environments. In 2016 IEEE 55th Conference on Decision and Control (CDC), p. 6557–6564. Cited by: §I. [24] H. Audren, A. Kheddar, and P. Gergondet (2016) Stability polygons reshaping and morphing for smooth multi-contact transitions and force control of humanoid robots. In 2016 IEEE-RAS 16th International Conference on Humanoid Robots (Humanoids), p. 1037–1044. Cited by: §I. [25] Z. Gu, R. Guo, W. Yates, Y. Chen, Y. Zhao, and Y. Zhao (2024) Walking-by-logic: signal temporal logic-guided model predictive control for bipedal locomotion resilient to external perturbations. In 2024 IEEE International Conference on Robotics and Automation (ICRA), p. 1121–1127. Cited by: §I. [26] Z. Gu, Y. Zhao, Y. Chen, R. Guo, J. K. Leestma, G. S. Sawicki, and Y. Zhao (2025) Robust-locomotion-by-logic: perturbation-resilient bipedal locomotion via signal temporal logic guided model predictive control. IEEE Transactions on Robotics. Cited by: §I. [27] J. Humphreys and C. Zhou (2025) Learning to adapt through bio-inspired gait strategies for versatile quadruped locomotion. Nature Machine Intelligence 7 (7), p. 1141–1153. Cited by: §I. [28] D. DeFazio, Y. Hayamizu, and S. Zhang (2024) Learning quadruped locomotion policies using logical rules. In Proceedings of the International Conference on Automated Planning and Scheduling, Vol. 34, p. 142–150. Cited by: §I. [29] O. Maler and D. Nickovic (2004) Monitoring temporal properties of continuous signals. In International symposium on formal techniques in real-time and fault-tolerant systems, p. 152–166. Cited by: §I. [30] A. Donzé and O. Maler (2010) Robust satisfaction of temporal logic over real-valued signals. In International conference on formal modeling and analysis of timed systems, p. 92–106. Cited by: §I, §I. [31] G. E. Fainekos and G. J. Pappas (2009) Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science 410 (42), p. 4262–4291. Cited by: §I, §I. [32] A. Balakrishnan and J. V. Deshmukh (2019) Structured reward shaping using signal temporal logic specifications. in 2019 ieee/rsj iros, 3481–3486. IEEE. Cited by: §I. [33] D. Aksaray, A. Jones, Z. Kong, M. Schwager, and C. Belta (2016) Q-learning for robust satisfaction of signal temporal logic specifications. In 2016 IEEE 55th Conference on Decision and Control (CDC), p. 6565–6570. Cited by: §I. [34] M. Atasever, C. Bakirci, A. R. Corona, K. Azbijari, and J. V. Deshmukh (2026) Learning gait-aware quadruped locomotion with temporal logic specifications. arXiv preprint arXiv:2607.00442. Cited by: §I. [35] T. Xie, S. Zhao, C. Wu, Y. Liu, Q. Luo, V. Zhong, Y. Yang, and T. Yu (2024) Text2reward: reward shaping with language models for reinforcement learning. In International Conference on Learning Representations, Vol. 2024, p. 35663–35699. Cited by: §I, §IV-A. [36] Y. J. Ma, W. Liang, G. Wang, D. Huang, O. Bastani, D. Jayaraman, Y. Zhu, J. Fan, et al. (2024) Eureka: human-level reward design via coding large language models. In International conference on learning Representations, Vol. 2024, p. 26516–26560. Cited by: §I. [37] Y. Chen, R. Gandhi, Y. Zhang, and C. Fan (2023) Nl2tl: transforming natural languages to temporal logics using large language models. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, p. 15880–15903. Cited by: §I. [38] OpenAI (2026) GPT-5.5: large language model. Note: https://openai.comAccessed: [2026-08-19] Cited by: §I. [39] Qwen Team (2026) Qwen3.6: open foundation model. Alibaba Cloud. Note: https://huggingface.co/QwenAccessed: [2026-08-19] Cited by: §I. [40] J. Schulman, F. Wolski, P. Dhariwal, A. Radford, and O. Klimov (2017) Proximal policy optimization algorithms. arXiv preprint arXiv:1707.06347. Cited by: §I. [41] N. Kohl and P. Stone (2004) Policy gradient reinforcement learning for fast quadrupedal locomotion. In IEEE International Conference on Robotics and Automation, 2004. Proceedings. ICRA’04. 2004, Vol. 3, p. 2619–2624. Cited by: §I. [42] E. Todorov, T. Erez, and Y. Tassa (2012) Mujoco: a physics engine for model-based control. In 2012 IEEE/RSJ international conference on intelligent robots and systems, p. 5026–5033. Cited by: §I. [43] E. Asarin, A. Donzé, O. Maler, and D. Nickovic (2011) Parametric identification of temporal properties. In International Conference on Runtime Verification, p. 147–160. Cited by: §I. [44] Y. Gilpin, V. Kurtz, and H. Lin (2020) A smooth robustness measure of signal temporal logic for symbolic control. IEEE Control Systems Letters 5 (1), p. 241–246. Cited by: §I. [45] Z. Fu, A. Kumar, J. Malik, and D. Pathak (2021) Minimizing energy consumption leads to the emergence of gaits in legged robots. arXiv preprint arXiv:2111.01674. Cited by: §I-A. [46] Y. Yang, T. Zhang, E. Coumans, J. Tan, and B. Boots (2022) Fast and efficient locomotion via learned gait transitions. In Conference on robot learning, p. 773–783. Cited by: §I-A. [47] R. M. Alexander and A. Jayes (1983) A dynamic similarity hypothesis for the gaits of quadrupedal mammals. Journal of zoology 201 (1), p. 135–152. Cited by: §I-A. [48] J. Humphreys, J. Li, Y. Wan, H. Gao, and C. Zhou (2023) Bio-inspired gait transitions for quadruped locomotion. IEEE Robotics and Automation Letters 8 (10), p. 6131–6138. Cited by: §I-A.