About

Todd Millstein is a professor in the Department of Computer Science at UCLA Samueli School of Engineering. His research interests include verified software, simple and efficient concurrency, network programming and verification, and probabilistic programming. He has received numerous awards for his teaching and research, including the UCLA Samueli Excellence in Teaching Award in 2024, the Northrop Grumman Excellence in Teaching Award in 2016, the IEEE Micro Top Picks Selection in 2012, the ACM SIGPLAN Most Influential PLDI Paper Award in 2011, and the NSF Career Award in 2006. He earned his PhD from the University of Washington in 2003.

Research topics

• Computer Science
• Computer network
• Artificial Intelligence
• Distributed computing
• Programming language
• Operating system
• Theoretical computer science
• Physics
• Algorithm
• Quantum mechanics

Selected publications

• Probabilistic Programs of Thought

  arXiv (Cornell University) · 2026-04-19

  preprintOpen access

  LLMs are widely used for code generation and mathematical reasoning tasks where they are required to generate structured output. They either need to reason about code, generate code for a given specification, or reason using programs of thought. The typical approach to code generation is to prompt the model and generate samples until an appropriate program is obtained. Within this process, sampling $n$ programs from the language model requires $n$ GPU compute-intensive generations which becomes prohibitively expensive for larger values of $n$. In this work, we address this limitation by exposing the LLM's distribution within the generated programs themselves. We propose a novel test-time framework we dub probabilistic programs of thought to obtain more samples from the model with fewer LLM generations. Given a program generated by a model and the associated next-token probabilities, we build a probabilistic program that compactly represents exponentially many deterministic programs. Since performing probabilistic reasoning in this probabilistic program is much cheaper, our approach allows sampling new programs without any additional GPU compute and little CPU overhead. We instantiate our approach on benchmarks for code generation, code understanding and mathematical reasoning and report improvements in performance with fewer generations from the LLM.

  PublisherDOI

• Probabilistic Programs of Thought

  ArXiv.org · 2026-04-19

  articleOpen access

  LLMs are widely used for code generation and mathematical reasoning tasks where they are required to generate structured output. They either need to reason about code, generate code for a given specification, or reason using programs of thought. The typical approach to code generation is to prompt the model and generate samples until an appropriate program is obtained. Within this process, sampling $n$ programs from the language model requires $n$ GPU compute-intensive generations which becomes prohibitively expensive for larger values of $n$. In this work, we address this limitation by exposing the LLM's distribution within the generated programs themselves. We propose a novel test-time framework we dub probabilistic programs of thought to obtain more samples from the model with fewer LLM generations. Given a program generated by a model and the associated next-token probabilities, we build a probabilistic program that compactly represents exponentially many deterministic programs. Since performing probabilistic reasoning in this probabilistic program is much cheaper, our approach allows sampling new programs without any additional GPU compute and little CPU overhead. We instantiate our approach on benchmarks for code generation, code understanding and mathematical reasoning and report improvements in performance with fewer generations from the LLM.

  PublisherOA PDF

• Tackling Ambiguity in User Intent for LLM-based Network Configuration Synthesis

  2025-11-17

  articleOpen access

  Beyond hallucinations, another problem in program synthesis using LLMs is ambiguity in user intent. We illustrate the ambiguity problem in a networking context for LLM-based incremental configuration synthesis of route maps and ACLs. Configuration stanzas frequently overlap in header space, making the relative priority of actions impossible for the LLM to infer without user interaction. Measurements in a large cloud identify complex ACLs with 100s of overlaps, showing ambiguity is a real problem. We propose a prototype system, Clarify, augmenting an LLM with a new module called a Disambiguator that helps elicit user intent. On a small synthetic workload, Clarify incrementally synthesizes routing policies and interactively disambiguates user intent to ensure correctness.

  PublisherDOI

• Synthesizing Implication Lemmas for Interactive Theorem Proving

  Proceedings of the ACM on Programming Languages · 2025-10-09

  articleOpen accessSenior author

  Interactive theorem provers (ITP) enable programmers to formally verify properties of their software systems. One burden for users of ITPs is identifying the necessary helper lemmas to complete a proof, for example those that define key inductive invariants. Existing approaches to lemma synthesis for ITPs have limited, if any, support for synthesizing implications : lemmas of the form P 1 ∧ ⋯ ∧ P n ⇒ Q . In this paper, we propose a technique and associated tool for synthesizing useful implication lemmas. Our approach employs a form of data-driven invariant inference to explore strengthenings of the current proof state, based on sample valuations of the current goal and assumptions. We have implemented our approach in a Rocq tactic called dilemma. We demonstrate its effectiveness in synthesizing necessary helper lemmas for proofs from the Verified Functional Algorithms textbook as well as from prior benchmark suites for lemma synthesis.

  PublisherDOI

