publications

2025

1. OptimalThinkingBench: Evaluating Over and Underthinking in LLMs

   Pranjal Aggarwal, Seungone Kim, Jack Lanchantin, and 4 more authors

   2025
2. Premise Selection for a Lean Hammer

   Thomas Zhu, Joshua Clune, Jeremy Avigad, and 2 more authors

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

   Pranjal Aggarwal, and Sean Welleck

   2025

   COLM 2025
4. Programming with Pixels: Can Computer-Use Agents do Software Engineering?

   Pranjal Aggarwal, and Sean Welleck

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

   Seongyun Lee, Seungone Kim,  others, and 4 more authors

   2025
6. Scaling Evaluation-time Compute with Reasoning Models as Process Evaluators

   Seungone Kim, Inseok Wu, Jinwoo Lee, and 8 more authors

   2025
7. Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpening

   Andre He, Daniel Fried, and Sean Welleck

   2025

   EMNLP 2025 (Oral)
8. Agentic-R1: Distilled Dual-Strategy Reasoning

   Weihua Du, Pranjal Aggarwal, Sean Welleck, and 1 more author

   arXiv preprint arXiv:2507.05707, 2025

   EMNLP 2025
9. The BiGGen Bench: A Principled Benchmark for Fine-grained Evaluation of Language Models with Language Models

   Seungone Kim, Juyoung Suk, Ji Yong Cho, and 29 more authors

   In Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers), 2025

   Best Paper Award
10. Evaluating Language Models as Synthetic Data Generators

    Seungone Kim, Juyoung Suk, Xiang Yue, and 7 more authors

    In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), Jul 2025
11. Optimizing Temperature for Language Models with Multi-Sample Inference

    Weihua Du, Yiming Yang, and Sean Welleck

    arXiv preprint arXiv:2502.05234, Jul 2025

    ICML 2025

2024

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

   Pranjal Aggarwal, Bryan Parno, and Sean Welleck

   Jul 2024

   ICML 2025
2. Inference Scaling Laws: An Empirical Analysis of Compute-Optimal Inference for Problem-Solving with Language Models

   Yangzhen Wu, Zhiqing Sun, Shanda Li, and 2 more authors

   Jul 2024

   ICLR 2025
3. miniCTX: Neural Theorem Proving with (Long-)Contexts

   Jiewen Hu, Thomas Zhu, and Sean Welleck

   ArXiv, Jul 2024

   ICLR 2025 Oral
4. ImProver: Agent-Based Automated Proof Optimization

   Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, and 1 more author

   Jul 2024

   ICLR 2025
5. Lean-STaR: Learning to Interleave Thinking and Proving

   Haohan Lin, Zhiqing Sun, Yiming Yang, and 1 more author

   Jul 2024

   ICLR 2025 Spotlight
6. Easy-to-Hard Generalization: Scalable Alignment Beyond Human Supervision

   Zhiqing Sun, Longhui Yu, Yikang Shen, and 4 more authors

   In Advances in Neural Information Processing Systems, Jul 2024
7. Prometheus 2: An Open Source Language Model Specialized in Evaluating Other Language Models

   Seungone Kim, Juyoung Suk, Shayne Longpre, and 7 more authors

   In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, Nov 2024
8. From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Models

   Sean Welleck, Amanda Bertsch, Matthew Finlayson, and 5 more authors

   Transactions on Machine Learning Research, Oct 2024
9. miniCodeProps: a Minimal Benchmark for Proving Code Properties

   E. Lohn, and Sean Welleck

   Oct 2024

   NeurIPS 2024 Workshop on Safe Generative AI

2023

1. A Survey of Deep Learning for Mathematical Reasoning

   Pan Lu, Liang Qiu, Wenhao Yu, and 2 more authors

   In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), Jul 2023

   Abs

   Mathematical reasoning is a fundamental aspect of human intelligence and is applicable in various fields, including science, engineering, finance, and everyday life. The development of artificial intelligence (AI) systems capable of solving math problems and proving theorems in language has garnered significant interest in the fields of machine learning and natural language processing. For example, mathematics serves as a testbed for aspects of reasoning that are challenging for powerful deep learning models, driving new algorithmic and modeling advances. On the other hand, recent advances in large-scale neural language models have opened up new benchmarks and opportunities to use deep learning for mathematical reasoning. In this survey paper, we review the key tasks, datasets, and methods at the intersection of mathematical reasoning and deep learning over the past decade. We also evaluate existing benchmarks and methods, and discuss future research directions in this domain.

