Advanced Topics in Machine Learning and Formal Methods

This course will explore advanced research topics at the intersection of machine learning and formal verification methods. It will discuss the verification problems that arise in machine learning applications, such as rigorously proving their robustness, safety, fairness, correctness, and other trustworthiness properties. The course will discuss state-of-the-art formal verification techniques that are applicable to practical machine learning models, such as deep neural networks and tree ensembles, and also how to train machine learning models that follow formal specifications. In addition, it will discuss the novel use of machine learning (including foundation models and large language models) in the field of formal methods.

Instructor: Prof. Huan Zhang (huanz at illinois dot edu)
Office: CSL 262
Canvas (for homework submission): https://canvas.illinois.edu/courses/51706
TA: Junyu Zhang (junyuz6 at illinois.edu) Contact the TA for homework submission related issues and re-grading request.

To find the lecture schedule, slides, and reading assignments, please go to the Course Schedule page.

Lectures

Time: Tuesday and Thursday 2:00PM – 3:20PM
Location: 3015 Electrical & Computer Eng Bldg
Schedule: Course Schedule
Video recordings: MediaSpace

Grading

Homework (3 sets): 30%
Problems will involve some coding and pencil paper proofs
Project: 50%
Proposal: 5%
Midterm presentation: 10%
Final presentation: 10% 
Report: 20% (for purely theoretical projects without code, the report will be scaled to 25%)
Code and documentation: 5%
Paper presentation: 15%
Each student will present one research paper during the semester (10%)
When not presenting, you are still required to read all papers assigned and submit a summary before class (5%)
Participation: 5%
Class participation
Feedback on projects (feedback forms will be given during the presentation weeks)
New problem suggestions and solutions

Important Dates:

Project Proposal: 9/27
Midterm presentation: mid-October (10/15, 10/17 tentative)
Final presentations: Last week of instruction
Final report: Due on the last day of final’s week: 12/19

Homework

There will be 3 sets of individual homework. The homework problems will involve pencil-paper proofs and some coding. The homework will be concentrated on the earlier 2/3rd of the semester.

In addition, you are required to read assign papers through out the semester and submit

Homework submission: homework needs to be submitted on Canvas. Submissions through other channels will not be accepted. Homework will be due at 11:59 pm CT on the due date.

Late policy: for each late day, there will be a 20% penalty on your grade. After 5 days, late homework will not be accepted. For example, if you submitted your homework two days late and scored 90, your grade for this late homework will be 90*60%=54. For medical excuses, please email me your absence letter from the Office of the Dean of Students.

A re-grading request is accepted within 48 hours once your grade is released on Canvas. Contact the TA regarding the request.

Course Project 

You will work on a semester-long research project focusing on topics related to machine learning and verification. Often the projects become publishable.
Good project will require ~6-8 hours/week — higher towards the end of the semester.  
Start early, and get frequent feedback.
Projects should be done in a team of 2 students. If you are sure that you want to work in a larger team (3 or more people), you can make a case, and we can consider it. 
Projects will be graded based on
soundness of claims, 
significance (novelty, impact, harness), 
presentation quality, and 
effort
Advice
Choose a high-risk project that if success will make you proud
Clearly define the problem ASAP
Get feedback frequently

Office hours

Each week, I have 1.5 hours of office hours available upon appointment, except holidays/breaks. Both in-person and Zoom options are available. Before you come to my office hour, please book your appointment 24 hours in advance: zoom or in-person. After booking, you should receive a confirmation email (if not, please check your spam folder). The office hours are available for officially registered students only. If you are auditing, please email the instructor to book a meeting instead.