Jonathan Laurent

I am a PhD candidate at Carnegie Mellon University and a former student of the École Normale Supérieure (Paris). My current research interests lie at the intersection of machine learning and automated theorem proving. My goal is to implement an AlphaZero-like agent capable of self-learning to prove and discover mathematical theorems without human supervision.

Previously, I developed techniques to uncover the causal structure of simulation trajectories generated from rule-based models of complex biochemical systems, in collaboration with Harvard Medical School. I am also passionate about teaching and programming in Julia or OCaml.

Email address: jonathan.laurent@cs.cmu.edu
Jonathan Laurent

Education

Carnegie Mellon University, Pittsburgh

PhD in Computer Science.

2017 – Present
École Normale Supérieure de Cachan, Cachan

MSc in Machine Learning, awarded with highest honors.

Master Vision et Apprentissage”, department of mathematics. Coursework

2016
École Normale Supérieure, Paris

BSc and MSc in Computer Science.

Diplôme en Sciences de l’ENS, spécialité informatique”. Coursework

2014 – 2016
Lycée Louis-Le-Grand, Paris

Classes Préparatoires aux Grandes Écoles (MPSI-MP*)

Preparatory courses to nationwide competitive exams in mathematics (major), physics and computer science. Admitted to the École Normale Supérieure in computer science, ranked 11th.

2011 – 2013

Research Experience

PhD in Computer Science at Carnegie Mellon University

I am currently a PhD student in Computer Science at Carnegie Mellon University). I have been developing techniques to uncover the causal structure of simulation trajectories generated from rule-based models of complex biochemical systems, in collaboration with the team of Walter Fontana at Harvard Medical School. From 2016 to 2018, I was advised by Jean Yang. I have been advised by Professor André Platzer since.

Fall 2016 – Present
Research Internship at IRIF

In the “PPS” team of the “Research Institute on the Foundations of Computer Science”, I developped a tactic for the Coq proof assistant that automatically suggests lemmas for proving the current goal. It relies on a statistical model of lemma relevance, which I fitted on a large corpora of formalized mathematics (the CoRN library). Report Code

March – August 2016
Research Internship at Harvard Medical School

In the team of Professor Walter Fontana, I developed a formalism to capture the notion of a biological pathway, along with some techniques to uncover pathways in networks of protein-protein interactions modelled using the Kappa language. Report

March – August 2015
Summer Internship at NASA Langley Research Center

I spent three months at the NASA Langley Research Center, under the supervision of Alwyn Goodloe. I developped the “Copilot Theorem” library, which enables fully-automated verification of safety properties of real-time embedded programs written in the Copilot language. Paper Talk Slides Code

June – August 2014

Teaching Experience

Here is a copy of my teaching statement.
Teaching Assistant for "Logical Foundations of Cyberphysical Systems"

I was a Teaching Assistant for the the Logical Foundations of Cyberphysical Systems class taught by André Platzer at CMU. I created class material optimized for remote learning (due to the COVID pandemic) and taught weekly hybrid recitations. I was nominated to CMU’s Alan Perlis Teaching Award (see my statement).

Selected Student Feedback

Fall 2020
Teaching Assistant for a Software Verification Class

I was a Teaching Assistant for an introductory software verification class (15-414), taught by Matt Fredrikson and André Plazer. In particular, I designed a set of five labs relying on the Why3 verification platform, which led students to writing a fully verified implementation of a SAT solver with unit propagation. I was also responsible for teaching the two lectures introducing the Why3 platform. Selected Student Feedback

Fall 2017
Oral Examiner in Mathematics

I was an oral examiner in mathematics at Lycée Condorcet and then Lycée Louis-Le-Grand. Every week, I met with six freshmen during two one-hour sessions and trained them for the oral entrance examinations of the French Grandes Écoles. A selection of some of my favorite exercises can be found here (currated with Léonard Blier).

2015 – 2016

Publications

Conference and Journal Papers

Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis
Jonathan Laurent, André Platzer Abstract Paper
NeurIPS 2022
A Trace Query Language for Kappa
Jonathan Laurent, Hector Medina Abarca, Pierre Boutillier, Jean Yang, Walter Fontana Abstract Paper
CMSB 2018
Counterfactual Resimulation for Causal Analysis of Rule-Based Models
Jonathan Laurent, Jean Yang, Walter Fontana Abstract Paper
IJCAI 2018
Assuring The Guardians
Jonathan Laurent, Alwyn Goodloe, Lee Pike Abstract Paper
RV 2015

Workshop Papers and Technical Reports

Causal Analysis of Rule-Based Models by Counterfactual Reasoning
Jonathan Laurent, Jean Yang, Walter Fontana Abstract Paper
SASB 2017
Suggesting Relevant Lemmas by Learning From Succesful Proofs
Jonathan Laurent, Internship Report Abstract Paper Code
2016
Causal Analysis of Rule-Based Models of Signaling Pathways
Jonathan Laurent’s Master Thesis Abstract Paper
2015

Selected Talks

Causal Analysis of Rule-Based Models through Counterfactual Reasoning
AI seminar, Carnegie Mellon University, Pittsburgh.
November 2018
Harvard PL Seminar, Boston.
December 2017
University of Alabama, Birmingham.
September 2017
PL Lunch, Carnegie Mellon University, Pittsburgh.
September 2017
SASB Workshop, New-York.
August 2017
Uncovering Pathways in Biomolecular Interaction Networks
PL Lunch, Carnegie Mellon University, Pittsburgh.
April 2017
Peut-on tout calculer ?
Lycée Louis-Le-Grand, Paris.
December 2014
SMT-based Model-Checking Techniques for the Verification of Synchronous Dataflow Programs
National Institute of Aerospace, Hampton.
August 2014

Honors and Awards

Nominated for Carnegie Mellon University’s Allan Perlis Teaching Award
2021
Programming Languages Mentoring Workshop (PLMW) Scholarship. Details
2017
Princeton University Graduate School’s Dean Grant, declined. Details
2016
University of Washington’s CSE Distinguished Graduate Student Award, declined. Details
2016
Ranked 4th at the Google HashCode programming contest, with team <$><*>.
2014
Admitted to the École Normale Supérieure in Computer Science, ranked 11th nationwide.
2013

Professional Service

External Reviewer for: OOPSLA 2018, FASE 2019, LICS 2020, ICCPS 2020, CADE 2021, ICCPS 2022, IJCAR 2022, FM 2023.
Organizer of the weekly PL Lunch at Carnegie Mellon University.
Spring 2018

Skills

Programming

  • I am an experienced programmer in OCaml, Haskell, Python and Julia.
  • I also have some significant programming experience in C++.

Languages

  • My mother tongue is French and I am fluent in English.