2. MAUVE Scores for Generative Models: Theory and Practice

   Krishna Pillutla, Lang Liu, John Thickstun, and 6 more authors

   ArXiv, Jul 2023
3. Inference-Time Policy Adapters (IPA): Tailoring Extreme-Scale LMs without Fine-tuning

   Ximing Lu, Faeze Brahman, Peter West, and 14 more authors

   EMNLP, Jul 2023
4. STEER: Unified Style Transfer with Expert Reinforcement

   Skyler Hallinan, Faeze Brahman, Ximing Lu, and 3 more authors

   EMNLP Findings, Jul 2023
5. Self-Refine: Iterative Refinement with Self-Feedback

   Aman Madaan, Niket Tandon, Prakhar Gupta, and 13 more authors

   In Thirty-seventh Conference on Neural Information Processing Systems, Jul 2023
6. Generating Sequences by Learning to Self-Correct

   Sean Welleck, Ximing Lu, Peter West, and 4 more authors

   In The Eleventh International Conference on Learning Representations , Jul 2023
7. llmstep: LLM proofstep suggestions in Lean

   Sean Welleck, and Rahul Saha

   In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS’23, Jul 2023
8. Neural theorem proving tutorial

   Sean Welleck

   In IJCAI 2023 Tutorial, Jul 2023
9. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

   Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, and 6 more authors

   In The Eleventh International Conference on Learning Representations , Jul 2023
10. Llemma: An Open Language Model For Mathematics

    Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, and 6 more authors

    arXiv preprint arXiv:2310.06786, Jul 2023
11. Faith and Fate: Limits of Transformers on Compositionality

    Nouha Dziri, Ximing Lu, Melanie Sclar, and 13 more authors

    In Thirty-seventh Conference on Neural Information Processing Systems, Jul 2023

2022

1. Rainier: Reinforced Knowledge Introspector for Commonsense Question Answering

   Jiacheng Liu, Skyler Hallinan, Ximing Lu, and 4 more authors

   In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, Dec 2022

   Abs

   Knowledge underpins reasoning. Recent research demonstrates that when relevant knowledge is provided as additional context to commonsense question answering (QA), it can substantially enhance the performance even on top of state-of-the-art. The fundamental challenge is where and how to find such knowledge that is high quality and on point with respect to the question; knowledge retrieved from knowledge bases are incomplete and knowledge generated from language models are inconsistent. We present Rainier, or Reinforced Knowledge Introspector, that learns to generate contextually relevant knowledge in response to given questions. Our approach starts by imitating knowledge generated by GPT-3, then learns to generate its own knowledge via reinforcement learning where rewards are shaped based on the increased performance on the resulting question answering. Rainier demonstrates substantial and consistent performance gains when tested over 9 different commonsense benchmarks: including 5 datasets that are seen during model training, as well as 4 datasets that are kept unseen. Our work is the first to report that knowledge generated by models that are orders of magnitude smaller than GPT-3, even without direct supervision on the knowledge itself, can exceed the quality of commonsense knowledge elicited from GPT-3.

2. Symbolic Knowledge Distillation: from General Language Models to Commonsense Models

   Peter West, Chandra Bhagavatula, Jack Hessel, and 6 more authors

   In Proceedings of the 2022 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Jul 2022
3. Generated Knowledge Prompting for Commonsense Reasoning

   Jiacheng Liu, Alisa Liu, Ximing Lu, and 5 more authors

   In Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), May 2022
