2.1 KiB
First Pass
Category: This is a review paper.
Context: This paper tries to keep up with where formal methods are for machine learning based systems. It is not necessarily a controls paper, but a broader machine learning paper in general.
Correctness: Really well written on the first pass. Easy to understand and things seem well cited.
Contributions: Great citations showing links to different papers and also provides nice spots for forward research. Talks about how verification needs to be done along the whole pipeline: from data prep to training to implementation. There needs to be more work on proving things about model behavior, but in general this review has a positive outlook on the field.
Clarity: Very well written, easy to understand. Except, what is abstractification of a network?
Second Pass
What is the main thrust? This review gives an overview of formal methods applied to machine learning. Formal methods has been used for ML to test for robustness for various perturbations on inputs. They start by talking about several types of formal methods, including deductive verification, design by refinement, proof assistants, model checking, and semantic static analysis, and then finally, abstract interpretation of semantic static analysis. The last one has been used the most in FM of ML.
A large part of the paper focuses on formal methods for neural network perturbation robustness. They split up the methods into two types: complete and incomplete formal methods. Complete formal methods are sound and complete. This means they do not have false positives or false negatives. These methods generally do not apply well to large networks (beyond hundreds gets rough), but give the highest level of assurance. Here, there are two more subcategories: SMT based solvers and MILP-based solvers.
SMT solvers are Satisfiability Modulo Theory solvers. These solvers
What is the supporting evidence?
What are the key findings? Local robustness
Third Pass
Recreation Notes:
Hidden Findings:
Weak Points? Strong Points?