Sean Welleck

Premise Selection for a Lean Hammer

RefineBench: Evaluating Refinement Capability of Language Models via Checklists

Programming with Pixels: Can Computer-Use Agents do Software Engineering?

OptimalThinkingBench: Evaluating Over and Underthinking in LLMs

The CoT Encyclopedia: Analyzing, Predicting, and Controlling how a Reasoning Model will Think

Scaling Evaluation-time Compute with Reasoning Models as Process Evaluators

miniCTX: Neural Theorem Proving with (Long-)Contexts

Lean-STaR: Learning to Interleave Thinking and Proving

L1: Controlling How Long A Reasoning Model Thinks With Reinforcement Learning

AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement

ImProver: Agent-Based Automated Proof Optimization

Optimizing Temperature for Language Models with Multi-Sample Inference

Inference Scaling Laws: An Empirical Analysis of Compute-Optimal Inference for LLM Problem-Solving