4. Prompt Waywardness: The Curious Case of Discretized Interpretation of Continuous Prompts

   Daniel Khashabi, Xinxi Lyu, Sewon Min, and 8 more authors

   In Proceedings of the 2022 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Jul 2022

   Abs

   Fine-tuning continuous prompts for target tasks has recently emerged as a compact alternative to full model fine-tuning. Motivated by these promising results, we investigate the feasibility of extracting a discrete (textual) interpretation of continuous prompts that is faithful to the problem they solve. In practice, we observe a “wayward” behavior between the task solved by continuous prompts and their nearest neighbor discrete projections: We can find continuous prompts that solve a task while being projected to an arbitrary text (e.g., definition of a different or even a contradictory task), while being within a very small (2%) margin of the best continuous prompt of the same size for the task. We provide intuitions behind this odd and surprising behavior, as well as extensive empirical analyses quantifying the effect of various parameters. For instance, for larger model sizes we observe higher waywardness, i.e, we can find prompts that more closely map to any arbitrary text with a smaller drop in accuracy. These findings have important implications relating to the difficulty of faithfully interpreting continuous prompts and their generalization across models and tasks, providing guidance for future progress in prompting language models.

5. LILA: A Unified Benchmark for Mathematical Reasoning

   Swaroop Mishra, Matthew Finlayson, Pan Lu, and 8 more authors

   In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, Dec 2022

   Abs

   Mathematical reasoning skills are essential for general-purpose intelligentsystems to perform tasks from grocery shopping to climate modeling. Towards evaluating and improving AI systems in this domain, we proposeLILA, a unified mathematical reasoning benchmark consisting of 23 diversetasks along four dimensions:(i) mathematical abilities e.g., arithmetic, calculus (ii) language format e.g., question-answering, fill-in-the-blanks (iii) language diversity e.g., no language, simple language (iv) external knowledge e.g., commonsense, physics. We construct our benchmark by extending 20 datasets benchmark by collecting task instructions and solutions in the form of Python programs,thereby obtaining explainable solutions in addition to the correct answer. We additionally introduce two evaluation datasets to measure out-of-distribution performance and robustness to language perturbation. Finally, we introduce BHASKARA,a general-purpose mathematical reasoning model trained on LILA. Importantly, we find that multi-tasking leads to significant improvements (average relative improvement of 21.83% F1 score vs. single-task models),while the best performing model only obtains 60.40%,indicating the room for improvement in general mathematical reasoning and understanding.

6. NaturalProver: Grounded Mathematical Proof Generation with Language Models

   Sean Welleck, Jiacheng Liu, Ximing Lu, and 2 more authors

   In Advances in Neural Information Processing Systems, Dec 2022
7. COLD Decoding: Energy-based Constrained Text Generation with Langevin Dynamics

   Lianhui Qin, Sean Welleck, Daniel Khashabi, and 1 more author

   In Advances in Neural Information Processing Systems, Dec 2022
8. QUARK: Controllable Text Generation with Reinforced Unlearning

   Ximing Lu, Sean Welleck, Jack Hessel, and 5 more authors

   In Advances in Neural Information Processing Systems, Dec 2022
9. NeuroLogic A*esque Decoding: Constrained Text Generation with Lookahead Heuristics

   Ximing Lu, Sean Welleck, Peter West, and 9 more authors

   In Proceedings of the 2022 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Jul 2022

   Abs

   The dominant paradigm for neural text generation is left-to-right decoding from autoregressive language models. Constrained or controllable generation under complex lexical constraints, however, requires foresight to plan ahead feasible future paths. Drawing inspiration from the A^* search algorithm, we propose NeuroLogic A*esque, a decoding algorithm that incorporates heuristic estimates of future cost. We develop lookahead heuristics that are efficient for large-scale language models, making our method a drop-in replacement for common techniques such as beam search and top-k sampling. To enable constrained generation, we build on NeuroLogic decoding (Lu et al., 2021), combining its flexibility in incorporating logical constraints with A*esque estimates of future constraint satisfaction. Our approach outperforms competitive baselines on five generation tasks, and achieves new state-of-the-art performance on table-to-text generation, constrained machine translation, and keyword-constrained generation. The improvements are particularly notable on tasks that require complex constraint satisfaction or in few-shot or zero-shot settings. NeuroLogic A*esque illustrates the power of decoding for improving and enabling new capabilities of large-scale language models.

