Certified folding-free deformable image registration: A whole-cell Jacobian certificate and a sequential variational solver
Abstract
Registration maps propagate labels, measure local volume change, and map results back through their inverses; requiring invertibility. Voxelwise checks can miss folds between grid points. We study the canonical continuous extension of a nodal displacement field by trilinear interpolation and give a test that proves its Jacobian determinant positive in every grid cell or rejects the map. The test is rigorous under IEEE 754 binary64 arithmetic (correct rounding, no contraction). With a fixed boundary, certification implies a bi-Lipschitz homeomorphism of the image domain. We introduce SeqVP, built around this certificate. A proximal Jacobian-determinant-curl formulation yields inner problems whose penalties on changes in the map, Jacobian determinant, and curl vanish to first order at the current iterate. The method decreases a fixed outer energy up to a floating-point resolution guard and certifies every committed iterate. After certified initialization, stopping at any time returns a folding-free map. A Poisson-preconditioned gradient method with Jacobian-aware step prediction and affine-scaling damping, initialized by certified handoff from an uncertified binary32 pre-optimizer, handles a 1 mm brain MRI with about 2e7 unknowns in 90 s on one GPU. On 49 held-out OASIS pairs, SeqVP achieves mean Dice 0.821 over 35 structures and 0.889 over 4 tissue classes, with certified zero folding. Gains are 0.022 and 0.025 over ANTs SyN, and 0.022 and 0.023 over uniGradICON with instance optimization at equal time (paired, Holm-adjusted p < 0.001), but maps are rougher. SeqVP is level with ANTs on LPBA40, behind it on IBSR18, and ahead of all label-free baselines on 20 large-deformation pairs. On fields from nine methods, the certificate finds non-positive-Jacobian cells in every ANTs SyN map (median 10, missed by voxelwise checks) and in maps from NiftyReg, ConvexAdam, uniGradICON, and TransMorph.
Related
- Certified Residual Quasi-Newton Methods for Distributed Variational Inequalities
- Differentiable Systematic Resampling for Variational Sequential Monte Carlo
- Sampling-Based Batch Sequential Design by Stein Variational Gradient Descent
- Posterior Regimes and Latent Deception: Variational Bayesian Inference in Hidden Markov Models for Sequential Fraud Detection in Financial Transactions
- A space-time finite element formulation for geometrically exact shear-deformable beams
BibTeX
@misc{zhao2026certified,
title = {{Certified folding-free deformable image registration: A whole-cell Jacobian certificate and a sequential variational solver}},
author = {Baihan Zhao and Zicong Zhou and Guojun Liao},
howpublished = {arXiv},
year = {2026},
month = nov,
doi = {10.48550/arxiv.2611.06954},
eprint = {2611.06954},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2611.06954},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Certified folding-free deformable image registration: A whole-cell Jacobian certificate and a sequential variational solver
AU - Baihan Zhao
AU - Zicong Zhou
AU - Guojun Liao
PY - 2026
DA - 2026/11/03
PB - arXiv
DO - 10.48550/arxiv.2611.06954
UR - https://arxiv.org/abs/2611.06954
AB - Registration maps propagate labels, measure local volume change, and map results back through their inverses; requiring invertibility. Voxelwise checks can miss folds between grid points. We study the canonical continuous extension of a nodal displacement field by trilinear interpolation and give a test that proves its Jacobian determinant positive in every grid cell or rejects the map. The test is rigorous under IEEE 754 binary64 arithmetic (correct rounding, no contraction). With a fixed boundary, certification implies a bi-Lipschitz homeomorphism of the image domain. We introduce SeqVP, built around this certificate. A proximal Jacobian-determinant-curl formulation yields inner problems whose penalties on changes in the map, Jacobian determinant, and curl vanish to first order at the current iterate. The method decreases a fixed outer energy up to a floating-point resolution guard and certifies every committed iterate. After certified initialization, stopping at any time returns a folding-free map. A Poisson-preconditioned gradient method with Jacobian-aware step prediction and affine-scaling damping, initialized by certified handoff from an uncertified binary32 pre-optimizer, handles a 1 mm brain MRI with about 2e7 unknowns in 90 s on one GPU. On 49 held-out OASIS pairs, SeqVP achieves mean Dice 0.821 over 35 structures and 0.889 over 4 tissue classes, with certified zero folding. Gains are 0.022 and 0.025 over ANTs SyN, and 0.022 and 0.023 over uniGradICON with instance optimization at equal time (paired, Holm-adjusted p < 0.001), but maps are rougher. SeqVP is level with ANTs on LPBA40, behind it on IBSR18, and ahead of all label-free baselines on 20 large-deformation pairs. On fields from nine methods, the certificate finds non-positive-Jacobian cells in every ANTs SyN map (median 10, missed by voxelwise checks) and in maps from NiftyReg, ConvexAdam, uniGradICON, and TransMorph.
ER -