Interactive Synthesis of Temporal Specifications from Examples and Natural Language
summary
LTLTalk synthesizes co-safe LTL specifications from one natural-language command plus a single demonstration by encoding structure and semantics as an SMT problem and using soft constraints biased by language. It generates multiple candidates, creates distinguishing worlds and animations, and narrows them with user judgments. Implemented in a simulated robot world, it uses SMT-based synthesis, grammar expansion to learn new DSL rules, averages 9.6s and 2.4 interactions, and recovers the correct spec in 8 of 10 benchmarks.
AI-written summary · about
chapters (9)
- 0:00Intro
- 0:26There is a promise...
- 0:44Synthesizing correct executions from specifications
- 7:09LTL: Linear Temporal Logic
- 8:36Generating candidate specifications: hard constraints
- 10:05Generating candidate specifications: soft constraints
- 12:03Interactive Synthesis: Conclusions from the Evaluation
- 13:31Interactive Synthesis: High-Level Overview
- 13:41Grammar Expansion
related talks
21mProgramming-by-Demonstration for Long-Horizon Robot Tasks
15mAbstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
29mSynchronous Programming and Refinement Types in Robotics: From Verification to Implementation
25mHigh-Level Mission Specification for Multiple Robots
28mPreference Learning from Minimal Human Feedback for Interactive
14mROSpec: A Domain-Specific Language for ROS-based Robot Software
20mAuthoring and Verifying Human-Robot Interactions
09mSituated Live Programming for Human-Robot Collaboration