Shafi Goldwasser, Orr Paradise
We study when and how AI systems can prove that their outputs are correct, bringing the tools of probabilistic proof systems and complexity theory to bear on AI safety. Our contributions are primarily theoretical, in the form of new definitions, constructions, and techniques, but the work is empirically guided: we run experiments on frontier models and on tiny "fruit-fly" models to test intuitions, and papers often pair a theorem with an experiment.
Stream overview
We are in Self-Proving models, and along the way in accelerating research at the interface of theory and practice (e.g. by way of harnesses). In Self-Proving models, here are a few example projects:
1. Implement the probabilistic-consistency proof system. We recently constructed a proof system with which a predictive model can prove that its probabilistic claims are self-consistent, with the verifier explicitly designed for implementation. The goal of this project is to build that verifier, then train a small prover (order 10M-100M parameters) against it via Transcript Learning or RLVF, and measure verifiability, i.e., the fraction of outputs the verifier accepts. This connects to the aforementioned collaboration with Cambridge, which the scholar could join.
2. Verifier hacking, in theory. RLVR as used in practice trains models against verifiers with no soundness guarantees. When does training against such a ""verifier"" result in a model that games it? In a stylized model, I have preliminary results showing that even benign training dynamics can inadvertently select a cheating prover, and that which prover is selected depends on fine features of the training setup (for instance, the noise structure). The direction is concrete but wide open: one could relax the fairly stringent assumptions the current theory asks for, or go empirical and test whether the phenomenon occurs in actual RLVR training. The destination is a characterization of when verifier-based training is sound: a theory of reward hacking for verifier-based training.
3. Universal Self-Proving models. The theoretical guarantees of Self-Proving models currently hold when trained against one fixed verifier. Can a single model prove its answers to verifiers specified in-context, including ones unseen during training? Mostly empirical (train across a family of proof systems, test generalization to new ones), with theory questions available close-by: what does in-context generalization over verifiers require? Presumably, a restricted class of verifiers (e.g. low-depth circuits) but can we say something more?
The list above is a suggested menu, certainly not a mandate. In our experience, projects are most effective when they are driven by the student's curiosity. Our preferred mode of advising is to be of service to the student: to let them follow the directions they find most interesting, mysterious, or promising, and to be there as a sounding board, friendly critic, verifier, etc.
Standard (1-2 hours of weekly 1:1s)
Boston
Indifferent
Strong preference
Mentors
Shafi Goldwasser is the C. Lester Hogan Professor in Electrical Engineering and Computer Sciences at the University of California, Berkeley, the RSA Professor of Electrical Engineering and Computer Science at MIT, and directs the Simons Institute's resilience research pod. Goldwasser is a cryptographer, and a co-founder and chief scientist of Duality Technologies.
Orr Paradise is a scientist at EPFL, appointed in its Theory of Machine Learning Laboratory and its Verification and Computer Architecture Lab. Paradise is also a researcher on Project CETI's theoretical analysis team, working on the machine analysis of sperm whale communication.
Fellows we are looking for
- Experience with theoretical computer science. Ideally a university-level course in computational complexity theory, cryptography, or a comparable theory course. At minimum, the candidate should be comfortable with the standard toolkit: NP-completeness, basic probability and concentration bounds, and the definitions of interactive proofs. We are aware that such courses are not always offered, especially for candidates from a non-traditional CS background. That is fine, but the candidate must demonstrate that they have already put in serious effort to learn this material and will have covered it by the start of the stream.
- Mathematical maturity: the ability to prove theorems and to verify a given proof. This is commonly obtained through university-level courses in mathematics, for example set theory, abstract algebra, combinatorics, or probability theory. Relatedly, we care a great deal about intellectual honesty. A half-finished or LLM-generated proof presented as complete is a serious red flag. Saying "I don't know" or "I could not close this step" is always the right move; using an LLM as a shortcut and then being unable to explain the result is not, (unless the tooling itself is explicitly the contribution).
- A clearly stated reason for pursuing research with us. We are much more interested in candidates who make a compelling case for working at the intersection of complexity theory and AI safety than in generically strong candidates who would be indifferent between our stream and others. We want to make sure this opportunity, both the student's and ours, is used well.
- Basic coding ability (see also Preferred Qualifications).
- Ability to conduct research independently. We are here to collaborate, guide and support, but we cannot manage the fellow's time or check in constantly. The fellow must be able to push a project forward on their own, recognize when they are stuck, and know when and how to ask for help.
- Experience or demonstrated interest in probabilistic proof systems (the sum-check protocol, PCPs, zero-knowledge proofs).
- Strong technical writing ability and a desire to write. A published paper, especially in theoretical computer science, is usually evidence of this, but other forms count too: long-form essays, technical blog posts, theses.
- Experience training small models (PyTorch, RL fine-tuning, evaluation pipelines).
- Experimental taste: the ability to design a small experiment that actually tests a theoretical claim, rather than one that just produces plots. Much of our empirical work is on small models and exists to sharpen intuition about what a theorem should say.
- Ability or interest in responsibly and effectively accelerating research using AI. Put bluntly: it is all too easy nowadays to vibe-code slop that resembles a valid technical artifact and disintegrates on closer examination. Spending the time to engineer a system (for example a harness) that is of real help for theoretical research is impressive. A non-trivial Lean-based autoformalization harness would be one such example.
- Ability to work across the theory/practice divide: explaining the conceptual/technical heard of a theorem, or an experimental result to a theorist.
- Problem taste. Our advising philosophy is that projects should be driven by the student's curiosity.
- Comfort with the intrinsic difficulty of research. Most of the time things will be uncertain and progress will be slow. We want fellows who can stay focused on the curiosity and beauty of the questions rather than give up when stuck, and who bring a constructive attitude to AI safety.