Modern engineering applications such as autonomous robots involve large-scale dynamical systems whose models are complex, uncertain, or only partially known, placing them beyond the reach of traditional model-based control techniques. Data-driven approaches, including machine learning and reinforcement learning, offer powerful tools for learning and decision-making in these settings, but often lack interpretability and provide limited guarantees of correctness and safety—critical requirements. Formal methods address these shortcomings by providing rich languages for expressing complex objectives and safety requirements, algorithmic techniques for verification and synthesis, and proofs that the resulting systems behave as intended. This talk that brings together control theory, formal methods, and machine learning to create control systems that scale and adapt to uncertain or unknown dynamics while remaining safe, correct, and interpretable. Examples from autonomous driving and robotic manipulation illustrate how this integration enables the synthesis of controllers for complex, safety-critical tasks.

[1] A formal methods approach to interpretable reinforcement learning for robotic planning

[2] Safe Model-based Control from Signal Temporal Logic Specifications Using Recurrent Neural Networks