AI and Formal Methods

The current era of Artificial Intelligence has demonstrated models powerful enough to catalyze major theoretical advances across fields like mathematics, physics, and biology through automated reasoning. Despite this power, frequent ”hallucinations” severely limit the usefulness of large language models as reliable scientific collaborators. To realize the promise of these technologies, scientists need a strong basis for trusting AI outputs, which requires robust mechanisms to catch, fix, and ultimately avoid errors. As recent discussions in both academia and industry highlight, the cost of incorrect or unverifiable AI-generated outputs, in code, scientific reasoning, and safety-critical domains, is already becoming significant. Formal methods—utilizing longstanding tools and techniques like theorem provers and model checkers—offer a rich set of symbolic reasoning capabilities. Whereas AI excels at pattern recognition, synthesis, and exploration, formal methods provide mathematically grounded tools for specification, verification, and explanation. Together, they offer the potential to move from plausible outputs to provably correct and trustworthy systems. In addition, formal verification can provide a training signal for improving the reasoning capabilities of the underlying models. This summit will convene leading scientists from AI, programming languages, formal verification, systems, mathematics, theoretical physics, and theoretical CS to forge a timely and necessary research agenda: the integration of AI methods with formal methods to drive scientific progress across the theoretical sciences. Experts from different disciplines have different needs, concerns, and perspectives on formal methods, so bringing these communities together will facilitate transfer of knowledge and techniques between domains.