从解耦到耦合：面向联合规格的学习型关键点检测鲁棒性验证

关键点检测是姿态估计、视点恢复和三维重建等众多视觉任务的基础，但现代神经网络模型仍对小幅输入扰动十分脆弱。尽管其重要性已备受关注，但针对关键点检测器的形式化鲁棒性验证基本未被探讨，这源于高维输入和连续坐标输出。我们提出了首个针对热图式关键点检测器的耦合鲁棒性验证框架，对所有关键点的联合偏差进行边界控制，捕捉它们的相互依赖性及下游任务需求。不同于以前解耦、以分类风格验证方法的做法——即独立验证每个关键点并产生保守保证——的框架，本方法验证的是整体行为。我们将验证建模为一次 falsification 问题，使用混合整数线性规划 (MILP) 将可达热图集合与联合偏差约束的多面体相结合。不可行性 certifies 鲁棒性，而可行性则提供反例，我们证明该方法是 sound 的：若它 certifies 模型为鲁棒，则保证关键点检测模型确实鲁棒。实验表明，本耦合方法在高验证率方面表现出色，在严格误差阈值下仍有效，而解耦方法则失败。