Resolution Publishes Work on AI-Automated Mathematical Formalization
AI safety startup Resolution demonstrated the use of agents to automatically formalize complex mathematical statements from statistical learning theory, such as resolution of singularities. This work aims to establish a rigorous science of research automation through the 'industrialization of mathematics,' laying groundwork for understanding the relationship between loss landscape geometry and generalization.
Full Report
Welcome to Import AI, a newsletter about AI research. Import AI runs on arXiv, cappuccinos, and feedback from readers. If you’d like to support this, please subscribe. How math could help alignment:*…What the “industrialization of mathematics” means for safety…*AI safety startup Resolution (formerly known as Sequent, Import AI 461) has published work on how it has automatically formalized some mathematical statements related to statistical learning theory. Specifically, the team has autoformalized the resolution of singularities, which they believe “lays the groundwork for further automated research into the relationship between loss landscape geometry and generalization.”
How they did it: I’ll skip over the math and concentrate on how they did it, which gives us some broader lessons for how people are using AI systems to push on the frontier of knowledge. A Resolution researcher “started by working with agents to develop two plans: a high-level, human-interpretable version and a detailed (112-page) plan divided into atomic steps that closely followed the existing literature,” they write. The researcher “then deputized an orchestrator agent to carry out the plan, spinning up agents to do pen-and-paper math, write Lean, and handle support functions like checking that things were staying on track… the execution phase required little scaffolding beyond the initial plan and some agent skills distilled from earlier internal autoformalization efforts.”
**$135k for math formalization:**The work took about a week, taking “on the order of 100B input tokens (90% cache reads) and about 300 million output tokens (totaling an estimated $135,000 in token spend), and produced about 600k lines of Lean.” Now that they’ve done this, they’ve been able to accelerate some other aspects of their research: “We have already seen both benefits from autoformalization in using this library to extend parts of singular learning theory. Formalizing resolution of singularities lets us automate more of the theory, for example, to better understand sampling, and that understanding is what lets us shape how models learn, which is the goal of what we call patterning”.
Why this matters - perhaps the math boom will help us make safe AI: Though frontier mathematics often seems disconnected from immediate advances in other fields, posts like this highlight how the two might converge. The key point here is that AI is making it possible to do things that were previously so unbelievably expensive and human-time-intensive that very few people did them and you couldn’t easily integrate them into the research roadmap of a startup - but that has now changed. “We expect the coming industrialization of mathematics to make possible a new, rigorous science of research automation,” Resolution writes.