Announcing Formal Verification at RESI (The Institute for Responsible Superintelligence)

This post is crossposted from my Substack, Structure and Guarantees, where I explore how formal verification and related ideas might scale to more complex intelligent systems. This article is a little different from usual: it’s an announcement of a new working group studying how to get formal methods off the ground, for pervasive use to address current concerns around cybersecurity and AI coding agents (and beyond).

There’s a lot of excitement and worry at the moment about OpenAI agents hacking into Hugging Face, as an example of increasingly powerful AI creating cybersecurity threats that feel fundamentally new. I’ve already written about how there are actually new opportunities we should seize for defenders, so the balance of power need not shift in favor of the bad guys. Formal verification is a secret weapon whose time has come. It even gives some important security theorems almost for free! In the case of that recent OpenAI-Hugging Face incident, a relevant application would be provably enforced containment (a case of guaranteed safe AI), whether within an evaluation environment or a production system. This kind of theorem can promote safety independently of what goes on within mysterious decision-making black boxes like deep neural networks.

I’m excited to announce here a new initiative to figure out the contours of an effort to ramp up related formal-methods work quickly and effectively. RESI, the Institute for Responsible Superintelligence, was recently kicked off, and you can read about it in the words of Chief Scientific Officer Adam Kalai. Let me tell you a bit about it from my perspective, before describing the working group I’m running to study formal verification to promote AI safety.

RESI

There sure is a lot of attention to AI safety at the moment. Many discussions include a (justified) sense of urgency. The problem with excessive urgency is going after simple, quickly deployable, but incomplete solutions. Ideally we would have safety approaches backed by solid mathematical theorems, a goal that often feels impossible when it comes to, for instance, directly constraining the behavior of large neural networks.

RESI is a new nonprofit aimed at tackling just those challenges. The DNA of the leadership is in theoretical computer science, especially cryptography, which has a track record of not just arguing that certain impossible-sounding goals are possible but also of backing up those claims with rigorous proof. Besides Kalai who I already mentioned, the other cofounders are my cryptographic MIT colleagues Shafi Goldwasser and Vinod Vaikuntanathan.

I like to say, mostly seriously, that Greater Boston gets just enough real winter weather to filter out people who aren’t ready to tolerate a little discomfort in service of a larger goal, like working on research that may take a bit to pan out legibly to the rest of the world. The same filter that is helpful for e.g. recruiting the right PhD students also plays into the great choice of a physical headquarters for RESI! At the same time, for grounding in practical relevance, there are plenty of extremely local connections into the tech industry, in RESI’s home of Kendall Square, MIT’s backyard, “the most innovative square mile on the planet.” All the major players in biotech and pharma have offices there, which reportedly explains Anthropic’s opening of an office that happens to be just a few blocks from RESI. There are large offices for Google, IBM, Meta, and Microsoft in Kendall Square itself, with Amazon also in walking distance and AMD, Nvidia, and Oracle in driving-commute range. Add in quite a mass of world-class universities in literal walking distance (assuming moderate physical fitness), and we have a recipe for thinking deep thoughts calibrated to have impact.

The Formal-Verification Working Group

One of the main activities of RESI is working groups, where world experts on important topics adjacent to AI safety meet regularly in person to build intellectual frameworks to guide progress. I’m excited to be chairing a working group on formal verification. The central question is how should formal verification be applied to allow the use of powerful AI throughout software development without creating new risks of cyberattacks or otherwise dangerous behavior? We’ll consider the question from today’s deployed systems to potential intelligence explosions as AI rapidly builds its own superhuman successors.

The specifics of the framework we build will depend on the members of the working group, but let me share my own starting thoughts. First, the scope includes both technical questions, of how software development and formal methods should be designed; and organizational questions, of how we organize the right people to create the right formal artifacts quickly enough, ahead of looming risks. That last part is tricky, considering I just argued an important focus of RESI is being willing to think a little longer than for most AI-safety efforts, to get strong theoretical guarantees! One mitigation is identifying useful work at different levels of readiness to begin. The increasing attention to deliberate slowdowns in frontier-model development may also allow more breathing room than worst-case planning has considered, which gives more-principled techniques time to develop.

