Efficient Prover–Estimator Debate via Signed Level-Set Optimization

Recursive debate makes complex claims verifiable by reducing them to subclaims that a human can eventually judge. Its weakness is obfuscation: a dishonest prover can hide an error among subclaims that an honest opponent cannot efficiently identify. Brown and Cohen introduced *prover-estimator* debate, replacing the search for a false subclaim with probabilistic predictions over all submitted subclaims. Their work showed that suitable probability estimators exist, but their argument uses reference answers unavailable to the estimator, which they note makes it non-executable, and provides a circuit-size upper bound exponential in the branching width. We here explore the conditions under which estimators can instead be constructed efficiently. When decompositions cannot profitably change the meaning of a claim, estimator construction reduces to local optimization guided by whether the prover alleges that the current estimate is too high or too low. Assuming efficient signed level-set optimization, our algorithm uses resettable access to a fixed prover and simulated debate scores, never hidden reference answers, and outputs an estimator satisfying a soundness bound against that prover, with construction and evaluation costs polynomial in the mechanism's parameters. Conversely, without this semantic restriction, a uniform compiler for a promised class of instances would yield randomized polynomial-time algorithms for every polynomial-time verifiable total search relation, even when the local gates are projections or constants. Thus, efficient local optimization alone is insufficient in the worst case.