Automated Reasoning with Machine Learning

Reasoning and learning are two fundamental piceces of (either artificial or natural) intelligence.
This seminar course is designed to introduce the cutting-edge research on combining logical reasoning with machine learning.
We will first study foundational ideas and engineering tricks behind modern reasoning engines, such as Boolean Satisfiability (SAT) solvers, Satisfiability modulo Theories (SMT) solvers, and domain-specific solvers.
We will then survey recent work that use machine learning to improve reasoning systems as well as the other way around.
Specifically, this course will cover the following topics -- Boolean satisfiability (SAT), Satisifiability module Theories (SMT), program analysis and synthesis, (inductive) logic programming, and neuro-symoblic methods.

At the end of this course, you will:

- Understand how SAT/SMT solvers work and use them to solve interesting challenges.
- Learn promises and articulate limitations of current machine learning and program reasoning research.
- Constructively critique research papers, and deliver a tutorial style presentation.
- Practice your research skills through a full cycle, i.e., propose ↠ implement & evaluate ↠ present & get feedback ↠ final report.

Students are expected to have some basic knowledge of machine learning, algorithms and data structures, and programming skills (e.g., Python + C family languages). Ideally, students should have already taken the following courses (or equivalent ones):

- CSC311H1 Introduction to Machine Learning
- CSC324H1 Principles of Programming Languages
- CSC373H1 Algorithm Design, Analysis & Complexity

- Pop-quizzes & Class Participation: 10%
- One Assignment: 15%
- In-Class Paper presentation: 15%
- Project (proposal 15%, presentation 20%, report 25%)

- The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability by Donald Knuth
- Handbook of Satisfiability by Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh
- Decision Procedures -- An Algorithmic Point of View by Daniel Kroening and Ofer Strichman
- The Calculus of Computation by Aaron R. Bradley and Zohar Manna
- Pattern recognition and Machine Learning by Christopher Bishop
- Deep Learning by Ian Goodfellow, Yoshua Bengio, and Aaron Courville