Verify, Then Vote

An answer you can build on

Verify, Then Vote is our first paper, and we are excited to put the whole project on GitHub: the manuscript, proofs, implementation, and experiment records. It grew out of a question we could investigate on a local machine, and ended up connecting the practical pleasure of an overnight model run with a more precise way to reason about its decisions.

There is something satisfying about giving your own machine a substantial job, leaving it to work, and coming back to a result you can investigate. Local models make that rhythm available for experiments too. An overnight run can turn a question into thousands of answers, complete with the messy disagreements that make the next question interesting.

We wanted to explore a simple idea: if several models disagree, can checking their evidence help us choose a better answer? A majority vote is an easy starting point. But five models can share a mistake. Counting agreement tells us what they said; we still need to investigate what supports it.

The result was a decision rule whose evidence we could inspect, test, and reuse. We could ask whether it chose better answers, identify the checks behind each change, and return to the same experiment with a different rule.

Source: Results, harm test, and replay · Models and evaluation methods

Five models, one local machine

We started with Llama 3.2 3B, Mistral 7B, Gemma 2 2B, Phi-3 mini, and Qwen 2.5 3B. The group fit a local-machine budget while giving us several model families to compare. We wanted enough disagreement to study, without turning answer collection into a cluster-management project.

Our run design used an Apple M3 Pro with 36 GiB of memory. Ollama served the local models. We recorded model digests so that a model name was not the only record of what had actually run. Temperature was 0.7 and a fixed seed was used; the collection also recorded request ordering and arrival ordering.

The source checker was a separate, hosted model, Claude Sonnet 5.5. The small local models gave us a varied group of answer generators; checking their cited passages used the hosted model. We kept both parts of the work so that we could examine how the final choice was made.

Local computing was particularly nice for the long collection runs. We could give the machine a queue and let it work while we did something else. The recorded primary collection session spans roughly eight hours. That is the kind of workload that fits an overnight computing habit: the machine does the repetitive part, and the human returns for the interesting part—finding out what happened.

Source: Models and evaluation methods · Local run design and hardware

Give every answer something to point to

Each model worked in two turns. First it wrote a search query, limited to twelve words. Retrieval returned five passages. Then the model answered the question, stated a confidence level, and cited up to three of those passages. That made the citation a concrete part of the saved output, rather than a vague suggestion to look something up later.

The workload covered factual questions, claim verification, scientific claims, and multiple-choice questions. Retrieval used BM25 over Wikipedia passages for most tasks. Scientific claims used research abstracts, with BM25 or embedding search selected by a seeded draw. Keeping retrieval in the record meant we could distinguish a bad search from a bad reading of a useful passage.

When an answer failed, we could trace it back through retrieval and citation. Sometimes the useful material never reached the model. Sometimes it was there, but the proposed answer or its citation did not follow. Those are different problems to fix; collapsing them into a single accuracy score would have hidden the distinction.

The checker examined the cited passage against the proposition it was supposed to support. It did not see the dataset’s correct answer. Its checks were still model judgments, not proof, but they gave the decision rule something more specific than a confidence score or a vote count.

Source: Models and evaluation methods

Make an overturn accountable

We turned those checks into an explicit rule. Start with a default answer from the vote, using a fixed policy to settle ties. An alternative can replace it only if one of its passages carries a support label from an accepted checker. Every replacement records the passage and label that allowed it.

We proved a precise property of that rule and checked it in Lean 4: if it replaces a correct default with a wrong answer, that wrong answer must have passed verification. This gives an auditor a specific place to investigate the failure: the answer, passage, and accepted checker label behind the change.

The guarantee describes the decision rule under its stated assumptions. A checker can misread a passage, and a source can be wrong. How often those failures occur still has to be measured. The useful result is that the rule makes the evidence permitting an overturn explicit and available for inspection.

Source: The decision rule and its formal guarantee · Proof catalogue and Lean 4 implementation

Make the comparison fair

We ran each decision method against the same saved answers and retrieved evidence. That held the inputs steady while we changed the selector. It also meant a promising variant could be compared directly with the original, instead of triggering another round of answer generation.