• Tuning Random Generators: Property-Based Testing as Probabilistic Programming

  Proceedings of the ACM on Programming Languages · 2025-10-09

  articleOpen access

  Property-based testing validates software against an executable specification by evaluating it on randomly generated inputs. The standard way that PBT users generate test inputs is via generators that describe how to sample test inputs through random choices. To achieve a good distribution over test inputs, users must tune their generators, i.e., decide on the weights of these individual random choices. Unfortunately, it is very difficult to understand how to choose individual generator weights in order to achieve a desired distribution, so today this process is tedious and limits the distributions that can be practically achieved. In this paper, we develop techniques for the automatic and offline tuning of generators. Given a generator with undetermined symbolic weights and an objective function, our approach automatically learns values for these weights that optimize for the objective. We describe useful objective functions that allow users to (1) target desired distributions and (2) improve the diversity and validity of their test cases. We have implemented our approach in a novel discrete probabilistic programming system, Loaded Dice, that supports differentiation and parameter learning, and use it as a language for generators. We empirically demonstrate that our approach is effective at optimizing generator distributions according to the specified objective functions. We also perform a thorough evaluation on PBT benchmarks, demonstrating that, when automatically tuned for diversity and validity, the generators exhibit a 3.1-7.4x speedup in bug finding.

  PublisherDOI

• Tuning Random Generators: Property-Based Testing as Probabilistic Programming

  arXiv (Cornell University) · 2025-08-20

  preprintOpen access

  Property-based testing validates software against an executable specification by evaluating it on randomly generated inputs. The standard way that PBT users generate test inputs is via generators that describe how to sample test inputs through random choices. To achieve a good distribution over test inputs, users must tune their generators, i.e., decide on the weights of these individual random choices. Unfortunately, it is very difficult to understand how to choose individual generator weights in order to achieve a desired distribution, so today this process is tedious and limits the distributions that can be practically achieved. In this paper, we develop techniques for the automatic and offline tuning of generators. Given a generator with undetermined symbolic weights and an objective function, our approach automatically learns values for these weights that optimize for the objective. We describe useful objective functions that allow users to (1) target desired distributions and (2) improve the diversity and validity of their test cases. We have implemented our approach in a novel discrete probabilistic programming system, Loaded Dice, that supports differentiation and parameter learning, and use it as a language for generators. We empirically demonstrate that our approach is effective at optimizing generator distributions according to the specified objective functions. We also perform a thorough evaluation on PBT benchmarks, demonstrating that, when automatically tuned for diversity and validity, the generators exhibit a 3.1-7.4x speedup in bug finding.

  PublisherDOI

• LLM-Based Config Synthesis requires Disambiguation

  ArXiv.org · 2025-07-16

  preprintOpen access

  Beyond hallucinations, another problem in program synthesis using LLMs is ambiguity in user intent. We illustrate the ambiguity problem in a networking context for LLM-based incremental configuration synthesis of route-maps and ACLs. These structures frequently overlap in header space, making the relative priority of actions impossible for the LLM to infer without user interaction. Measurements in a large cloud identify complex ACLs with 100's of overlaps, showing ambiguity is a real problem. We propose a prototype system, Clarify, which uses an LLM augmented with a new module called a Disambiguator that helps elicit user intent. On a small synthetic workload, Clarify incrementally synthesizes routing policies after disambiguation and then verifies them. Our treatment of ambiguities is useful more generally when the intent of updates can be correctly synthesized by LLMs, but their integration is ambiguous and can lead to different global behaviors.

  PublisherOA PDFDOI

