$k$-server-bench: Automating Potential Discovery for the $k$-Server Conjecture

TL;DR

This paper presents a code-based challenge for automated discovery related to the $k$-server conjecture, aiming to find potential functions that could lead to proofs or counterexamples, and introduces a benchmark for such methods.

Contribution

It formulates a new open-ended challenge for automated mathematical discovery in the context of the $k$-server conjecture and provides initial experimental results demonstrating its difficulty and potential.

Findings

Current methods solve nontrivial instances for $k=3$

Methods reduce violations in the $k=4$ regime but do not fully resolve the challenge

The task serves as a benchmark that improves upon existing open-ended code-based benchmarks.

Abstract

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.