Logically Sound Arguments for the Effectiveness of ML Safety Measures

TL;DR

This paper enhances the rigor of safety arguments for machine learning by introducing a formal assurance case and theorem proving to validate a conservative post-processor for DNN-based pedestrian detection.

Contribution

It develops a semi-formal assurance framework and formal proof approach to verify safety measures in ML systems, addressing weaknesses in existing detection algorithms.

Findings

Identification of weaknesses in DNN pedestrian detection

Development of a conservative post-processor for safety

Formal proof obligations reveal limitations in semi-formal reasoning

Abstract

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.