10. Maieutic Prompting: Logically Consistent Reasoning with Recursive Explanations

    Jaehun Jung, Lianhui Qin, Sean Welleck, and 4 more authors

    In Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, Dec 2022

    Abs

    Pre-trained language models (LMs) struggle with consistent reasoning; recently, prompting LMs to generate explanations that self-guide the inference has emerged as a promising direction to amend this. However, these approaches are fundamentally bounded by the correctness of explanations, which themselves are often noisy and inconsistent. In this work, we develop Maieutic Prompting, which aims to infer a correct answer to a question even from the unreliable generations of LM. Maieutic Prompting induces a tree of explanations abductively (e.g. X is true, because ...) and recursively, then frames the inference as a satisfiability problem over these explanations and their logical relations. We test Maieutic Prompting for true/false QA on three challenging benchmarks that require complex commonsense reasoning. Maieutic Prompting achieves up to 20% better accuracy than state-of-the-art prompting methods, and as a fully unsupervised approach, performs competitively with supervised models. We also show that Maieutic Prompting improves robustness in inference while providing interpretable rationales.

2021

1. NaturalProofs: Mathematical Theorem Proving in Natural Language

   Sean Welleck, Jiacheng Liu, Ronan Le Bras, and 3 more authors

   In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1), Dec 2021
2. Towards Grounded Natural Language Proof Generation

   Sean Welleck, Jiacheng Liu, Jesse Michael Han, and 1 more author

   In NeurIPS 2021 Workshop on Math AI for Education: Bridging the Gap Between Research and Smart Education, Dec 2021
3. Divergence Frontiers for Generative Models: Sample Complexity, Quantization Effects, and Frontier Integrals

   Lang Liu, Krishna Pillutla, Sean Welleck, and 3 more authors

   In Advances in Neural Information Processing Systems, Dec 2021
4. Mode recovery in neural autoregressive sequence modeling

   Ilia Kulikov, Sean Welleck, and Kyunghyun Cho

   In Proceedings of the 5th Workshop on Structured Prediction for NLP (SPNLP 2021), Aug 2021

   Abs

   Despite its wide use, recent studies have revealed unexpected and undesirable properties of neural autoregressive sequence models trained with maximum likelihood, such as an unreasonably high affinity to short sequences after training and to infinitely long sequences at decoding time. We propose to study these phenomena by investigating how the modes, or local maxima, of a distribution are maintained throughout the full \textitlearning chain of the ground-truth, empirical, learned and decoding-induced distributions, via the newly proposed \textitmode recovery cost. We design a tractable testbed where we build three types of ground-truth distributions: (1) an LSTM based structured distribution, (2) an unstructured distribution where probability of a sequence does not depend on its content, and (3) a product of these two which we call a semi-structured distribution. Our study reveals both expected and unexpected findings. First, starting with data collection, mode recovery cost strongly relies on the ground-truth distribution and is most costly with the semi-structured distribution. Second, after learning, mode recovery cost from the ground-truth distribution may increase or decrease compared to data collection, with the largest cost degradation occurring with the semi-structured ground-truth distribution. Finally, the ability of the decoding-induced distribution to recover modes from the learned distribution is highly impacted by the choices made earlier in the learning chain. We conclude that future research must consider the entire learning chain in order to fully understand the potentials and perils and to further improve neural autoregressive sequence models.

5. Symbolic Brittleness in Sequence Models: on Systematic Generalization in Symbolic Mathematics

   Sean Welleck, Peter West, Jize Cao, and 1 more author

   In AAAI Conference on Artificial Intelligence, Aug 2021
6. MAUVE: Measuring the Gap Between Neural Text and Human Text using Divergence Frontiers

   Krishna Pillutla, Swabha Swayamdipta, Rowan Zellers, and 4 more authors

   In Advances in Neural Information Processing Systems, Aug 2021

2020

