8. Formal Methods and Decision Making in the Age of AI
Organizers: Lars Lindemann, Cristian Ioan Vasile
Website: https://sites.google.com/lehigh.edu/fmcdc2023
Location: Orchid Junior 4211
Abstract:
The rapid advancement of machine learning and AI is leading to a paradigm shift in the way we make high-level decisions and low-level control for autonomous and robotic systems. While these advancements present exciting opportunities towards building intelligent systems, it also introduces new challenges, such as dealing with the fragility of neural networks, that require novel solutions. Our workshop on “Formal Methods and Decision Making in the Age of AI” aims to unravel these challenges and open problems for a general audience and discuss what new principles and techniques we need for perception-enabled system design, scalable design of distributed systems, verifiable learning-enabled systems, systems with humans in the loop, and safety in autonomy. For this purpose, we have invited eight renowned expert speakers.
One of the primary objectives of the workshop is to identify key research challenges and opportunities in the areas of formal methods and decision making in the age of AI. Our speakers have been selected in this regard, and the workshop has a focus on:
- Control of perception-enabled systems: Perception-enabled systems are those that use high-dimensional sensors to make sense of the environment so that appropriate control actions can be taken. The workshop will popularize recent approaches for analyzing these systems, including statistical techniques for handling uncertainty under formal specifications.
- Scalable design of distributed systems: As AI becomes increasingly integrated into distributed systems, new methods are needed for designing and testing large-scale multi-agent systems. These design approaches need to be scalable and formally correct even in the face of agent failures and changing environmental conditions.
- Verifiable learning-enabled systems: As AI systems become more complex and autonomous, it becomes increasingly important to ensure and verifying that they are behaving as intended. Formal methods can be used to precisely formulate an intended system behavior, and new scalable formal verification tools need to be designed for verifying that high-dimensional learning-enabled systems are achieving their intended goals.
- Systems with humans in the loop: As humans become more integrated into AI systems, new approaches are needed for designing and evaluating feedback control loops that now incorporate robot and human feedback. The workshop will explore methods for ensuring that AI systems can effectively interact with humans. Formal specifications are close to structured language and present a convenient interface between humans.
- Safety in autonomy: One of the most critical challenges in the development of AI systems is ensuring their safety and reliability. There is a strong need for new methods for ensuring the safety of autonomous systems, including approaches for identifying and mitigating potential failures and developing backup systems in case of a failure.
The workshop will provide a platform for theoreticians as well as practitioners from the fields of systems & control theory, formal methods, machine learning & AI, and applied mathematics to come together and discuss their latest research and emerging trends. Participants will be able to share their insights with each other on the current state-of-the-art in formal methods, decision making and AI, and explore opportunities for interdisciplinary collaborations. To further exchange between our speakers and participants, we will have panel discussions.
With this workshop, we would also like to address a common misconception that formal methods in robotics and control do not scale and are hence not practical. Our expert speakers will showcase that we can now solve real-life problems and have reached a certain stage of maturity. Therefore, the workshop will also promote the use of formal methods and decision making techniques in real-world applications, including autonomous driving and robotic systems.
Overall, the workshop aims to advance our understanding of the challenges and opportunities that arise from the use of AI in decision making. By bringing together experts from different fields, the workshop will facilitate interdisciplinary collaborations and foster the development of new approaches that can help ensure the safe and effective use of AI technologies.
Lecture Schedule:
Event | Time |
Initial Remarks (Prof. Lars Lindemann and Prof. Cristian-Ioan Vasile) | 8:45 am to 9:00 am |
Speaker: Dr. Morteza Lahijanian, University of Colorado Boulder Data-driven Verification and Control Synthesis for Dynamical Systems via Bayesian Reasoning | 9:00 am to 9:35 am |
Speaker: Dr. Necmiye Ozay, University of Michigan Formal methods for Cyber Physical Systems: State of the Art and Future Challenges | 9:35 am to 10:10 am |
Break | 10:10 am to 10:25 am |
Speaker: Dr. Dimos Dimarogonas, KTH Royal Institute of Technology Spatiotemporal logic control for leader-follower multi-agent systems | 10:25 am to 11:00 am |
Speaker: Dr. Jyotirmoy Deshmukh, University of Southern California Logic-based Specifications meet Learning-enabled Control | 11:00 am to 11:35 am |
Break | 11:35 am to 11:40 am |
Panel Discussion Panelists: Lahijanian, Ozay, Dimarogonas, Deshmukh | 11:40 am to 12:00 pm |
Lunch | 12:00 pm to 1:30 pm |
Speaker: Dr. Alessandro Abate, University of Oxford Certified learning, or learning for verification? | 1:30 pm to 2:05 pm |
Speaker: Dr. Xiang Yin, Shanghai Jiao Tong University Formal Verification and Synthesis of Security for Cyber-Physical Systems: Notions, Algorithms and Recent Trends | 2:05 pm to 2:40 pm |
Speaker: Dr. Yiannis Kantaros, Washington University St. Louis Safe Perception-based Temporal Logic Planning in Unknown Semantic Environments | 2:40 pm to 3:15 pm |
Break | 3:15 pm to 3:30 pm |
Speaker: Dr. Sayan Mitra, University of Illinois at Urbana Champaign Assuring Safety of Learning-Enabled Systems with Perception Contracts | 3:30 pm to 4:05 pm |
Speaker: Dr. Sofie Haesaert, Eindhoven University of Technology Using data to tackle uncertainty in correct-by-design control synthesis | 4:05 pm to 4:40 pm |
Break | 4:40 pm to 4:45 pm |
Panel Discussion Panelists: Abate, Yin, Kantaros, Mitra, Haesaert | 4:45 pm to 5:05 pm |