Cornell gets $3.8 million for AI verification research

Cornell said mathematics professor Lionel Levine received $1.5 million over 18 months from the nonprofit Coefficient Giving to test whether language models follow the principles, or “constitutions,” written for them by developers. Associate professor Daniel Halpern-Leistner received $2.3 million over three years from the Defense Advanced Research Projects Agency to develop tools that translate parts of mathematical arguments into computer-verifiable form.

Together, the awards point to the same economic problem: AI systems are becoming more capable, but verification remains labor-intensive, human-dependent and slow. That creates a drag on productivity in fields where confidence in results is essential. In mathematics, where AI is increasingly helping generate long and intricate proofs, the cost of checking can become a binding constraint on research throughput. In AI safety, the inability to test whether a model follows stated values raises the risk that companies ship systems whose behavior diverges from their training goals.

Levine’s work builds on EigenBench, a benchmark Cornell says it has already developed to measure aspects of a model’s character and values. His team will try to create scoring methods for constitutional adherence, assess whether outside auditors can verify the principles used in training, and examine whether model behavior shifts during recursive self-improvement. That last question is especially relevant to developers racing to improve models with AI-generated feedback, because it goes to whether oversight can keep pace with model evolution.

Halpern-Leistner’s project targets a different but related vulnerability: the growing volume of mathematical work AI can help produce. His team is building “autoformalization” tools that convert pieces of an argument into a format a computer can check. Cornell said the tools are already available through MathCopilot.org, with the aim of folding verification into ordinary workflows rather than treating it as an after-the-fact audit.

The broader market implication is that AI safety is moving from abstract debate to infrastructure investment. Anthropic’s recent warning that advanced systems could manipulate or blackmail users, Meta’s cuts to AI safety staff and OpenAI’s pauses over security concerns have all underscored the tension between speed and control. Funding like Cornell’s does not solve those risks, but it does show where capital and public research dollars are being directed: toward measurement, auditing and formal verification rather than just larger models.

For investors, that matters because the next phase of AI competition may hinge less on training bigger systems than on proving they are reliable enough for enterprise use, regulated industries and scientific applications. Companies that can reduce verification costs, document model behavior and build credible safety tooling may be better positioned to defend margins and avoid regulatory backlash. Those that cannot may face slower adoption, higher compliance costs and greater legal exposure if models behave in ways their developers did not intend.

The two Cornell grants are unlikely to produce commercial deployment soon, but they highlight a structural shift in AI spending priorities. As frontier models become more powerful, the premium on trust, auditability and proof-checking is rising with them.