1. Consistency of a Recurrent Language Model With Respect to Incomplete Decoding

   Sean Welleck, Ilia Kulikov, Jaedeok Kim, and 2 more authors

   In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), Nov 2020

   Abs

   Despite strong performance on a variety of tasks, neural sequence models trained with maximum likelihood have been shown to exhibit issues such as length bias and degenerate repetition. We study the related issue of receiving infinite-length sequences from a recurrent language model when using common decoding algorithms. To analyze this issue, we first define inconsistency of a decoding algorithm, meaning that the algorithm can yield an infinite-length sequence that has zero probability under the model. We prove that commonly used incomplete decoding algorithms – greedy search, beam search, top-k sampling, and nucleus sampling – are inconsistent, despite the fact that recurrent language models are trained to produce sequences of finite length. Based on these insights, we propose two remedies which address inconsistency: consistent variants of top-k and nucleus sampling, and a self-terminating recurrent language model. Empirical results show that inconsistency occurs in practice, and that the proposed methods prevent inconsistency.

2. MLE-guided parameter search for task loss minimization in neural sequence modeling

   Sean Welleck, and Kyunghyun Cho

   In AAAI Conference on Artificial Intelligence, Nov 2020
3. Don’t Say That! Making Inconsistent Dialogue Unlikely with Unlikelihood Training

   Margaret Li, Stephen Roller, Ilia Kulikov, and 4 more authors

   In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, Jul 2020

   Abs

   Generative dialogue models currently suffer from a number of problems which standard maximum likelihood training does not address. They tend to produce generations that (i) rely too much on copying from the context, (ii) contain repetitions within utterances, (iii) overuse frequent words, and (iv) at a deeper level, contain logical flaws. In this work we show how all of these problems can be addressed by extending the recently introduced unlikelihood loss (Welleck et al., 2019) to these cases. We show that appropriate loss functions which regularize generated outputs to match human distributions are effective for the first three issues. For the last important general issue, we show applying unlikelihood to collected data of what a model should not do is effective for improving logical consistency, potentially paving the way to generative models with greater reasoning ability. We demonstrate the efficacy of our approach across several dialogue tasks.

4. A Generalized Framework of Sequence Generation with Application to Undirected Sequence Models

   Elman Mansimov, Alex Wang, Sean Welleck, and 1 more author

   Jul 2020
5. Neural Text Generation With Unlikelihood Training

   Sean Welleck, Ilia Kulikov, Stephen Roller, and 3 more authors

   In International Conference on Learning Representations, Jul 2020

2019

1. Non-Monotonic Sequential Text Generation

   Sean Welleck, Kianté Brantley, Hal Daumé Iii, and 1 more author

   In Proceedings of the 36th International Conference on Machine Learning, 09–15 jun 2019

   Abs PDF

   Standard sequential generation methods assume a pre-specified generation order, such as text generation methods which generate words from left to right. In this work, we propose a framework for training models of text generation that operate in non-monotonic orders; the model directly learns good orders, without any additional annotation. Our framework operates by generating a word at an arbitrary position, and then recursively generating words to its left and then words to its right, yielding a binary tree. Learning is framed as imitation learning, including a coaching method which moves from imitating an oracle to reinforcing the policy’s own preferences. Experimental results demonstrate that using the proposed method, it is possible to learn policies which generate text without pre-specifying a generation order, while achieving competitive performance with conventional left-to-right generation.

2. Dialogue Natural Language Inference

   Sean Welleck, Jason Weston, Arthur Szlam, and 1 more author

   In Proceedings of the 57th Annual Meeting of the Association for Computational Linguistics, Jul 2019
3. Sequential Graph Dependency Parser

   Sean Welleck, and Kyunghyun Cho

   In Proceedings of the International Conference on Recent Advances in Natural Language Processing (RANLP 2019), Sep 2019

2017

1. Loss Functions for Multiset Prediction

   Sean Welleck, Zi-Mei Yao, Yujie Gai, and 3 more authors

   In Neural Information Processing Systems, Sep 2017
2. Saliency-based Sequential Image Attention with Multiset Prediction

   Sean Welleck, Jialin Mao, Kyunghyun Cho, and 1 more author

   In Advances in Neural Information Processing Systems, Sep 2017