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.
翻译:我们调查了在机器学习功能安全性的论点中实现足够严格的问题。 通过考虑基于 DNN 的 2D 绑定箱检测算法的已知弱点,我们通过将其与安全目标挂钩,强化了不精确行人定位的度量。 精细化导致在标准非最大压抑之后引入保守的后处理器作为反制措施。 然后我们提出了一个半正式的保证案例,用于论证后处理器的有效性,该案例被进一步转化为正式的证明义务,以证明这些论点的正确性。 应用理论证明不仅发现有必要引入缺失的索赔和数学概念,而且还暴露了在半正式论证中使用的Dempster-Shafer规则的局限性。