Logically Sound Arguments for the Effectiveness of ML Safety Measures
This work addresses safety assurance for ML in critical applications like autonomous driving, but it is incremental as it builds on known detection weaknesses and formal methods.
The paper tackles the problem of ensuring rigorous safety arguments for machine learning functions by sharpening metrics for pedestrian detection weaknesses and introducing a conservative post-processor. It proposes a semi-formal assurance case and formal proof obligations, using theorem proving to uncover missing claims and limitations in existing argumentation rules.
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.