• Everything Is a Program (Even If It's Not) (Keynote)

  2024-10-17

  article1st authorCorresponding

  A brief discussion at a conference more than 15 years ago led to a collaborative research agenda that has been incredibly fun, intellectually challenging, and impactful. Internet protocols like BGP and DNS underlie everything that we do online, but they routinely break network security and reliability due to their complexity and fragility. While there are many moving parts and underlying causes, time and again the programming languages perspective has proven to be a powerful way to make progress. In short, everything is a program (even if it’s not), and once something is a program we can give it a precise semantics and bring to bear a host of techniques to reason about its behavior. I’ll illustrate this approach through examples from my work, but the ideas are applicable beyond computer networks. I’ll also distill some general lessons that I’ve learned about doing collaborative research and making an impact.

  PublisherDOI

• If Layering is useful, why not Sublayering?

  2024-11-11 · 1 citations

  articleOpen access

  The Internet's success arose from classical layering: protocols like TCP and Ethernet can be independently understood, changed, debugged, verified, and offloaded to hardware using a clean service interface between layers. To accrue the same benefits at a finer grain, we suggest sublayering, i.e., layering recursively within each layer. We show that the data link and routing layers have natural sublayers. However, while TCP intuitively decomposes into sub-functions (connection management, reliable delivery, congestion control) common state variables like sequence numbers and window sizes entangle these functions, making sublayering difficult. We propose an alternate sublayered TCP with equivalent functionality which enables easily changing congestion control and connection management. We also argue that sublayering can help create robust and verified Internet protocol implementations akin to seL4 for Operating Systems. To this end, we describe early experiments with a verified sublayered implementation of a simple bit-stuffing protocol using Coq, and a verified monolithic implementation of a lightweight TCP using Dafny. We end with a set of challenges for sublayered protocols.

  PublisherDOI

• Bit Blasting Probabilistic Programs

  Proceedings of the ACM on Programming Languages · 2024-06-20 · 8 citations

  articleOpen accessSenior author

  Probabilistic programming languages (PPLs) are an expressive means for creating and reasoning about probabilistic models. Unfortunately hybrid probabilistic programs that involve both continuous and discrete structures are not well supported by today’s PPLs. In this paper we develop a new approximate inference algorithm for hybrid probabilistic programs that first discretizes the continuous distributions and then performs discrete inference on the resulting program. The key novelty is a form of discretization that we call bit blasting , which uses a binary representation of numbers such that a domain of <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" overflow="scroll"> <mml:msup> <mml:mn>2</mml:mn> <mml:mi>b</mml:mi> </mml:msup> </mml:math> discretized points can be succinctly represented as a discrete probabilistic program over poly <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline" overflow="scroll"> <mml:mfenced close=")" open="("> <mml:mi>b</mml:mi> </mml:mfenced> </mml:math> Boolean random variables. Surprisingly, we prove that many common continuous distributions can be bit blasted in a manner that incurs no loss of accuracy over an explicit discretization and supports efficient probabilistic inference. We have built a probabilistic programming system for hybrid programs called HyBit , which employs bit blasting followed by discrete probabilistic inference. We empirically demonstrate the benefits of our approach over existing sampling-based and symbolic inference approaches

  PublisherOA PDFDOI

Recent grants

• FMitF: Opening Up the Black Box of Probabilistic Program Inference

  NSF · $1.1M · 2018–2023

• NeTS: Medium: Collaborative Research: Systematic Analysis of Protocol Implementations

  NSF · $447k · 2012–2017

• NeTS: Medium: Collaborative Research: Network Configuration Synthesis: A Path to Practical Deployment

  NSF · $630k · 2017–2021

• "CAREER:" Enforcing and Validating User-Defined Programming Disciplines

  NSF · $400k · 2006–2012

• SHF: Small: Interacting to Specify Software

  NSF · $500k · 2015–2020

Frequent coauthors

• Ramesh Govindan

  University of Southern California

  26 shared

• Guy Van den Broeck

  University of California, Los Angeles

  21 shared

• Daniel Marino

  Virginia Commonwealth University

  20 shared

• Craig Chambers

  19 shared

• Nupur Kothari

  Microsoft Research (United Kingdom)

  18 shared

• Steven Holtzen

  18 shared

• Madanlal Musuvathi

  Microsoft (United States)

  17 shared

• Abhayendra Singh

  Google (United States)

  15 shared

Awards & honors

• UCLA Samueli Excellence in Teaching Award - 2024
• Northrop Grumman Excellence in Teaching Award - 2016
• IEEE Micro Top Picks Selection - 2012
• ACM SIGPLAN Most Influential PLDI Paper Award - 2011
• NSF Career Award - 2006