A new framework lets engineers specify exactly how a four-legged robot should move — and then automatically turns those specs into training rewards.
Researchers built a system where distinct gaits (walking-trot, trot, and bound) are defined using Signal Temporal Logic, a formal language for describing time-based constraints. Those specs — covering things like leg synchronization, speed tracking, and joint limits — get converted into a continuous reward signal fed to a Proximal Policy Optimization training loop. The team tested it on Google's Barkour quadruped inside the MuJoCo XLA physics simulator, using parallelization and domain randomization to speed up training and toughen the resulting policies.
The headline result: STL-shaped rewards produced tighter velocity tracking and more stable training than the hand-crafted baseline. That matters because hand-crafted reward functions are notoriously brittle — small tweaks can collapse a policy, and it's rarely obvious why. Encoding gait requirements as formal specifications makes the intended behavior explicit and auditable, which is useful both for debugging and for anyone who needs to certify that a robot won't behave unexpectedly.
Robotics labs have long leaned on dense reward shaping to coax RL agents into useful behavior; the novelty here is using a formal specification language to generate those shaped rewards systematically rather than by intuition. Whether that holds up outside a simulator is the next question.