Verification

When can an answer be checked more cheaply than it can be produced? The answer decides how fast AI that accelerates research can go while every step stays checkable by people.

The question

Some answers are much easier to check than to find. A proof can take years to find and far less time to check, line by line. A filled-in sudoku takes a minute to check, however long it took to solve.

Complexity theory makes this precise. For the problems in the class NP, a proposed answer can be checked quickly. For the hardest of them, the NP-complete problems, no fast way to find one is known. Whether one exists is the P versus NP question, which is open.

We ask the same question of the work language models now do: reading, arguing, proving and writing code. For which of those tasks can an answer be checked more cheaply than it can be produced, by how much, and with what in hand?

Why it matters for the loop

AI that accelerates research, including research on AI, is a loop: each turn's results are the next turn's starting point. For people to check every turn, checking has to cost less than producing, and keep costing less as the loop speeds up.

Where the gap is wide, a person, or a simpler program a person trusts, can check each turn and the loop can move fast. Where it is narrow, checking takes as long as the work, and the loop either slows down or goes unchecked. Knowing which tasks fall where tells us where the loop can run and where it has to wait for people.

Fig. 1 · IllustrativeThe question, not a result. For some tasks the cost of checking an answer grows far more slowly with difficulty than the cost of producing it; for others it may not. The drawing carries no data, and a result from the program will replace it.

The approach

Theory: We compare the cost of checking with the cost of producing for the kinds of reasoning models are asked to do, and ask what a check needs in hand: a proof, a worked solution, or a quote from a source.
Evaluation on real models: We test what the theory predicts on real language models, with evaluations that isolate one question at a time and are sized in advance, so that the result can confirm or refute the prediction.
In the Serre platform: The platform already relies on one cheap check. A claim taken from a paper is kept only if its quote is found in the paper's text: finding the claim takes reading the paper, and checking it takes a search.

Outputs

In progress. Nothing from this program is published yet: no paper, preprint or dataset. Our first publications are in preparation, and each will be listed under publications as it is released.