PeopleofSuperintelligence

Researcher

Sorin Lerner

Sorin Lerner is a computer scientist whose research applies AI to program proofs and programming tools. In 2003, he coauthored a method for automatically proving compiler optimizations sound; in 2020, he coauthored Proverbot9001, which used machine learning to generate software correctness proofs. He studied computer engineering at McGill and earned a computer science PhD at the University of Washington before joining UC San Diego in 2006. In 2024, he coauthored CoqPyt, a Python tool for working with Coq proofs, and a study of live programming for validating AI-generated code. He is dean of Cornell Bowers and a professor of computer science, with current work on LLM-based program proofs and human-centered programming environments.

Works
192
Citations
4,246
h-index
32
Badges

Publication numbers from OpenAlex, as of 27 October 2026.

Timeline

  1. 2003

    Correct compiler optimizations

    With Todd Millstein and Craig Chambers, he develops Cobalt, a domain-specific language for compiler optimizations, and a method to prove those transformations sound. Their PLDI paper wins the 2003 Best Paper Award.

  2. 2006

    Joining UC San Diego

    He grows up in Montreal, studies computer engineering at McGill and earns a computer science PhD at the University of Washington. In January 2006, he joins the Jacobs School's Computer Science and Engineering faculty.

  3. 2018–2019

    A teaching award

    At UC San Diego, he receives the Jacobs School of Engineering's CSE Teacher of the Year award for 2018–2019.

  4. 2020

    Proverbot9001 generates proofs

    In 2020, he coauthors Proverbot9001, a proof-search system that uses machine learning to produce software correctness proofs in interactive theorem provers.

  5. 2024

    Coq proof navigation

    As a coauthor of the 2024 CoqPyt paper, he presents a Python tool for interacting with Coq and extracting rich premise data. The tool supports work on LLM-based proof synthesis and repair.

  6. 2024

    Checking AI-generated code

    At CHI 2024, he coauthors a study that builds a Python editor combining an AI programming assistant with live programming. In a 17-person experiment, the team finds lower cognitive load for some AI-code validation tasks.

  7. 2025

    Rango for proof synthesis

    He coauthors Rango, an automated tool for Coq proof synthesis, in 2025. It retrieves relevant premises and similar proofs at each step, and receives an ACM SIGSOFT Distinguished Paper Award at ICSE 2025.

  8. Since November 2025

    Dean of Cornell Bowers

    He is dean of the Cornell Ann S. Bowers College of Computing and Information Science and a professor of computer science, appointed in November 2025. Before joining Cornell, he serves as chair of UC San Diego's Department of Computer Science and Engineering and helps guide the launch of its artificial-intelligence major and online master's program in data science. His recent work uses AI, machine learning and LLMs to build program proofs, and applies human-centered design and user studies to improve programming environments.

Career

  1. Since 2025Cornell UniversityDean, Cornell Ann S. Bowers College of Computing and Information Science; Professor of Computer Science
  2. From 2006University of California, San DiegoComputer Science and Engineering faculty member
  3. University of California, San DiegoChair

Education

  1. McGill UniversityComputer Engineering studies
  2. University of WashingtonPhD in Computer Science

From the biography and OpenAlex affiliations (the years of papers that list the organization), so some years are approximate.

Checked career sources: jacobsschool.ucsd.edu, cse.ucsd.edu, bowers.cornell.edu.

Colleagues

People with dated positions at the same organization in the same years.

Sources and credits

Photo: We have no published photo of Sorin Lerner yet. Send us a free-licensed photo.

  1. Automatically Proving the Correctness of Compiler Optimizations web.cs.ucla.edu. Checked 27 October 2026.
  2. Faculty Profiles | Jacobs School of Engineering jacobsschool.ucsd.edu. Checked 27 October 2026.
  3. Congrats Sorin Lerner: CSE’s 2018-19 Teacher of the Year cse.ucsd.edu. Checked 27 October 2026.
  4. Generating Correctness Proofs with Neural Networks arxiv.org. Checked 27 October 2026.
  5. CoqPyt: Proof Navigation in Python in the Era of LLMs arxiv.org. Checked 27 October 2026.
  6. Sorin Lerner cs.cornell.edu. Checked 27 October 2026.
  7. Validating AI-Generated Code with Live Programming arxiv.org. Checked 27 October 2026.
  8. Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification conf.researchr.org. Checked 27 October 2026.
  9. ACM SIGSOFT Distinguished Paper Award at ICSE 2025 joaoff.com. Checked 27 October 2026.
  10. Sorin Lerner | Cornell Bowers bowers.cornell.edu. Checked 27 October 2026.