-
SAIL: Faster-than-Demonstration Execution of Imitation Learning Policies
Authors:
Nadun Ranawaka Arachchige,
Zhenyang Chen,
Wonsuhk Jung,
Woo Chul Shin,
Rohan Bansal,
Pierre Barroso,
Yu Hang He,
Yingyang Celine Lin,
Benjamin Joffe,
Shreyas Kousik,
Danfei Xu
Abstract:
Offline Imitation Learning (IL) methods such as Behavior Cloning are effective at acquiring complex robotic manipulation skills. However, existing IL-trained policies are confined to executing the task at the same speed as shown in demonstration data. This limits the task throughput of a robotic system, a critical requirement for applications such as industrial automation. In this paper, we introd…
▽ More
Offline Imitation Learning (IL) methods such as Behavior Cloning are effective at acquiring complex robotic manipulation skills. However, existing IL-trained policies are confined to executing the task at the same speed as shown in demonstration data. This limits the task throughput of a robotic system, a critical requirement for applications such as industrial automation. In this paper, we introduce and formalize the novel problem of enabling faster-than-demonstration execution of visuomotor policies and identify fundamental challenges in robot dynamics and state-action distribution shifts. We instantiate the key insights as SAIL (Speed Adaptation for Imitation Learning), a full-stack system integrating four tightly-connected components: (1) a consistency-preserving action inference algorithm for smooth motion at high speed, (2) high-fidelity tracking of controller-invariant motion targets, (3) adaptive speed modulation that dynamically adjusts execution speed based on motion complexity, and (4) action scheduling to handle real-world system latencies. Experiments on 12 tasks across simulation and two real, distinct robot platforms show that SAIL achieves up to a 4x speedup over demonstration speed in simulation and up to 3.2x speedup in the real world. Additional detail is available at https://nadunranawaka1.github.io/sail-policy
△ Less
Submitted 13 June, 2025;
originally announced June 2025.
-
Adapt3R: Adaptive 3D Scene Representation for Domain Transfer in Imitation Learning
Authors:
Albert Wilcox,
Mohamed Ghanem,
Masoud Moghani,
Pierre Barroso,
Benjamin Joffe,
Animesh Garg
Abstract:
Imitation Learning can train robots to perform complex and diverse manipulation tasks, but learned policies are brittle with observations outside of the training distribution. 3D scene representations that incorporate observations from calibrated RGBD cameras have been proposed as a way to mitigate this, but in our evaluations with unseen embodiments and camera viewpoints they show only modest imp…
▽ More
Imitation Learning can train robots to perform complex and diverse manipulation tasks, but learned policies are brittle with observations outside of the training distribution. 3D scene representations that incorporate observations from calibrated RGBD cameras have been proposed as a way to mitigate this, but in our evaluations with unseen embodiments and camera viewpoints they show only modest improvement. To address those challenges, we propose Adapt3R, a general-purpose 3D observation encoder which synthesizes data from calibrated RGBD cameras into a vector that can be used as conditioning for arbitrary IL algorithms. The key idea is to use a pretrained 2D backbone to extract semantic information, using 3D only as a medium to localize this information with respect to the end-effector. We show across 93 simulated and 6 real tasks that when trained end-to-end with a variety of IL algorithms, Adapt3R maintains these algorithms' learning capacity while enabling zero-shot transfer to novel embodiments and camera poses.
△ Less
Submitted 15 May, 2025; v1 submitted 6 March, 2025;
originally announced March 2025.
-
Leroy and Blazy were right: their memory model soundness proof is automatable (Extended Version)
Authors:
Pedro Barroso,
Mário Pereira,
António Ravara
Abstract:
Xavier Leroy and Sandrine Blazy in 2007 conducted a formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C. Considering their formalization was performed essentially in first-order logic, one question left open by the authors was whether their proofs could be automated using a verification framework for first-order logic. We took the chal…
▽ More
Xavier Leroy and Sandrine Blazy in 2007 conducted a formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C. Considering their formalization was performed essentially in first-order logic, one question left open by the authors was whether their proofs could be automated using a verification framework for first-order logic. We took the challenge and automated their formalization using Why3, significantly reducing the proof effort. We systematically followed the Coq proofs and realized that in many cases at around one third of the way Why3 was able to discharge all VCs. Furthermore, the proofs still requiring interactions (e.g. induction, witnesses for existential proofs, assertions) were factorized isolating auxiliary results that we stated explicitly. In this way, we achieved an almost-automatic soundness and safety proof of the memory model. Nonetheless, our development allows an extraction of a correct-by-construction concrete memory model, going thus further than the preliminary Why version of Leroy and Blazy.
△ Less
Submitted 5 December, 2022;
originally announced December 2022.
-
Animated Logic: Correct Functional Conversion to Conjunctive Normal Form
Authors:
Pedro Barroso,
Mário Pereira,
António Ravara
Abstract:
We present an approach to obtain formally verified implementations of classical Computational Logic algorithms. We choose the Why3 platform because it allows to implement functions in a style very close to the mathematical definitions, as well as it allows a high degree of automation in the verification process.
As proof of concept, we present a mathematical definition of the algorithm to conver…
▽ More
We present an approach to obtain formally verified implementations of classical Computational Logic algorithms. We choose the Why3 platform because it allows to implement functions in a style very close to the mathematical definitions, as well as it allows a high degree of automation in the verification process.
As proof of concept, we present a mathematical definition of the algorithm to convert propositional formulae to conjunctive normal form, implementations in WhyML (the Why3 language, very similar to OCaml), and proofs of correctness of the implementations. We apply our proposal on two variants of this algorithm: one in direct-style and another with an explicit stack structure. Being both first-order versions, Why3 processes the proofs naturally.
△ Less
Submitted 10 March, 2020;
originally announced March 2020.
