Pretrained Embeddings as a Behavior Specification Mechanism
This work addresses the challenge of specifying and verifying behaviors in AI-enabled systems, particularly for robotics and perception-based interactions, though it appears incremental as it builds on existing specification and embedding concepts.
The authors tackled the problem of formally specifying behavioral properties for AI systems interacting with the physical world by introducing embeddings as a first-class construct in a specification language, resulting in a new temporal logic called ETL that enables expressing a wider range of properties and shows promising results in steering systems toward desirable behaviors in robot planning tasks.
We propose an approach to formally specifying the behavioral properties of systems that rely on a perception model for interactions with the physical world. The key idea is to introduce embeddings -- mathematical representations of a real-world concept -- as a first-class construct in a specification language, where properties are expressed in terms of distances between a pair of ideal and observed embeddings. To realize this approach, we propose a new type of temporal logic called Embedding Temporal Logic (ETL), and describe how it can be used to express a wider range of properties about AI-enabled systems than previously possible. We demonstrate the applicability of ETL through a preliminary evaluation involving planning tasks in robots that are driven by foundation models; the results are promising, showing that embedding-based specifications can be used to steer a system towards desirable behaviors.