danesabo/Obsidian
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

vault backup: 2025-07-02 15:48:01

Browse Source
This commit is contained in:
Dane Sabo 2025-07-02 15:48:01 -04:00
parent 18e266df8d
commit 4fc9f94924
1 changed files with 10 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Notes on Papers/A Review of Formal Methods applied to Machine Learning.md
View File

@ -26,7 +26,8 @@ network?
**What is the main thrust?** **What is the main thrust?**
This review gives an overview of formal methods applied to machine learning. 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 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 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, assistants, model checking, and semantic static analysis, and then finally,
abstract interpretation of semantic static analysis. The last one has been abstract interpretation of semantic static analysis. The last one has been
used the most in FM of ML. used the most in FM of ML.
@ -39,7 +40,14 @@ These methods generally do not apply well to large networks (beyond
hundreds gets rough), but give the highest level of assurance. Here, there hundreds gets rough), but give the highest level of assurance. Here, there
are two more subcategories: SMT based solvers and MILP-based solvers. are two more subcategories: SMT based solvers and MILP-based solvers.
SMT solvers are Satisfiability Modulo Theory solvers. These 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
**What is the supporting evidence?** **What is the supporting evidence?**