Cornell mathematicians are developing new approaches to two growing challenges created by advanced artificial intelligence: ensuring that AI systems behave according to intended values and verifying the rapidly increasing volume of AI-assisted mathematical research.
Lionel Levine, professor of mathematics at Cornell University, received $1.5 million over 18 months from Coefficient Giving to develop mathematical tools for AI safety. His research focuses on the constitutions used to define the character and values of frontier language models.
Levine’s team is working on four connected projects. The first builds on EigenBench, a benchmark developed by his group, to measure whether large language models follow their stated constitutions. Later projects will explore methods for independently verifying the constitution used to train a model and examining whether its values change during recursive self-improvement. Another project will investigate whether desirable behavioral characteristics can be reproduced in future models.
Levine argues that recursive self-improvement requires careful study because feedback loops could produce unexpected or dangerous behavior. His Math for AI Safety initiative also provides open problems, research agendas, and papers intended to bring more mathematicians into AI safety research.
A separate $2.3 million, three-year DARPA grant supports associate professor Daniel Halpern-Leistner’s work on preserving mathematical research integrity. AI systems can now produce research-level mathematical reasoning at unprecedented volume, creating additional pressure on human reviewers.
Halpern-Leistner is developing autoformalization tools that convert mathematical arguments into forms that computers can verify. His MathCopilot platform makes current autoformalization tools freely available while minimizing disruption to mathematicians’ existing workflows.
Cornell researchers are also comparing these systems for cost, speed, and accuracy. The broader goal is to make formal verification a practical part of mathematical research, allowing researchers to work with increasingly complex arguments while retaining confidence that individual components are correct.