We also separated development from evaluation. Development questions were where we chose settings; the evaluation collected answers to 1,000 primary questions. The primary comparison focused on 526 questions where the models had proposed both correct and incorrect answers. Those mixed cases are especially useful for studying how a rule chooses between alternatives.

Before treating an improvement as a success, we also wanted to know how often the rule damaged a majority that was already right. A system can fix many mistakes and introduce new ones at the same time. Recording both lets us ask a more useful question than whether the final percentage went up.

Source: Results, harm test, and replay · Models and evaluation methods

What changed when we checked

Checking the evidence helped. Across 1,000 primary questions, the original rule raised accuracy from 77.1% for majority vote to 85.0%. That gave us a promising result to investigate—and a record detailed enough to see how the improvement happened.

On 526 questions where the models proposed both correct and incorrect answers, the rule corrected 91 wrong majorities. It also changed 12 right majorities into wrong answers. Some of the gain against the majority baseline came from a different way of breaking ties; it would be misleading to credit all of it to checking the sources.

We also checked whether the passages were doing real work. In a later control, we withheld the cited text or replaced it with unrelated text and ran the checker again. Replaying the decisions with those replacement labels eliminated 76 of the original 91 corrections. This showed dependence on the supplied passages in the tested decisions; it does not rule out influence from the checker’s learned knowledge when relevant text is present.

We also tested whether the gains came with too many avoidable mistakes. The rule harmed 12 of the 376 initially correct majorities: an observed rate of 3.2%. Its upper confidence bound was 5.5%, above our preset 5% ceiling, so the original rule failed that test. Having the individual decisions let us investigate the failure rather than stop at the average.

We then tried a more conservative rule: keep the initial answer when it has verified support. With a second group of five models, it corrected 73 wrong majorities and overturned three right ones, raising accuracy on mixed-answer questions from 73.1% to 85.9%. Its harm-rate upper bound was 2.2%, below our preset 5% ceiling. We specified this revision before collecting the second pool, but those models answered the same questions and reused some earlier checks. This tests transfer across models; performance on unseen questions remains open.

Source: Results, harm test, and replay

A useful surprise

We also asked Sonnet to choose directly from the proposed answers and passages. On the first pool’s 526 mixed-answer questions, that judge reached 93.9% accuracy against our original rule’s 86.5%. It cost less for a first decision, too. These were choices among answers already generated, not a comparison of complete systems starting from nothing.

On first-decision accuracy and cost, the judge won this comparison. Our method also gave us an explicit policy and a record of the passage behind each overturn. We could inspect those choices, then change the rule or the participating models without paying for the same checks again. That made the next experiment a concrete part of the result.

Source: Results, harm test, and replay · Models and evaluation methods

The next experiment starts here

Because we saved the answers, passages, and checks, we could change a decision rule or leave out a model without asking the checker to do the same work again. In one analysis, we removed each model in turn and replayed 3,510 decisions in 23 seconds, with no new model calls.

All 1,100 benchmark decisions reproduced byte for byte from their saved inputs under the same policies. The released artifact includes the records and analysis scripts so others can reconstruct the results without running the models again.

That reuse has a boundary. A new answer or passage may need a new check. The replay savings do not cover generating the original answers, collecting the evidence, or building the project.

This is what we want to keep building on: an explicit decision policy, evidence we can audit, and an experiment that leaves the next experiment cheaper to ask. The paper preserves the accuracy gains, the failed original harm test, the successful revised rule, and the stronger judge comparison so others can investigate the same tradeoffs.

Putting out a first paper also means letting other people into the work. Alongside the manuscript, the repository includes a proof catalogue and Lean 4 formalizations of the selection and gate guarantees, plus the code and recorded experiments. The formal results describe the decision rules under their stated assumptions; the experiments show what happened when we ran the models. Both are there to explore, question, and build on. We would love to see what someone tries next.

Source: Results, harm test, and replay · Reproducible artifact · Proof catalogue and Lean 4 implementation