projects | L3 Lab at CMU

reasoning and verification

Language models for mathematics and code

Our research uses mathematics as a testbed for reasoning, and integrates language models with interactive proof assistants such as Lean. Moving forward, we are interested in enabling strong reasoning capabilities, verified code synthesis and mathematics, and furthering the science of scaling in these domains.

Foundation models for mathematics

As part of a multi-lab collaboration we developed Llemma and ProofPile II, a foundation model for mathematics and 55 billion token dataset with 1.5 billion tokens of formal code.

Neural and symbolic theorem proving

We develop theorem proving methods that leverage informal and formal representations. For example, Draft Sketch Prove uses language models to sketch formal proofs based on informal proofs, then fills in the gaps.

Neural tools for formal verification

We develop practical tools that make formal proof assistants easier to use. For example, LLMstep uses language models to provide verified next-step suggestions in Lean.

iterative improvement

Iterative improvement

We aim to develop machine learning systems that improve over time. In the context of language, we have viewed this problem as one of interleaving search and learning, which requires new inference-time algorithms and algorithms for learning from feedback. Moving forward, we are particularly interested in iterative improvement in the context of reasoning and code, along with core algorithmic development.

Iterative refinement algorithms

We develop algorithms for iteratively refining outputs at inference time, allowing for efficient search that takes advantage of feedback. Examples include Self-Correction and Self-Refinement.

Search and decoding algorithms

We develop inference-time algorithms that search for sequences guided by constraints. Examples include A* lookahead decoding and Maeutic inference.

Learning from feedback

We draw on ideas from reinforcement learning to design new algorithms for learning from feedback. For example, Quark brings ideas from batch- and goal-conditioned RL to language.

science of llms

Science of neural language models

We analyze neural language models, including formalizing their behavior, studying their ability to generalize, and evaluating their learned distributions. Moving forward, we are broadly interested in basic research related to large language models, scalable evaluation, and efficient methods for generating sequences.

Generalization

We aim to understand how language models generalize, including out-of-distribution generalization in formal reasoning and the role of memorization. Examples include Symbolic Brittleness, Limits of Transformers, and Llemma.

Scalable evaluation

We aim to reduce the human effort needed to evaluate large language models. For example, Mauve enables automatic evaluation of text at a distributional level using information divergences.

Formal analysis

We formalize aspects of language generation and develop theory and empirical analysis. Relevant work includes decoding algorithm consistency, mode recovery, and multi-step reasoning.