Chief Scientist at the UK AI Safety Institute (AISI). Previously, DeepMind, OpenAI, Google Brain, etc.
Geoffrey Irving
Karma: 1,725
Thousand-dimensional structure
Announcing our $160M grant from Coefficient Giving
Thank you for the report! We haven’t heard this from anyone else; do you have any other details that might help us diagnose? CC @Jesse Hoogland for visibility. If it seems isolated we may triage and hope it resolves with time.
Geoffrey Irving’s Shortform
We’re changing our name: Sequent is now Resolution.
Two weeks ago, we launched Sequent, a new alignment research organization working on a portfolio of ASI safety bets. Following our announcement, we discovered ⊢ Sequent, a formal verification startup launched only about a month earlier! And by a friend and former colleague, no less! After discussing it with the other ⊢ Sequent, we decided that the best course of action was to change our name. This brings us to Resolution (resolution.org).
Go check out Sequent! They’re going to do exciting things with formal verification too. And go check our new website! We’ve just posted new positions and opened our first hiring round.
http://resolution.org/careers
Of course, no name would be complete without fun stories! We have two:
1. Resolution as in the resolution algorithm in first-order logic, one of the foundational methods of generating proofs.
2. Resolution as in resolution of singularities: any singular variety can be reparameterized into a nonsingular form for easier analysis. Which is also a metaphor for the AI Singularity: let’s try to the untangle that limit into forms that can be analyzed more rigorously.
“Did you lie?” Evaluating Lie Detectors across Model Scale and Belief-Verified Model Organisms
Resolution (fka Sequent): scale and automation for higher confidence in alignment
Automated Alignment is Harder Than You Think
Bringing More Expertise to Bear on Alignment
Research Areas in Cognitive Science (The Alignment Project by UK AISI)
The Alignment Project by UK AISI
I think both protocols mentioned (MIP* = RE and the pointers one) already do what you want here. In the background the provers have to do unbounded work to prepare for the stuff they show the verifier, but the verifier’s work is limited to a fixed polynomial in the input size.
And more strongly: in the pointer version where we have two competing provers, a malicious prover can’t force an honest prover to do significantly more work than would be required in an honest case.
The need to relativise in debate
I would love the two of you (Beth and @Jacob Pfau) to talk about this in detail, if you’re up for it! Getting the experimental design right is key is we want to get more human participant experiments going and learn from them. The specific point of “have a high standard for efficacy” was something I was emphasising to Jacob a few weeks ago as having distinguished your experiments from some of the follow-ons.
I think this maybe a forest vs. trees thing where we failed to say the thing explicitly because we’ve been intentionally living in the “Alice and Bob have similar heuristics and computational power” for years: the set in the paper models the set of heuristics, but I am surprised that the term “heuristic” ended up not in the final text (we just speak a lot about relative computational resources).
Fundamentally if you let B attend to either A’s thoughts or to A’s context and also ensure A and B are similar, we think A shouldn’t be able to hide things from B. If A is a very different model, or a stronger model, this won’t hold, and we should expect arguments which A can navigate in ways B can’t defend against. So in order to get anything like this to go through you need some kind of “B knows what A knows” invariant.
The setting is where A and B have access to the same set of heuristics. This is modeled explicitly in the paper as a shared set of functions they can call, but corresponds to them being the same model or similar for LLM training.
The requirements are stability, compactness, and A-provability (meaning that the first player Alice knows how to correctly answer claims). It’s important that A-probability is a requirement, as otherwise you can do silly things like lifting up to multilinear extensions of your problem over finite fields, and then there will always been lots of independent evidence which can be turned into stability.
I agree with this! On the empirical side, we’re hoping to both get more human participant experiments to happen around debate, and to build more datasets that try to probe obfuscated arguments. The dataset aspect is important, as I think in the years since the original paper follow-on scalable oversight experiments (debate or not) have been too underpowered in various ways to detect the problem, which then results in insufficient empirical work getting into the details.
One way to think about amplification or debate is that they’re methods for accelerated evaluation of large computations: instead of letting the debaters choose where in the computation to branch, you could just take all branches and do the full exponential work. Then safety splits into
1. Are all perturbations of the unaccelerated computation safe?
2. If we train for debate, do we get one of those?
If humans are systematically biased, this can break (1) before we get to (2). It may still be possible to shift some of the load from the unaccelerated computation to the protocol by finding protocols that are robust to some classes of systematic error (this post discusses that). This is a big issue, and one where we’ll be trying to get more work to happen. A particular case is that many organisations are planning to use scalable oversight for automated safety research, and people love to be optimistic that new safety schemes might work.
We’ll model the verifier as being in P, and the prover as being in...