All proofs relating maximum clique, maximum consensus, and group-k consistency bounds were formally verified in Lean, with the formalization released online.
Abstract
Maximum clique and maximum consensus are widely used formulations for robust point cloud registration in robotics. Maximum consensus seeks one transformation that aligns as many matches as possible, while maximum clique selects matches through pairwise distance tests. Maximum clique is often used as a substitute for or an approximation to maximum consensus, with empirical evidence suggesting a close relationship. However, how closely the two formulations agree is not fully understood. We study this relationship theoretically. We show that a maximum clique can have arbitrarily large alignment error and be arbitrarily larger than the maximum consensus set at any fixed positive tolerance, and derive geometric conditions that bound this error. When rotation is fixed, we derive sharp error bounds and tests that exactly characterize maximum consensus for the translation subproblem. Finally, we study group-$k$ consistency, which tests groups of $k$ matches, and determine the smallest group sizes that guarantee alignment error bounds independent of point cloud scale and geometry. These are $d+1$ for rotations and translations and $d+2$ when reflections are allowed, in dimensions $d\ge 2$. Interactive examples and proof verification using the Lean theorem prover are available at https://ariarobotics.github.io/mc-vs-mc-registration/.
Problem
Robust point cloud registration often uses maximum clique (pairwise distance tests) as a substitute for maximum consensus (one transformation aligning the most matches). How closely the two formulations agree had not been characterized theoretically.
Approach
The authors analyze alignment error for pairwise-consistent and group-k-consistent correspondence sets. They use a zero-sum combination lemma, Jung's theorem for the translation-only subproblem, near-isometry theory, and Procrustes analysis. Counterexamples show where these consistency tests fail, and all proofs are formally verified in Lean.
Results
A maximum clique can have arbitrarily large alignment error and can be arbitrarily larger than the maximum consensus set at any fixed positive tolerance. For fixed rotation, sharp Jung-type bounds are derived, and group-(d+1) consistency exactly characterizes maximum consensus. The smallest group sizes that guarantee scale-independent error bounds are d+1 for proper rigid motions and d+2 when reflections are allowed, for d≥2.
(c) Maximum clique alignment(d) Maximum consensus alignment