Proof-Carrying Optimality for Finite Identification under Bounded Adversarial Answer Errors
Independently checkable upper and lower certificates for exact finite-identification query complexity
Vikram Lex
Public preprint posted on Zenodo in July 2026. The journal manuscript is under review at the Journal of Machine Learning Research.
Zenodo · Under Review at JMLR
Paper Summary
Finite identification asks a learner to determine an unknown behaviour using probes from a fixed alphabet when an adversary may corrupt up to b answers. Exact worst-case query complexity is the value of a large minimax game, so an optimum can be expensive to reproduce. We develop proof-carrying methods for many-valued behaviour tables. Portable certificates combine a noiseless strategy with a small lower witness to prove an affine identity OPT_A(b) = αb + β for every budget, with proof size independent of b. Expanded certificates pair a robust strategy at one budget with an adversary DAG closed by analytic lower bounds. We also provide independently checkable lower bounds and certificates for the non-adaptive optimum. All 30 cells in a 15-instance primary matrix at b ∈ {0,1} receive two-sided optimality proofs. A 101-instance sweep across b ∈ {0,1,2} proves 300 of 303 declared cells, leaving three explicit resource-limit outcomes. At b = 2, adaptivity strictly improves on the exact non-adaptive optimum in 91 completed cells, by as many as 84 probes. Replay is faster than synthesis in 29 of 30 timed primary cells, although the largest accepted lower certificate contains 8.9 million moves. These results make query-complexity claims auditable while exposing proof construction and proof size as bottlenecks.
Proof-carrying Optimality
Untrusted search constructs candidate strategies and witnesses; a separate verifier recomputes and replays the supplied evidence without repeating synthesis.
Declared Identification Game
The input is an explicit many-valued behaviour table with a fixed probe alphabet and a declared adversarial error budget. The target is exact worst-case adaptive or non-adaptive query complexity.
Portable and Expanded Strategies
Portable certificates prove affine all-budget identities from a noiseless strategy and lower witness. Expanded certificates encode a robust strategy for one budget when a compact all-budget proof is unavailable.
Adversary and Cover Certificates
Replayable adversary DAGs, analytic closures, and non-adaptive cover evidence independently establish matching lower bounds, allowing the verifier to accept an optimum or reject with a reason.
Proof Coverage
Completed cells carry matching upper and lower evidence; incomplete cells remain explicitly identified as resource limits rather than inferred values.
Primary Matrix
15 instances at adversarial error budgets 0 and 1
Every declared primary cell receives both an accepted strategy certificate and a matching lower-bound certificate.
Certificate replay is faster than constructing the result in 29 of 30 timed primary cells; timing observations are descriptive and come from two machines.
The largest accepted lower certificate contains 8.9 million moves, exposing proof size as a practical bottleneck even when verification avoids search.
Declared Sweep
101 instances across adversarial error budgets 0, 1, and 2
The sweep proves 300 of 303 declared cells. The remaining three are reported as resource-limit outcomes, not estimated optima.
At error budget 2, adaptivity strictly improves on the exact non-adaptive optimum in 91 completed cells.
The maximum certified adaptive advantage is 84 probes relative to the exact non-adaptive optimum.
Verification Scope
What the certificates do and do not establish
All claims concern an explicit finite behaviour table and its declared probe alphabet; the largest primary table has 49 classes and 220 probes.
Verification is polynomial in the explicit table and supplied proof, not necessarily in a succinct description of the underlying game.
Resource exhaustion remains a first-class reported outcome rather than being converted into an unsupported query-complexity value.
Cite This Paper
@misc{lex2026proofcarrying,
title={Proof-Carrying Optimality for Finite Identification under Bounded
Adversarial Answer Errors},
author={Lex, Vikram},
year={2026},
month={jul},
publisher={Zenodo},
doi={10.5281/zenodo.21651833},
url={https://doi.org/10.5281/zenodo.21651833},
note={Preprint; manuscript under review at the Journal of Machine
Learning Research}
}