Trustworthy-by-Design Autonomous AI Systems
Abstract
There has been a fast-growing trend in developing autonomous artificial intelligence (AI) systems operating in dynamic, partially known, and unpredictable environments. Autonomous AI systems must self-deliberate to accomplish tasks, especially in challenging situations when human instructions are lacking or delayed, e.g., NASA’s Mars 2020 Perseverance rover. Yet, these systems must be trustworthy, as empowering AI systems with the ability to self-deliberate carries significant risks. This necessitates a crucial need for guarantees that suitable trustworthiness in the action and decision making of the AI systems is always respected, especially for safety-critical and security-critical applications. Reactive synthesis, originated from formal methods (FM), emerges as a trustworthy-by-design technique in developing verifiably correct controllers for autonomous AI systems. This talk puts a particular focus on reactive synthesis of Linear Temporal Logic on finite traces (LTLf), which has established its scabalibity and applicability in utilizing reactive synthesis for building trustworthy autonomous AI systems. We will present in this talk an overview of key advancements in LTLf synthesis, highlighting its scalability and potential in complex scenarios. These results base on a so-called DFA-technology, which essentially takes the maximal simplicity of reasoning about efficiently constructed deterministic finite word automaton (DFA) of the LTLf objective. The goal of this talk is to engage researchers in AI and FM, encouraging further advances on developing computationally scalable techniques for trustworthy autonomous AI systems in real-world applications.