What would a kind of open, distributed Manhattan Project in this space look like? I see three main tiers, going from most conventional to least. They’re drawn here going from bottom to top to indicate the magnitude of divergence from where formal methods is already headed.

First we have the classic challenges of formal verification of full-stack systems infrastructure. Almost from the beginning of computers as we know them in the middle of the 20th century, there was theoretical work on rigorous proof of program correctness. There have long been advocates for applying those methods to critical digital infrastructure, and indeed, circa the year 2000, we saw examples in safety-critical domains like avionics (one example here). The approach grew significantly in real-world usage as technologies like SMT solvers and separation logic appeared or scaled in the 21st century. As a result, there is a medium-sized population of trained true believers, ready to verify all important digital infrastructure and even connect such results into end-to-end theorems. I will claim that, compared to the next two tiers, this one is relatively predictable and shovel-ready, in terms of potential to get more work going quickly through funding and education about effective use of AI coding assistants.

Next we have the specific infrastructure of deep learning. The classic problems of formal verification are hard enough that experts stick with them for decades, and relatively few have moved onto the newfangled kinds of infrastructure behind, say, LLM serving. We have GPUs, CUDA and other frameworks/languages for programming them, plus all of the infrastructure for, say, scheduling and cybersecurity of data centers. The overlap of knowledge of these components with deep formal-verification knowledge is relatively little, but I believe that intersection could be grown rapidly with the right encouragement. It seems feasible to me to have end-to-end formal verification of much of the infrastructure of state-of-the-art deep-learning data centers, on top of which governance mechanisms and their proofs can be added. That is, we should be able to prove that something approaching a full data center implements a mathematical model of running linear-algebra expressions or whatever, along with all control systems that decide which models to run on which input data when. For instance, there has been a lot of thinking around how to enforce treaties that limit strength of deployed AI systems. Formal methods can help ensure such enforcement is implemented correctly, perhaps in the form of open-source code that mutually distrusting actors must all come to endorse, say thanks to collaborating on a common proof of it. Plenty of formal-methods experts will be excited to learn more and contribute, and the challenge is one of technical education about the problems and techniques, in partnership with experts on this kind of infrastructure.

Finally we have verification of recursively self-improving systems for responsible superintelligence. The mainstream of formal verification is used to dealing with twistily self-referential systems, like compilers that compile themselves, which may supercharge their own performance over time, if optimization involves any kind of search with a fixed budget of time or memory. However, there are new challenges of systems that repeatedly improve themselves, especially with regard to real-world decision-making. These challenges are conjectured to be at the center of making it safe to take full advantage of AI through properly controlled intelligence explosions. Now one problem is that probably most experts on formal verification aren’t yet convinced that such ideas have become practically relevant and aren’t just “science fiction.” Even people who buy into the importance will often not feel very oriented on exactly how one would start attacking the problem formally. So taking a stab at designing a framework and building consensus around it would be one goal of the working group. Another would be brainstorming about ways to educate formal-methods experts on the topic and ways to facilitate support, financial and otherwise, for related efforts.

Conclusion

I’m looking for members of the working group who have not just the relevant expertise but also pass a seniority bar similar to the one we associate with conference program committees (the folks who carry out peer review in top publication venues). So, e.g., most students wouldn’t qualify, though we may decide to organize events that invite the community more broadly. I should also emphasize that the process is intended to take place mostly in in-person meetings in or near RESI HQ in Kendall Square, so we probably won’t want working-group members who can’t plausibly make day trips to participate (even if such trips happen relatively infrequently). People who aren’t scared off by those constraints I’m very glad to hear from, regarding interest in joining the working group.

The next post will make an independent proposal in the third tier above, about how to use formal verification to set up a useful kind of recursive self-improvement, connecting to my recent ranting about rethinking the hardware-software interface. We’ll think about how to structure code optimization on top of fixed hardware in a way that delivers real value while avoiding classic AI-safety gotchas.