-
Joint Semi-supervised 3D Super-Resolution and Segmentation with Mixed Adversarial Gaussian Domain Adaptation
Authors:
Nicolo Savioli,
Antonio de Marvao,
Wenjia Bai,
Shuo Wang,
Stuart A. Cook,
Calvin W. L. Chin,
Daniel Rueckert,
Declan P. O'Regan
Abstract:
Optimising the analysis of cardiac structure and function requires accurate 3D representations of shape and motion. However, techniques such as cardiac magnetic resonance imaging are conventionally limited to acquiring contiguous cross-sectional slices with low through-plane resolution and potential inter-slice spatial misalignment. Super-resolution in medical imaging aims to increase the resoluti…
▽ More
Optimising the analysis of cardiac structure and function requires accurate 3D representations of shape and motion. However, techniques such as cardiac magnetic resonance imaging are conventionally limited to acquiring contiguous cross-sectional slices with low through-plane resolution and potential inter-slice spatial misalignment. Super-resolution in medical imaging aims to increase the resolution of images but is conventionally trained on features from low resolution datasets and does not super-resolve corresponding segmentations. Here we propose a semi-supervised multi-task generative adversarial network (Gemini-GAN) that performs joint super-resolution of the images and their labels using a ground truth of high resolution 3D cines and segmentations, while an unsupervised variational adversarial mixture autoencoder (V-AMA) is used for continuous domain adaptation. Our proposed approach is extensively evaluated on two transnational multi-ethnic populations of 1,331 and 205 adults respectively, delivering an improvement on state of the art methods in terms of Dice index, peak signal to noise ratio, and structural similarity index measure. This framework also exceeds the performance of state of the art generative domain adaptation models on external validation (Dice index 0.81 vs 0.74 for the left ventricle). This demonstrates how joint super-resolution and segmentation, trained on 3D ground-truth data with cross-domain generalization, enables robust precision phenoty** in diverse populations.
△ Less
Submitted 16 July, 2021;
originally announced July 2021.
-
Explainable Anatomical Shape Analysis through Deep Hierarchical Generative Models
Authors:
Carlo Biffi,
Juan J. Cerrolaza,
Giacomo Tarroni,
Wenjia Bai,
Antonio de Marvao,
Ozan Oktay,
Christian Ledig,
Loic Le Folgoc,
Konstantinos Kamnitsas,
Georgia Doumou,
**ming Duan,
Sanjay K. Prasad,
Stuart A. Cook,
Declan P. O'Regan,
Daniel Rueckert
Abstract:
Quantification of anatomical shape changes currently relies on scalar global indexes which are largely insensitive to regional or asymmetric modifications. Accurate assessment of pathology-driven anatomical remodeling is a crucial step for the diagnosis and treatment of many conditions. Deep learning approaches have recently achieved wide success in the analysis of medical images, but they lack in…
▽ More
Quantification of anatomical shape changes currently relies on scalar global indexes which are largely insensitive to regional or asymmetric modifications. Accurate assessment of pathology-driven anatomical remodeling is a crucial step for the diagnosis and treatment of many conditions. Deep learning approaches have recently achieved wide success in the analysis of medical images, but they lack interpretability in the feature extraction and decision processes. In this work, we propose a new interpretable deep learning model for shape analysis. In particular, we exploit deep generative networks to model a population of anatomical segmentations through a hierarchy of conditional latent variables. At the highest level of this hierarchy, a two-dimensional latent space is simultaneously optimised to discriminate distinct clinical conditions, enabling the direct visualisation of the classification space. Moreover, the anatomical variability encoded by this discriminative latent space can be visualised in the segmentation space thanks to the generative properties of the model, making the classification task transparent. This approach yielded high accuracy in the categorisation of healthy and remodelled left ventricles when tested on unseen segmentations from our own multi-centre dataset as well as in an external validation set, and on hippocampi from healthy controls and patients with Alzheimer's disease when tested on ADNI data. More importantly, it enabled the visualisation in three-dimensions of both global and regional anatomical features which better discriminate between the conditions under exam. The proposed approach scales effectively to large populations, facilitating high-throughput analysis of normal anatomy and pathology in large-scale studies of volumetric imaging.
△ Less
Submitted 4 January, 2020; v1 submitted 28 June, 2019;
originally announced July 2019.
-
3D High-Resolution Cardiac Segmentation Reconstruction from 2D Views using Conditional Variational Autoencoders
Authors:
Carlo Biffi,
Juan J. Cerrolaza,
Giacomo Tarroni,
Antonio de Marvao,
Stuart A. Cook,
Declan P. O'Regan,
Daniel Rueckert
Abstract:
Accurate segmentation of heart structures imaged by cardiac MR is key for the quantitative analysis of pathology. High-resolution 3D MR sequences enable whole-heart structural imaging but are time-consuming, expensive to acquire and they often require long breath holds that are not suitable for patients. Consequently, multiplanar breath-hold 2D cine sequences are standard practice but are disadvan…
▽ More
Accurate segmentation of heart structures imaged by cardiac MR is key for the quantitative analysis of pathology. High-resolution 3D MR sequences enable whole-heart structural imaging but are time-consuming, expensive to acquire and they often require long breath holds that are not suitable for patients. Consequently, multiplanar breath-hold 2D cine sequences are standard practice but are disadvantaged by lack of whole-heart coverage and low through-plane resolution. To address this, we propose a conditional variational autoencoder architecture able to learn a generative model of 3D high-resolution left ventricular (LV) segmentations which is conditioned on three 2D LV segmentations of one short-axis and two long-axis images. By only employing these three 2D segmentations, our model can efficiently reconstruct the 3D high-resolution LV segmentation of a subject. When evaluated on 400 unseen healthy volunteers, our model yielded an average Dice score of $87.92 \pm 0.15$ and outperformed competing architectures.
△ Less
Submitted 28 February, 2019;
originally announced February 2019.
-
Uniform, Integral and Feasible Proofs for the Determinant Identities
Authors:
Iddo Tzameret,
Stephen A. Cook
Abstract:
Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over $GF(2)$ in Hrubes-Tzameret [SICOMP'15]. Specifically, we show that the multiplicativity of the determinant function and the Cayley-Hamilton theorem over the integers are prov…
▽ More
Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over $GF(2)$ in Hrubes-Tzameret [SICOMP'15]. Specifically, we show that the multiplicativity of the determinant function and the Cayley-Hamilton theorem over the integers are provable in the bounded arithmetic theory $\mathbf{VNC}^2$; the latter is a first-order theory corresponding to the complexity class $\mathbf{NC}^2$ consisting of problems solvable by uniform families of polynomial-size circuits and $O(\log ^2 n)$-depth. This also establishes the existence of uniform polynomial-size $\mathbf{NC}^2$-Frege proofs of the basic determinant identities over the integers (previous propositional proofs hold only over the two element field).
△ Less
Submitted 10 November, 2018;
originally announced November 2018.
-
Deep learning cardiac motion analysis for human survival prediction
Authors:
Ghalib A. Bello,
Timothy J. W. Dawes,
**ming Duan,
Carlo Biffi,
Antonio de Marvao,
Luke S. G. E. Howard,
J. Simon R. Gibbs,
Martin R. Wilkins,
Stuart A. Cook,
Daniel Rueckert,
Declan P. O'Regan
Abstract:
Motion analysis is used in computer vision to understand the behaviour of moving objects in sequences of images. Optimising the interpretation of dynamic biological systems requires accurate and precise motion tracking as well as efficient representations of high-dimensional motion trajectories so that these can be used for prediction tasks. Here we use image sequences of the heart, acquired using…
▽ More
Motion analysis is used in computer vision to understand the behaviour of moving objects in sequences of images. Optimising the interpretation of dynamic biological systems requires accurate and precise motion tracking as well as efficient representations of high-dimensional motion trajectories so that these can be used for prediction tasks. Here we use image sequences of the heart, acquired using cardiac magnetic resonance imaging, to create time-resolved three-dimensional segmentations using a fully convolutional network trained on anatomical shape priors. This dense motion model formed the input to a supervised denoising autoencoder (4Dsurvival), which is a hybrid network consisting of an autoencoder that learns a task-specific latent code representation trained on observed outcome data, yielding a latent representation optimised for survival prediction. To handle right-censored survival outcomes, our network used a Cox partial likelihood loss function. In a study of 302 patients the predictive accuracy (quantified by Harrell's C-index) was significantly higher (p < .0001) for our model C=0.73 (95$\%$ CI: 0.68 - 0.78) than the human benchmark of C=0.59 (95$\%$ CI: 0.53 - 0.65). This work demonstrates how a complex computer vision task using high-dimensional medical image data can efficiently predict human survival.
△ Less
Submitted 8 October, 2018;
originally announced October 2018.
-
The Complexity of the Comparator Circuit Value Problem
Authors:
Stephen A. Cook,
Yuval Filmus,
Dai Tri Man Le
Abstract:
In 1990 Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem (CCV). He and Mayr showed that NL \subseteq CC \subseteq P, and proved that in addition to CCV several other problems are complete for CC, including the stable marriage problem, and finding the lexicographically first maximal matching in a bipartite graph. We are i…
▽ More
In 1990 Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem (CCV). He and Mayr showed that NL \subseteq CC \subseteq P, and proved that in addition to CCV several other problems are complete for CC, including the stable marriage problem, and finding the lexicographically first maximal matching in a bipartite graph. We are interested in CC because we conjecture that it is incomparable with the parallel class NC which also satisfies NL \subseteq NC \subseteq P, and note that this conjecture implies that none of the CC-complete problems has an efficient polylog time parallel algorithm. We provide evidence for our conjecture by giving oracle settings in which relativized CC and relativized NC are incomparable.
We give several alternative definitions of CC, including (among others) the class of problems computed by uniform polynomial-size families of comparator circuits supplied with copies of the input and its negation, the class of problems AC^0-reducible to CCV, and the class of problems computed by uniform AC^0 circuits with CCV gates. We also give a machine model for CC, which corresponds to its characterization as log-space uniform polynomial-size families of comparator circuits. These various characterizations show that CC is a robust class. The main technical tool we employ is universal comparator circuits.
Other results include a simpler proof of NL \subseteq CC, and an explanation of the relation between the Gale-Shapley algorithm and Subramanian's algorithm for stable marriage.
This paper continues the previous work of Cook, Lê and Ye which focused on Cook-Nguyen style uniform proof complexity, answering several open questions raised in that paper.
△ Less
Submitted 25 July, 2013; v1 submitted 13 August, 2012;
originally announced August 2012.
-
Complexity Classes and Theories for the Comparator Circuit Value Problem
Authors:
Stephen A. Cook,
Dai Tri Man Le,
Yuli Ye
Abstract:
Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem. He proved that several other problems are complete for CC, including the stable marriage problem, and finding the lexicographical first maximal matching in a bipartite graph. We suggest alternative definitions of CC based on different reducibilities and introduce a two-so…
▽ More
Subramanian defined the complexity class CC as the set of problems log-space reducible to the comparator circuit value problem. He proved that several other problems are complete for CC, including the stable marriage problem, and finding the lexicographical first maximal matching in a bipartite graph. We suggest alternative definitions of CC based on different reducibilities and introduce a two-sorted theory VCC* based on one of them. We sharpen and simplify Subramanian's completeness proofs for the above two problems and formalize them in VCC*.
△ Less
Submitted 4 October, 2011; v1 submitted 21 June, 2011;
originally announced June 2011.
-
Formalizing Randomized Matching Algorithms
Authors:
Dai Tri Man Le,
Stephen A. Cook
Abstract:
Using Jeřábek 's framework for probabilistic reasoning, we formalize the correctness of two fundamental RNC^2 algorithms for bipartite perfect matching within the theory VPV for polytime reasoning. The first algorithm is for testing if a bipartite graph has a perfect matching, and is based on the Schwartz-Zippel Lemma for polynomial identity testing applied to the Edmonds polynomial of the graph.…
▽ More
Using Jeřábek 's framework for probabilistic reasoning, we formalize the correctness of two fundamental RNC^2 algorithms for bipartite perfect matching within the theory VPV for polytime reasoning. The first algorithm is for testing if a bipartite graph has a perfect matching, and is based on the Schwartz-Zippel Lemma for polynomial identity testing applied to the Edmonds polynomial of the graph. The second algorithm, due to Mulmuley, Vazirani and Vazirani, is for finding a perfect matching, where the key ingredient of this algorithm is the Isolating Lemma.
△ Less
Submitted 9 August, 2012; v1 submitted 27 March, 2011;
originally announced March 2011.
-
Formal Theories for Linear Algebra
Authors:
Stephen A Cook,
Lila A Fontes
Abstract:
We introduce two-sorted theories in the style of [CN10] for the complexity classes \oplusL and DET, whose complete problems include determinants over Z2 and Z, respectively. We then describe interpretations of Soltys' linear algebra theory LAp over arbitrary integral domains, into each of our new theories. The result shows equivalences of standard theorems of linear algebra over Z2 and Z can be p…
▽ More
We introduce two-sorted theories in the style of [CN10] for the complexity classes \oplusL and DET, whose complete problems include determinants over Z2 and Z, respectively. We then describe interpretations of Soltys' linear algebra theory LAp over arbitrary integral domains, into each of our new theories. The result shows equivalences of standard theorems of linear algebra over Z2 and Z can be proved in the corresponding theory, but leaves open the interesting question of whether the theorems themselves can be proved.
△ Less
Submitted 16 March, 2012; v1 submitted 7 January, 2011;
originally announced January 2011.
