63 lines
2.5 KiB
Markdown
63 lines
2.5 KiB
Markdown
# 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 a set
|
|
of constraints and check to see whether or not all of the constraints can be
|
|
satisfied. Safety conditions are encoded as the *negation* of the safety constraint.
|
|
That way, if a safety condition is violated, the SMT solver will pick it up as a
|
|
counter example.
|
|
|
|
MILP based solvers are Mixed Integer Linear Programming solvers. MILPs use
|
|
linear programming where certain constraints are integers to reduce the solving space.
|
|
|
|
**What is the supporting evidence?**
|
|
|
|
**What are the key findings?**
|
|
Local robustness
|
|
|
|
# Third Pass
|
|
**Recreation Notes:**
|
|
|
|
**Hidden Findings:**
|
|
|
|
**Weak Points? Strong Points?**
|