TCSExam: Evaluating frontier LLMs on the full range of TCS research
Abstract
Can large language models (LLMs) advance theoretical computer science and resolve its long-standing *open conjectures*? To study progress toward this goal, we introduce TCSExam, a unified framework and benchmark covering the full range of TCS research. It evaluates t*heorem proving*, *solver engineering*, and *constructions* alongside direct attempts to prove or refute open conjectures. TCSExam comprises 100 expert-reviewed tasks, with submissions checked by the Lean kernel or an executable task checker. Our evaluation of six frontier LLMs reveals substantial differences in theorem proving. When no proof outline is supplied, the strongest model produces complete, verified proofs in 70% of attempts, compared with at most 11.7% for any other model. Submitted solvers improve on selected public competition solutions, and constructions surpass selected reference bounds. None of the six models fully proves or refutes any of the 30 open conjectures under a budget of up to 12 hours per attempt. Individual attempts nevertheless yield independently verified mathematical results, including special cases and explicit bounds. With shared task interfaces and reproducible verification, TCSExam provides an extensible foundation for developing and evaluating LLMs for autonomous TCS research.
est. 32% chance this paper gets accepted at ICLR 2027.
What do you think this paper will get?
All positions stay anonymous.