Search papers, labs, and topics across Lattice.
This paper introduces $k$-server-bench, a code-based challenge for automated mathematical discovery focused on finding potential functions that satisfy a system of linear inequalities related to the $k$-server conjecture. The benchmark provides a sound (but incomplete) evaluation procedure, where violated inequalities refute a candidate potential function. Experiments show that agentic methods can solve nontrivial instances in the resolved $k=3$ regime and reduce violations in the open $k=4$ regime, suggesting the task is challenging but achievable.
Automating the hunt for potential functions just got real: a new benchmark lets AI agents tackle the $k$-server conjecture, a major unsolved problem in competitive analysis.
We introduce a code-based challenge for automated, open-ended mathematical discovery based on the $k$-server conjecture, a central open problem in competitive analysis. The task is to discover a potential function satisfying a large graph-structured system of simple linear inequalities. The resulting evaluation procedure is sound but incomplete: any violated inequality definitively refutes a candidate, whereas satisfying all inequalities does not by itself constitute a proof of the corresponding conjecture's special case. Nevertheless, a candidate that passes all constraints would be strong evidence toward a valid proof and, to the best of our knowledge, no currently known potential achieves this under our formulation in the open $k=4$ circle case. As such, a successful candidate would already be an interesting contribution to the $k$-server conjecture, and could become a substantial theoretical result when paired with a full proof. Experiments on the resolved $k=3$ regime show that current agentic methods can solve nontrivial instances, and in the open $k=4$ regime they reduce the number of violations relative to existing potentials without fully resolving the task. Taken together, these results suggest that the task is challenging but plausibly within reach of current methods. Beyond its relevance to the $k$-server community, where the developed tooling enables researchers to test new hypotheses and potentially improve on the current record, the task also serves as a useful \emph{benchmark} for developing code-based discovery agents. In particular, our $k=3$ results show that it mitigates important limitations of existing open-ended code-based benchmarks, including early saturation and the weak separation between naive random baselines and more sophisticated methods.
