Verification of ML Systems via Reparameterization
- URL: http://arxiv.org/abs/2007.06776v1
- Date: Tue, 14 Jul 2020 02:19:25 GMT
- Title: Verification of ML Systems via Reparameterization
- Authors: Jean-Baptiste Tristan, Joseph Tassarotti, Koundinya Vajjha, Michael L.
Wick, Anindya Banerjee
- Abstract summary: We show how a probabilistic program can be automatically represented in a theorem prover.
We also prove that the null model used in a Bayesian hypothesis test satisfies a fairness criterion called demographic parity.
- Score: 6.482926592121413
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: As machine learning is increasingly used in essential systems, it is
important to reduce or eliminate the incidence of serious bugs. A growing body
of research has developed machine learning algorithms with formal guarantees
about performance, robustness, or fairness. Yet, the analysis of these
algorithms is often complex, and implementing such systems in practice
introduces room for error. Proof assistants can be used to formally verify
machine learning systems by constructing machine checked proofs of correctness
that rule out such bugs. However, reasoning about probabilistic claims inside
of a proof assistant remains challenging. We show how a probabilistic program
can be automatically represented in a theorem prover using the concept of
\emph{reparameterization}, and how some of the tedious proofs of measurability
can be generated automatically from the probabilistic program. To demonstrate
that this approach is broad enough to handle rather different types of machine
learning systems, we verify both a classic result from statistical learning
theory (PAC-learnability of decision stumps) and prove that the null model used
in a Bayesian hypothesis test satisfies a fairness criterion called demographic
parity.
Related papers
- Neural Model Checking [10.376573742987917]
We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification.
Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic.
We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.
arXiv Detail & Related papers (2024-10-31T10:17:04Z) - Bisimulation Learning [55.859538562698496]
We compute finite bisimulations of state transition systems with large, possibly infinite state space.
Our technique yields faster verification results than alternative state-of-the-art tools in practice.
arXiv Detail & Related papers (2024-05-24T17:11:27Z) - Conformal Predictions for Probabilistically Robust Scalable Machine Learning Classification [1.757077789361314]
Conformal predictions make it possible to define reliable and robust learning algorithms.
They are essentially a method for evaluating whether an algorithm is good enough to be used in practice.
This paper defines a reliable learning framework for classification from the very beginning of its design.
arXiv Detail & Related papers (2024-03-15T14:59:24Z) - Probabilistic Safety Regions Via Finite Families of Scalable Classifiers [2.431537995108158]
Supervised classification recognizes patterns in the data to separate classes of behaviours.
Canonical solutions contain misclassification errors that are intrinsic to the numerical approximating nature of machine learning.
We introduce the concept of probabilistic safety region to describe a subset of the input space in which the number of misclassified instances is probabilistically controlled.
arXiv Detail & Related papers (2023-09-08T22:40:19Z) - Automated Learning of Interpretable Models with Quantified Uncertainty [0.0]
We introduce a new framework for genetic-programming-based symbolic regression (GPSR)
GPSR uses model evidence to formulate replacement probability during the selection phase of evolution.
It is shown to increase interpretability, improve robustness to noise, and reduce overfitting when compared to a conventional GPSR implementation.
arXiv Detail & Related papers (2022-04-12T19:56:42Z) - CC-Cert: A Probabilistic Approach to Certify General Robustness of
Neural Networks [58.29502185344086]
In safety-critical machine learning applications, it is crucial to defend models against adversarial attacks.
It is important to provide provable guarantees for deep learning models against semantically meaningful input transformations.
We propose a new universal probabilistic certification approach based on Chernoff-Cramer bounds.
arXiv Detail & Related papers (2021-09-22T12:46:04Z) - Multi Agent System for Machine Learning Under Uncertainty in Cyber
Physical Manufacturing System [78.60415450507706]
Recent advancements in predictive machine learning has led to its application in various use cases in manufacturing.
Most research focused on maximising predictive accuracy without addressing the uncertainty associated with it.
In this paper, we determine the sources of uncertainty in machine learning and establish the success criteria of a machine learning system to function well under uncertainty.
arXiv Detail & Related papers (2021-07-28T10:28:05Z) - From Undecidability of Non-Triviality and Finiteness to Undecidability
of Learnability [0.0]
We show that there is no general-purpose procedure for rigorously evaluating whether newly proposed models indeed successfully learn from data.
For PAC binary classification, uniform and universal online learning, and exact learning through teacher-learner interactions, learnability is in general undecidable.
There is no one-size-fits-all algorithm for deciding whether a machine learning model can be successful.
arXiv Detail & Related papers (2021-06-02T18:00:04Z) - General stochastic separation theorems with optimal bounds [68.8204255655161]
Phenomenon of separability was revealed and used in machine learning to correct errors of Artificial Intelligence (AI) systems and analyze AI instabilities.
Errors or clusters of errors can be separated from the rest of the data.
The ability to correct an AI system also opens up the possibility of an attack on it, and the high dimensionality induces vulnerabilities caused by the same separability.
arXiv Detail & Related papers (2020-10-11T13:12:41Z) - A Note on High-Probability versus In-Expectation Guarantees of
Generalization Bounds in Machine Learning [95.48744259567837]
Statistical machine learning theory often tries to give generalization guarantees of machine learning models.
Statements made about the performance of machine learning models have to take the sampling process into account.
We show how one may transform one statement to another.
arXiv Detail & Related papers (2020-10-06T09:41:35Z) - Good Classifiers are Abundant in the Interpolating Regime [64.72044662855612]
We develop a methodology to compute precisely the full distribution of test errors among interpolating classifiers.
We find that test errors tend to concentrate around a small typical value $varepsilon*$, which deviates substantially from the test error of worst-case interpolating model.
Our results show that the usual style of analysis in statistical learning theory may not be fine-grained enough to capture the good generalization performance observed in practice.
arXiv Detail & Related papers (2020-06-22T21:12:31Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.