# Logically Sound Arguments for the Effectiveness of ML Safety Measures

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 28 references that are in the map.
- First posted on arXiv 4 Nov 2021.

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

- [Microsoft COCO: Common Objects in Context](https://mlsanity.com/paper/1405.0312/) (2014)
- [DeepXplore: Automated Whitebox Testing of Deep Learning Systems](https://mlsanity.com/paper/1705.06640/) (2017)
- [Dynamic Head: Unifying Object Detection Heads with Attentions](https://mlsanity.com/paper/2106.08322/) (2021)
- [A Safety Framework for Critical Systems Utilising Deep Neural Networks](https://mlsanity.com/paper/2003.05311/) (2020)
- [Safety-Aware Hardening of 3D Object Detection Neural Network Systems](https://mlsanity.com/paper/2003.11242/) (2020)
- [The missing link: Developing a safety case for perception components in automated driving](https://mlsanity.com/paper/2108.13294/) (2021)
- [A Framework for Assurance of Medication Safety using Machine Learning](https://mlsanity.com/paper/2101.05620/) (2021)

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

- [Unaligned but Safe -- Formally Compensating Performance Limitations for Imprecise 2D Object Detection](https://mlsanity.com/paper/2202.05123/) (2022)
- [Towards Rigorous Design of OoD Detectors](https://mlsanity.com/paper/2306.08447/) (2023)

## Abstract (arXiv)

We investigate the issues of achieving sufficient rigor in the arguments for the safety of machine learning functions. By considering the known weaknesses of DNN-based 2D bounding box detection algorithms, we sharpen the metric of imprecise pedestrian localization by associating it with the safety goal. The sharpening leads to introducing a conservative post-processor after the standard non-max-suppression as a counter-measure. We then propose a semi-formal assurance case for arguing the effectiveness of the post-processor, which is further translated into formal proof obligations for demonstrating the soundness of the arguments. Applying theorem proving not only discovers the need to introduce missing claims and mathematical concepts but also reveals the limitation of Dempster-Shafer's rules used in semi-formal argumentation.