Contextual Search and Bilateral Trade with a Trace-Square-Root Potential
Romain Cosson, Federico Fusco, Anupam Gupta, Stefano Leonardi, Renato Paes Leme, Matteo Russo
cs.GT
Nov 6, 2026 · v1
cs.LG
TL;DR
All proofs of the regret bounds for contextual search and bilateral trade are formalized in Lean 4, with a linked repository.
Abstract
We present a unified potential method for contextual search and bilateral trade with one-bit feedback and obtain order-tight algorithms for both problems. Our framework starts from a Bayesian perspective in which the unknown target (for contextual search) and the unknown pair of valuations (for bilateral trade) are sampled from a known prior distribution. In that model, the decision maker bases its prediction on the posterior distribution, obtained by conditioning on feedback received in previous rounds. For Bayesian contextual search, we present an algorithm with a total loss bounded by $O(\mathrm{Tr} \sqrt Σ)$, where $Σ$ is the covariance matrix of the target's prior; and for contextual bilateral trade, our algorithm's regret is bounded by $O(\mathrm{Tr} \sqrt{Σ_S}+\mathrm{Tr} \sqrt{Σ_B})$, where $Σ_S$ and $Σ_B$ are the covariance matrices of the seller's and buyer's valuations. We then use ideas from this Bayesian setting and adapt a “dual” of this trace-square-root potential to the classical worst-case setting, where the target and valuations are chosen adversarially from the unit Euclidean ball. For both contextual search and bilateral trade, we obtain tight $O(\sqrt d)$-regret algorithms. These results match the existing lower bounds up to a constant factor and improve on the previous guarantees of $O(d\log d)$ for contextual search and of $O(d6^d)$ for bilateral trade.
Problem
Contextual search and contextual bilateral trade with one-bit feedback had a gap between the known Omega(sqrt d) lower bounds and the best upper bounds, O(d log d) and O(d 6^d) respectively.
Approach
A unified potential method based on the trace-square-root of the covariance, Tr sqrt(Sigma), is developed first in a Bayesian setting, where predictions use posterior moments. A dual form of this potential is then adapted to the adversarial setting, where targets lie in the unit Euclidean ball. The first adversarial bilateral-trade proof was suggested by an AI model and later rewritten by the authors. All proofs were formalized in Lean 4.
Results
The Bayesian algorithms achieve O(Tr sqrt Sigma) loss for contextual search and O(Tr sqrt Sigma_S + Tr sqrt Sigma_B) regret for bilateral trade. In the adversarial setting both problems get O(sqrt d) regret, which matches the lower bounds up to constants.
| Result | Contextual search | Bilateral trade |
|---|
| Lower bound | sqrt(d) | sqrt(d)/6 |
| Liu, Paes Leme, Schneider | O(d log d) | — |
| Cosson et al. | — | O(d 6^d) |
| This work | O(sqrt d) | O(sqrt d) |
Worst-case regret bounds