Kelly Buchanan

I’m a Postdoctoral Scholar at Stanford University working with Scott Linderman and Christopher Ré. My research focuses on reliability in AI systems. I develop evaluations for the reasoning capabilities (especially coding) of frontier AI models, and use the ensuing insights to build better agentic systems that can verify their own reasoning, quantify uncertainty, and operate safely at scale.

Some of my recent projects include:

Terminal-Bench (ICLR, 2026), a benchmark for evaluating agentic systems in realistic terminal environments. Now widely used to test open and closed-source foundation models under real-world constraints.
Weaver (NeurIPS, 2025), a verification framework that fuses weak but cost-efficient verifiers into unified correctness estimates, closing the generation–verification gap.

I completed my PhD at Columbia University’s Center for Theoretical Neuroscience, where I worked with Liam Paninski and John Cunningham. My research developed ML methods for functional imaging, pose estimation, and behavioral segmentation, used by organizations including Q-state Biosciences, the International Brain Laboratory, and the Zuckerman Institute.

I also spent time at Google as a Student Researcher on the Reliable Deep Learning team, evaluating reliability of large language and vision models.

I earned my Bachelor’s and Master’s degrees with Honors in Electrical Engineering from KU.

Selected Publications

Terminal-Bench: Benchmarking Agents on Hard, Realistic Tasks in Command Line Interfaces

The Terminal-Bench Team

ICLR, 2026

Abs HTML Website Code

AI agents may soon become capable of autonomously completing valuable, longhorizon tasks in diverse domains. Current benchmarks either do not measure real-world tasks, or are not sufficiently difficult to meaningfully measure frontier models. To this end, we present Terminal-Bench 2.0: a carefully curated hard benchmark composed of 89 tasks in computer terminal environments inspired by problems from real workflows. Each task features a unique environment, humanwritten solution, and comprehensive tests for verification. We show that frontier models and agents score less than 65% on the benchmark and conduct an error analysis to identify areas for model and agent improvement. We publish the dataset and evaluation harness to assist developers and researchers in future work at tbench.ai.
A Unifying Framework for Parallelizing Sequential Models with Linear Dynamical Systems

Xavier Gonzalez^*, E. Kelly Buchanan^*, Hyun Dong Lee, and 5 more authors

TMLR, 2026

Abs HTML Code

Harnessing parallelism in seemingly sequential models is a central challenge for modern machine learning. Several approaches have been proposed for evaluating sequential processes in parallel using iterative fixed-point methods, like Newton, Picard, and Jacobi iterations. In this work, we show that these methods can be understood within a common framework based on linear dynamical systems (LDSs), where different iteration schemes arise naturally as approximate linearizations of a nonlinear recursion. Moreover, we theoretically analyze the rates of convergence of these methods, and we verify the predictions of this theory with several case studies. This unifying framework highlights shared principles behind these techniques and clarifies when particular fixed-point methods are most likely to be effective. By bridging diverse algorithms through the language of LDSs, the framework provides a clearer theoretical foundation for parallelizing sequential models and points toward new opportunities for efficient and scalable computation.
Weaver: Shrinking the Generation-Verification Gap by Scaling Compute for Verification

Jon Saad-Falcon^*, E. Kelly Buchanan^*, Mayee F. Chen^*, and 9 more authors

NeurIPS, 2025

Abs HTML Blog Code

Verifiers can improve language model (LM) capabilities by providing feedback or selecting the best response from a pool of generated candidates. Currently, high-quality verifiers are either unscalable (e.g., humans) or limited in utility (e.g., tools like Lean for formal proofs). While LM judges and reward models have become broadly useful as general-purpose verifiers, a significant performance gap remains between them and oracle verifiers. To help close this gap, we introduce Weaver, a framework for designing a strong verifier by combining multiple weak, imperfect verifiers. First we find that weighted ensembles of verifiers, which typically require learning from labeled data, significantly outperform unweighted combinations due to differences in the verifiers. To reduce the dependency on labeled data, Weaver leverages weak supervision to estimate each verifier’s accuracy and combines their outputs into a unified score that better reflects true response quality. However, directly applying weak supervision algorithms poses several challenges, including inconsistent verifier output formats and handling low-quality verifiers. Weaver addresses these challenges by using dataset statistics to normalize outputs and filter specific verifiers. We study the effectiveness of Weaver in repeated sampling settings, where a model generates multiple candidate responses at test time and a verifier is used to select the correct one. Our evaluations demonstrate that Weaver significantly improves the pass@1 performance across several reasoning and math tasks, achieving o3-mini level accuracy with Llama 3.3 70B Instruct (a much cheaper non-reasoning model) as the generator, and an ensemble of smaller judge and reward models as the verifiers (86.2% average). This gain mirrors the jump achieved between GPT-4o and o3-mini (69.0% vs. 86.7%), which required extensive finetuning and post-training interventions. To make Weaver more efficient, we train a compact 400M cross-encoder using Weaver’s combined output scores. This distilled model retains 98.7% of Weaver’s full accuracy while reducing verification compute by up to 99.97%.