Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications

Xusheng Luo, Changliu Liu

TL;DR

This work proposes the first coupled robustness verification framework for heatmap-based keypoint detectors that bounds the joint deviation across all keypoints, capturing their interdependencies and downstream task requirements.

Abstract

Keypoint detection underpins many vision tasks, including pose estimation, viewpoint recovery, and 3D reconstruction, yet modern neural models remain vulnerable to small input perturbations. Despite its importance, formal robustness verification for keypoint detectors is largely unexplored due to high-dimensional inputs and continuous coordinate outputs. We propose the first coupled robustness verification framework for heatmap-based keypoint detectors that bounds the joint deviation across all keypoints, capturing their interdependencies and downstream task requirements. Unlike prior decoupled, classification-style approaches that verify each keypoint independently and yield conservative guarantees, our method verifies collective behavior. We formulate verification as a falsification problem using a mixed-integer linear program (MILP) that combines reachable heatmap sets with a polytope encoding joint deviation constraints. Infeasibility certifies robustness, while feasibility provides counterexamples, and we prove the method is sound: if it certifies the model as robust, then the keypoint detection model is guaranteed to be robust. Experiments show that our coupled approach achieves high verified rates and remains effective under strict error thresholds where decoupled methods fail.

From Decoupled to Coupled: Robustness Verification for Learning-based Keypoint Detection with Joint Specifications

TL;DR

This work proposes the first coupled robustness verification framework for heatmap-based keypoint detectors that bounds the joint deviation across all keypoints, capturing their interdependencies and downstream task requirements.

Abstract

Keypoint detection underpins many vision tasks, including pose estimation, viewpoint recovery, and 3D reconstruction, yet modern neural models remain vulnerable to small input perturbations. Despite its importance, formal robustness verification for keypoint detectors is largely unexplored due to high-dimensional inputs and continuous coordinate outputs. We propose the first coupled robustness verification framework for heatmap-based keypoint detectors that bounds the joint deviation across all keypoints, capturing their interdependencies and downstream task requirements. Unlike prior decoupled, classification-style approaches that verify each keypoint independently and yield conservative guarantees, our method verifies collective behavior. We formulate verification as a falsification problem using a mixed-integer linear program (MILP) that combines reachable heatmap sets with a polytope encoding joint deviation constraints. Infeasibility certifies robustness, while feasibility provides counterexamples, and we prove the method is sound: if it certifies the model as robust, then the keypoint detection model is guaranteed to be robust. Experiments show that our coupled approach achieves high verified rates and remains effective under strict error thresholds where decoupled methods fail.
Paper Structure (32 sections, 1 theorem, 24 equations, 8 figures, 9 tables)

This paper contains 32 sections, 1 theorem, 24 equations, 8 figures, 9 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Formal verification of neural networks
  4. Certification of keypoint detection
  5. Background
  6. Keypoint detection
  7. Verification of neural networks
  8. Problem Formulation
  9. Robustness as Feasibility of the MILP
  10. A point inside the reachable set and out-of-bound keypoint errors
  11. Dynamic indexing and and maximality check under keypoint deviations
  12. Binary indicator of ${\mathbf Z}$ at indexed location $({\mathbf v}_0 + \delta {\mathbf v})$.
  13. Extracting values indexed by $({\mathbf v}_0 + \delta {\mathbf v})$.
  14. Finding a counterexample.
  15. Pruning the size of MILP
  16. ...and 17 more sections

Key Result

theorem 1

Our approach is sound: if it certifies the model as robust, then the keypoint detection model is guaranteed to be robust.

Figures (8)

  • Figure 1: Overview of the keypoint detection pipeline and the proposed verification framework. A thick red dashed line divides keypoint detection (above) and verification (below). A seed image ${\mathbf X}_0$ where an airplane is parking at the airport is processed by the model to identify keypoints, which are marked as green dots. The verification framework takes as input the seed image ${\mathbf X}_0$ and a set of perturbed images ${\mathbf X}$ (with local perturbations indicated by red circles) that form the convex hull ${\mathcal{X}}$, along with the keypoint error bound $\delta{\mathcal{V}}$. By checking the feasibility of the MILP that is derived from the reachable set ${\mathcal{Z}}$ of the model and the keypoint error bound $\delta {\mathcal{V}}$, the method returns whether the model is robust.
  • Figure 2: An illustration of dynamic indexing for the first keypoint: the green grid indicates the ground-truth keypoint location, while the red grid represents the perturbed keypoint position. The index deviation (1, -1) retrieves the value $Z_{31}$.
  • Figure : (a)(b)(c)
  • Figure : (a) center (b) generator (c) prediction
  • Figure : (a)(b)(c)
  • ...and 3 more figures

Theorems & Definitions (5)

  • theorem 1: Soundness
  • proof
  • remark 1
  • Example 1
  • Example \ref{exmp:comparison}