Counterexamples to a best-of-n win-rate bound at every budget

Dev D. Goyal

Counterexamples to a best-of-n win-rate bound at every budget

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Problem and result

Problem: Beirami et al.'s best-of-n win-rate versus KL divergence conjecture (Conjecture 7.2)
Posed in: Beirami et al., ICML 2025 (PMLR 267), Conjecture 7.2 and Eq. (28)
Status: Disproved
Result: For every budget n ≥ 2 and cap δ > 0, a finite reference law with all probabilities ≤ δ has a best-of-n policy with D < ℓ(W), violating W ≤ ℓ⁻¹(D); for n = 2, p = (2/5,1/5,1/5,1/5) gives W = 163/250.

Abstract

For every n≥2 and δ>0, there is a finite positive reference distribution whose largest atom is at most δ and whose best-of-n policy violates the proposed divergence–win-rate curve. A four-response best-of-two example gives exact probabilities and a strict logarithmic certificate. The proof uses finite interval bounds and gives a quantitative positive gap. It does not determine the sharp replacement curve.

Details

Year: 2026
Discipline: Theoretical computer science
Area: Sampling algorithms and information theory
Subject: Sampling algorithms and information theory
Result type: Disproof for every budget n≥2 and every positive atom cap
Formal proof: Shared Lean library
Family: best-of-n
Keywords: best-of-n sampling, win rate, KL divergence, language model alignment, counterexample

Statement and scope

Result summary. The catalogue summary repeats the abstract above, including its stated limits. The formally checked statements are listed under Formal proof.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 266 KB
PDF on GitHub: papers/theoretical-computer-science/best-of-n/paper.pdf
LaTeX source: papers/theoretical-computer-science/best-of-n/paper.tex
Bibliography: papers/theoretical-computer-science/best-of-n/references.bib

Formal proof

The selected theorems of this result are proved in the shared Lean 4 library of the repository. Its Comparator configuration checks each one against the matching statement in the Challenge module and permits only the axioms propext, Classical.choice and Quot.sound.

Proof module: lean/MathAndTheory/TheoreticalCS/BestOfN/Extension.lean
Family sources: lean/MathAndTheory/TheoreticalCS/BestOfN/
Challenge: lean/Challenges/TheoreticalCS/BestOfN/Main.lean
Solution interface: lean/Solutions/TheoreticalCS/BestOfN/Main.lean
Comparator file: lean/comparator/theoretical-computer-science/best-of-n.json
Statement guide: lean/docs/theoretical-computer-science/best-of-n.md
Toolchain: leanprover/lean4:v4.35.0

Checked theorems

Namespace MathAndTheory.BestOfNExtension

BestOfNChallenge.result
BestOfNChallenge.every_budget_small_atoms

Reproduce

The commands below are quoted from papers/theoretical-computer-science/best-of-n/verification/README.md, which gives their context and working directory.

Reproduce the computations

python3 papers/theoretical-computer-science/best-of-n/verification/scripts/verify.py
python3 papers/theoretical-computer-science/best-of-n/verification/scripts/extension.py

Reproduce the formal checks

cd lean
lake exe cache get
lake build MathAndTheory.TheoreticalCS.BestOfN.Extension Solutions.TheoreticalCS.BestOfN.Main
lake env lean Solutions/TheoreticalCS/BestOfN/Main.lean

Reproduce the formal checks

bash scripts/verify-comparator.sh comparator/theoretical-computer-science/best-of-n.json

README: papers/theoretical-computer-science/best-of-n/README.md
Verification guide: papers/theoretical-computer-science/best-of-n/verification/README.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Original problem. Beirami et al., ICML 2025, Conjecture 7.2 and equation (28).

Questions and answers

Is the best-of-n win-rate conjecture of Beirami et al. true?

No. This preprint shows that Conjecture 7.2, W ≤ ℓ⁻¹(D) with ℓ(w) = log(w/(1−w)) + 1/w − 2, fails for every budget n ≥ 2, even when every reference probability is at most any prescribed δ > 0. The source's proved upper bounds on divergence and win rate remain valid.

What is the simplest counterexample?

Best-of-two with reference probabilities (2/5, 1/5, 1/5, 1/5) gives the selected law (4/25, 5/25, 7/25, 9/25), win rate 163/250 and ℓ(W) − D > 1/2445. The paper does not determine the sharp replacement curve.

Is the proof formally verified?

Yes. Lean 4 proves the four-response counterexample, its inverse-curve consequence and the every-budget theorem with arbitrarily small atoms. The preprint itself has not been refereed.

Cite

Citation file papers/theoretical-computer-science/best-of-n/citation.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026bestofn,
  author = {Dev D. Goyal},
  title = {Counterexamples to a best-of-$n$ win-rate bound at every budget},
  year = {2026},
  month = oct,
  howpublished = {Preprint},
  version = {1.0.0},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/theoretical-computer-science/best-of-n},
  note = {Preprint, 26 October 2026. Not peer reviewed. Includes a Lean 4.35.0 formalization. See the collection's authorship disclosure for the autonomous research process.}
}