Robert Joseph George - Building Trustworthy AI for Mathematics and Science
Discussion description: AI systems are becoming increasingly capable at mathematics, coding, and scientific reasoning, but generating a convincing answer is very different from generating one that can be rigorously trusted. In this discussion, I’ll begin with a brief introduction to Lean and formal theorem proving, and explain how formal methods can be used to make mathematical and computational reasoning machine-checkable. I’ll then discuss our work on TorchLean, a framework for verified machine learning in Lean, including neural-network execution, automatic differentiation, floating-point semantics, and neural-network verification. I’ll also cover FloatLib, our work on formally verified floating-point arithmetic, and how these tools fit into a broader effort to build AI and scientific-computing systems whose outputs can be independently checked rather than simply trusted. Finally, I’ll discuss recent advances in using AI and computation for difficult problems in mathematics and scientific computing, including recent progress surrounding the Navier–Stokes and Euler equations and some of our own work on singularity formation and stability in the 3D Euler equations. More broadly, I’ll explore how AI, numerical computation, and formal verification may increasingly work together as tools for mathematical discovery. More broadly, the discussion will explore what it might look like for AI to become a genuine tool for mathematical discovery: proposing ideas, performing large-scale computation, assisting with proofs, and ultimately helping verify the scientific and mathematical claims that emerge from that process.
Brief bio:
Robert Joseph George is a PhD student in Mathematics and Computer Science at Caltech, advised by Anima Anandkumar. His research focuses on verified machine learning, AI for mathematics, formal verification, and scientific computing. He is supported by the Caltech Graduate Fellowship, Harmonic AI, and DARPA expMath fund.