Project summary

We currently lack formal verification and provable guarantees for AI safety. 

AI safety today is largely post-hoc. We train models, then evaluate them for dangerous behaviours and misalignment. In other terms, our guarantees are empirical, based on a post-hoc evaluation. While this can catch a large amount of issues, this is not enough for the most critical applications. Nothing guarantees that we have covered all cases. 

As AI scales, the need for fully verifiable guarantees becomes crucial. And such guarantees are only given through formal verification, that guarantees behavior based on the characteristics of the trained model and the query. Just like statistical learning offers generalization bounds for classical machine learning, we need bounds for modern AI models. 

Why is this not possible now ? Deep learning theory is full of complex scientific problems, to which we only have partial solutions and approximations. The sheer scale of the task, and the complexity of the math, has so far made progress difficult. It covers topics ranging from optimisation to representation learning. Progress is fragmented, and all the possible paths cannot be investigated by human researchers. The math has to be extracted from a paper, verified and reviewed. Alternatives then have to be tested. Incremental progress is slow, yet the need is becoming more and more urgent.

This is the gap OpenTheory (open-theory.org) fills.

OpenTheory is an open mathematical project for deep learning theory. It offers:

• Formalization: We formalize deep learning theory in Lean4. Our proofs become fully checkable by machines.

• Conjectures : We formalize, mostly by hand, the conjectures and intermediate lemmas necessary for safe AI. All point towards the final goal, predictive alignment and safety bounds.

• Structured : We have a list of dependencies between proofs so the relevant proofs to work on can be quickly identified. 

• Compositional: We aim to cover AI in its diversity. We formalize neural network primitives, so we can support various components across architecture, optimizer, data, parametrization, and generalization. For instance, formalizing activation functions and MLPs.

• Coordination : We have a visual platform and an MCP. Ai agents can run the formalization along with humans. 

• Collaborative: Any researcher can contribute. Fully open source and open. 

The long-term goal is an open repository of deep learning theory for all. 

I am seeking funding for the first phase of OpenTheory on a subset of deep learning theory (representation learning).

What are this project's goals? How will you achieve them?

The goal of OpenTheory is to provide open source machine-verifiable proofs and mathematical guarantees for controllable AI outputs.

1. Verifiable Outputs: Provable guarantees for deep learning models, across the variety of architectures and tasks. In other terms, we have formal guarantees for safety.

2. Verifiable Controls: Developing formal verification techniques for causal modifications to steer model behavior.

3. Predicting Improvements: Theoretical predictions for cheaper and better training, cheaper inference, and better performance. 

How will this funding be used?

I am requesting between 15k$ and 50k$ for the initial six-month phase.

The funding would primarily on AI credits and and engineering time. It would allow me to use state of the art models to prove a subset of conjectures. It would also allow me work on OpenTheory instead of other projects.

The budget would cover:

• AI inference and API costs, compute and hosting;

• potentially researcher time or engineering contracts for Lean/formalization work;

Existing frontier models can be used for generation while Lean4 provides verification, so the tools are available, we mainly lack the resources. 

If the project receives only partial funding, I would prioritize a part of the core repository, verification pipeline and proofs in representation learning.

Who is on your team? What's your track record on similar projects?

I am currently leading the project. I am a CS PhD at Cambridge. My research is deep learning theory and on the mathematical structure of machine-learning tasks.  I have experience leading organisations and teams, both from my time in industry and in startups.  

The CS department at Cambridge is involved and interested. Amongst our first contributors, we have experts there in both deep learning and in formal methods, ranging from graduate students to professors.

For this first phase, however, we will keep the team lean and focus on demonstrating that the approach works.

What are the most likely causes and outcomes if this project fails?

There are several ways OpenTheory could fail.

1. Technical Difficulty.  Automated formalization of some conjectures can remain too difficult for models.

2. Field Velocity. The field is advancing fast. We need to keep up the formal guarantees too and we might lack the resources to cover an exponential increase in model capacity. OpenTheory would also need to scale autoformalization to keep up with the loop. 

3. Expert Opinion. We need experts to formalize the key conjectures for the model to prove. This means we need reliable expert opinions to help us out, which is a potential point of failure   

4. Impact.  Formal verification might apply only to a relatively narrow subset of the reasoning.  We ultimately care about AI safety, but even the tightest formal bounds might not have the impact we wish. This is unlikely but possible. 

Even if another lab formalizes these conjectures before us and open sources these proofs, we would still count this as a win and contribution to the ecosystem. 

If the strongest version of OpenTheory does not work, I expect the project would still produce useful outputs.

How much money have you raised in the last 12 months, and from where

OpenTheory has not yet raised external funding. I have developed the project independently with my own AI credits.