Position: Formal Methods are the Principled Foundation of Safe AI

Artificial Intelligence (AI) has the potential to transform society and the economy. However, both public and private entities have been increasingly expressing significant concern about the potential of state-of-the-art AI models to cause societal and financial harm. This lack of trust is because they can misbehave, and we lack a clear, principled understanding of when, why, or how they fail. Formal methods offer a principled foundation to mitigate risks, yielding stronger notions of trust than possible with intuition or empirical methods, such as bug finding and benchmarking. In this position paper, we will describe how formal methods can be used for (i) proving that a trained model satisfies desired safety properties, (ii) guiding the model updates during training towards satisfying safety properties, and (iii) reliably explaining and interpreting the black-box workings of AI models. We will discuss the challenges hindering the broader adoption of formal methods for AI safety and outline future directions for overcoming them.