Machine learning builds a model by training it on data, not by writing a specification. That raises a question. Once the model exists, what can we prove about it? Testing measures accuracy on a sample of inputs, while formal verification asks whether a stated property holds for every input in some region [4]. The models here are neural networks, which pass inputs through layers of weighted connections to compute an output [1]. An ensemble runs several models on the same input, and soft voting combines them by averaging the probabilities they output. An ensemble with soft voting can raise accuracy and keep working if a single model fails [2]. A property of particular interest is robustness. A small, deliberate change to an input is called an adversarial perturbation, and a robust model does not let such a change flip its answer. Formal robustness verification tries to prove this for a whole region of inputs, not for sampled points alone [3, 4].
A warning runs through this part of the session: a single headline score does not make a model trustworthy. Such a score, for example overall accuracy or the area under the receiver operating characteristic curve (AUROC), can look excellent while the model still fails in ways that matter in use. So verification also checks other properties. Calibration asks whether the predicted probabilities match how often things really happen. If a well-calibrated model says 80% on many cases, the predicted outcome should occur in about 80% of them, and the expected calibration error (ECE) measures the gap [5]. Explainability asks which input features drove a given prediction. Methods like SHAP (SHapley Additive exPlanations) give each feature a share of the result, and such explanations are only useful if they stay stable under small changes [6]. Two more properties are monotonicity, where raising a meaningful input should move the prediction in the expected direction, and fairness, where the model should not disadvantage protected groups [7]. The goal is to check these properties together, not to read trust off one number.
The session's other strand keeps the goal of proving a property, but changes the object of study from a learned model to a networked system, that is, many processes that run in parallel and communicate by messages. One communication model is broadcast, where a sent message reaches all neighbours at once. Broadcast can be reliable, or unreliable if messages may be lost [10]. The basic question is one of safety, also called reachability. Can any process ever reach an error state? Usually one wants that guarantee for a whole family of systems of every size, not one fixed instance, which is the aim of parameterized verification [8, 9]. Graph grammars give a compact, rule-based way to describe such families of network topologies [11]. A recurring theme is the line between decidable and undecidable problems. Some of these questions have no general algorithm, yet adding a restriction, such as message loss or a wait-only protocol, can restore decidability [9, 10].
Keywords to look up: machine-learning verification · neural network · ensemble / soft voting · adversarial robustness · trustworthy AI · calibration (ECE) · explainable AI / SHAP · monotonicity · fairness · distributed system · broadcast communication · safety / reachability · parameterized verification · graph grammar / graph transformation · decidability · undecidability.
Sources
- I. Goodfellow, Y. Bengio, A. Courville. Deep Learning. MIT Press, 2016. deeplearningbook.org
- T. G. Dietterich. "Ensemble Methods in Machine Learning." MCS, 2000. doi.org/10.1007/3-540-45014-9_1
- I. J. Goodfellow, J. Shlens, C. Szegedy. "Explaining and Harnessing Adversarial Examples." ICLR, 2015. arxiv.org/abs/1412.6572
- G. Katz, C. Barrett, D. Dill, K. Julian, M. Kochenderfer. "Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks." CAV, 2017. doi.org/10.1007/978-3-319-63387-9_5
- C. Guo, G. Pleiss, Y. Sun, K. Q. Weinberger. "On Calibration of Modern Neural Networks." ICML, 2017. arxiv.org/abs/1706.04599
- S. M. Lundberg, S.-I. Lee. "A Unified Approach to Interpreting Model Predictions." NeurIPS, 2017. arxiv.org/abs/1705.07874
- S. Barocas, M. Hardt, A. Narayanan. Fairness and Machine Learning. MIT Press, 2023. fairmlbook.org
- S. M. German, A. P. Sistla. "Reasoning about Systems with Many Processes." JACM, 1992. doi.org/10.1145/146637.146681
- R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, J. Widder. Decidability of Parameterized Verification. Morgan & Claypool, 2015. doi.org/10.2200/S00658ED1V01Y201508DCT013
- G. Delzanno, A. Sangnier, G. Zavattaro. "Parameterized Verification of Ad Hoc Networks." CONCUR, 2010. doi.org/10.1007/978-3-642-15375-4_22
- H. Ehrig, K. Ehrig, U. Prange, G. Taentzer. Fundamentals of Algebraic Graph Transformation. Springer, 2006. doi.org/10.1007/3-540-31188-2