# Specifying and Testing k-Safety Properties for Machine-Learning Models

arXiv: https://arxiv.org/abs/2206.06054 · HTML: https://mlsanity.com/paper/2206.06054/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 73 references that are in the map.
- First posted on arXiv 13 Jun 2022.

## Builds on (most cited first, 26 of 26)

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [Speech Commands: A Dataset for Limited-Vocabulary Speech Recognition](https://mlsanity.com/paper/1804.03209/) (2018)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Universal Sentence Encoder](https://mlsanity.com/paper/1803.11175/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [DeepTest: Automated Testing of Deep-Neural-Network-driven Autonomous Cars](https://mlsanity.com/paper/1708.08559/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Fairness Testing: Testing Software for Discrimination](https://mlsanity.com/paper/1709.03221/) (2017)
- [Automated Directed Fairness Testing](https://mlsanity.com/paper/1807.00468/) (2018)
- [Metamorphic Testing: A New Approach for Generating Next Test Cases](https://mlsanity.com/paper/2002.12543/) (2020)
- [Concolic Testing for Deep Neural Networks](https://mlsanity.com/paper/1805.00089/) (2018)
- [Feature-Guided Black-Box Safety Testing of Deep Neural Networks](https://mlsanity.com/paper/1710.07859/) (2017)
- [Probabilistic Verification of Fairness Properties via Concentration](https://mlsanity.com/paper/1812.02573/) (2018)
- [Perfectly Parallel Fairness Certification of Neural Networks](https://mlsanity.com/paper/1912.02499/) (2019)
- [Identifying Implementation Bugs in Machine Learning based Image Classifiers using Metamorphic Testing](https://mlsanity.com/paper/1808.05353/) (2018)
- [Improving Neural Network Verification through Spurious Region Guided Refinement](https://mlsanity.com/paper/2010.07722/) (2020)
- [Structure-Invariant Testing for Machine Translation](https://mlsanity.com/paper/1907.08710/) (2019)
- [Testing DNN Image Classifiers for Confusion & Bias Errors](https://mlsanity.com/paper/1905.07831/) (2019)
- [Make Sure You're Unsure: A Framework for Verifying Probabilistic Specifications](https://mlsanity.com/paper/2102.09479/) (2021)
- [A Declarative Metamorphic Testing Framework for Autonomous Driving](https://mlsanity.com/paper/2012.10672/) (2020)
- [NEUROSPF: A tool for the Symbolic Analysis of Neural Networks](https://mlsanity.com/paper/2103.00124/) (2021)

## Built on by (most cited first, 5 of 5)

- [Evaluating Superhuman Models with Consistency Checks](https://mlsanity.com/paper/2306.09983/) (2023)
- [Consistency Checks for Language Model Forecasters](https://mlsanity.com/paper/2412.18544/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Context-Aware Testing: A New Paradigm for Model Testing with Large Language Models](https://mlsanity.com/paper/2410.24005/) (2024)
- [Automatically Testing Functional Properties of Code Translation Models](https://mlsanity.com/paper/2309.12813/) (2023)

## Abstract (arXiv)

Machine-learning models are becoming increasingly prevalent in our lives, for instance assisting in image-classification or decision-making tasks. Consequently, the reliability of these models is of critical importance and has resulted in the development of numerous approaches for validating and verifying their robustness and fairness. However, beyond such specific properties, it is challenging to specify, let alone check, general functional-correctness expectations from models. In this paper, we take inspiration from specifications used in formal methods, expressing functional-correctness properties by reasoning about k different executions, so-called k-safety properties. Considering a credit-screening model of a bank, the expected property that "if a person is denied a loan and their income decreases, they should still be denied the loan" is a 2-safety property. Here, we show the wide applicability of k-safety properties for machine-learning models and present the first specification language for expressing them. We also operationalize the language in a framework for automatically validating such properties using metamorphic testing. Our experiments show that our framework is effective in identifying property violations, and that detected bugs could be used to train better models.