For the past 60 years, we have been relying on testing for building robust, bug-free software. And yet, despite our best efforts, bugs slip past our test cases all the time, resulting in a number of incidents that range from benign to catastrophic. In this lecture series, you will be introduced to an entirely different way to build robust software: by writing code that is formally proven to be free of bugs. We will cover the basics of formal verification that is required for real, complex systems: specification, building state machines and reasoning about them using inductive invariants.
Learning and decision-making problems often boil down to a balancing act between exploring new possibilities and exploiting the best known one. For nearly seventy-five years, the multi-armed bandit problem has been the predominant theoretical model for investigating these issues. Applications in machine learning and electronic markets pushed multi-armed bandits to the forefront of computing research in the present century. These lectures will introduce some seminal algorithms for solving multi-armed bandit problems in Bayesian and prior-independent settings, discuss contemporary extensions to contextual bandit problems, and present applications to settings with strategic users.
Mitigating distribution shift remains one of the major challenges of AI and machine learning. Training distributions often deviate significantly from test distributions, and pre-trained models are commonly deployed without a precise understanding of these differences. In such cases, a model may have poor performance with potentially dangerous consequences.
In this minicourse we will describe the first set of efficient algorithms for learning with distribution shift for broad classes of functions and distributions. A major obstacle to obtaining these algorithms is the computational intractability of testing even simple properties of distributions. Instead we will analyze algorithms that are allowed to fail gracefully or reject if a significant distribution shift is detected. Our topics will touch on many areas of theoretical computer science and machine learning.