Showing 1–30 of 30 results for author: Cook, S

The Importance of Collective Privacy in Digital Sexual and Reproductive Health

Authors: Teresa Almeida, Maryam Mehrnezhad, Stephen Cook

Abstract: There is an abundance of digital sexual and reproductive health technologies that presents a concern regarding their potential sensitive data breaches. We analyzed 15 Internet of Things (IoT) devices with sexual and reproductive tracking services and found this ever-extending collection of data implicates many beyond the individual including partner, child, and family. Results suggest that digital… ▽ More There is an abundance of digital sexual and reproductive health technologies that presents a concern regarding their potential sensitive data breaches. We analyzed 15 Internet of Things (IoT) devices with sexual and reproductive tracking services and found this ever-extending collection of data implicates many beyond the individual including partner, child, and family. Results suggest that digital sexual and reproductive health data privacy is both an individual and collective endeavor. △ Less

Submitted 26 November, 2023; originally announced November 2023.

RAISE -- Radiology AI Safety, an End-to-end lifecycle approach

Authors: M. Jorge Cardoso, Julia Moosbauer, Tessa S. Cook, B. Selnur Erdal, Brad Genereaux, Vikash Gupta, Bennett A. Landman, Tiarna Lee, Parashkev Nachev, Elanchezhian Somasundaram, Ronald M. Summers, Khaled Younis, Sebastien Ourselin, Franz MJ Pfister

Abstract: The integration of AI into radiology introduces opportunities for improved clinical care provision and efficiency but it demands a meticulous approach to mitigate potential risks as with any other new technology. Beginning with rigorous pre-deployment evaluation and validation, the focus should be on ensuring models meet the highest standards of safety, effectiveness and efficacy for their intende… ▽ More The integration of AI into radiology introduces opportunities for improved clinical care provision and efficiency but it demands a meticulous approach to mitigate potential risks as with any other new technology. Beginning with rigorous pre-deployment evaluation and validation, the focus should be on ensuring models meet the highest standards of safety, effectiveness and efficacy for their intended applications. Input and output guardrails implemented during production usage act as an additional layer of protection, identifying and addressing individual failures as they occur. Continuous post-deployment monitoring allows for tracking population-level performance (data drift), fairness, and value delivery over time. Scheduling reviews of post-deployment model performance and educating radiologists about new algorithmic-driven findings is critical for AI to be effective in clinical practice. Recognizing that no single AI solution can provide absolute assurance even when limited to its intended use, the synergistic application of quality assurance at multiple levels - regulatory, clinical, technical, and ethical - is emphasized. Collaborative efforts between stakeholders spanning healthcare systems, industry, academia, and government are imperative to address the multifaceted challenges involved. Trust in AI is an earned privilege, contingent on a broad set of goals, among them transparently demonstrating that the AI adheres to the same rigorous safety, effectiveness and efficacy standards as other established medical technologies. By doing so, developers can instil confidence among providers and patients alike, enabling the responsible scaling of AI and the realization of its potential benefits. The roadmap presented herein aims to expedite the achievement of deployable, reliable, and safe AI in radiology. △ Less

Submitted 24 November, 2023; originally announced November 2023.

Comments: 14 pages, 3 figures

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.

Joint Motion Correction and Super Resolution for Cardiac Segmentation via Latent Optimisation

Authors: Shuo Wang, Chen Qin, Nicolo Savioli, Chen Chen, Declan O'Regan, Stuart Cook, Yike Guo, Daniel Rueckert, Wenjia Bai

Abstract: In cardiac magnetic resonance (CMR) imaging, a 3D high-resolution segmentation of the heart is essential for detailed description of its anatomical structures. However, due to the limit of acquisition duration and respiratory/cardiac motion, stacks of multi-slice 2D images are acquired in clinical routine. The segmentation of these images provides a low-resolution representation of cardiac anatomy… ▽ More In cardiac magnetic resonance (CMR) imaging, a 3D high-resolution segmentation of the heart is essential for detailed description of its anatomical structures. However, due to the limit of acquisition duration and respiratory/cardiac motion, stacks of multi-slice 2D images are acquired in clinical routine. The segmentation of these images provides a low-resolution representation of cardiac anatomy, which may contain artefacts caused by motion. Here we propose a novel latent optimisation framework that jointly performs motion correction and super resolution for cardiac image segmentations. Given a low-resolution segmentation as input, the framework accounts for inter-slice motion in cardiac MR imaging and super-resolves the input into a high-resolution segmentation consistent with input. A multi-view loss is incorporated to leverage information from both short-axis view and long-axis view of cardiac imaging. To solve the inverse problem, iterative optimisation is performed in a latent space, which ensures the anatomical plausibility. This alleviates the need of paired low-resolution and high-resolution images for supervised learning. Experiments on two cardiac MR datasets show that the proposed framework achieves high performance, comparable to state-of-the-art super-resolution approaches and with better cross-domain generalisability and anatomical plausibility. △ Less

Submitted 8 July, 2021; originally announced July 2021.

Comments: The paper is early accepted to MICCAI 2021. The codes are available at https://github.com/shuowang26/SRHeart

A Method and Analysis to Elicit User-reported Problems in Intelligent Everyday Applications

Authors: Malin Eiband, Sarah Theres Völkel, Daniel Buschek, Sophia Cook, Heinrich Hussmann

Abstract: The complex nature of intelligent systems motivates work on supporting users during interaction, for example through explanations. However, as of yet, there is little empirical evidence in regard to specific problems users face when applying such systems in everyday situations. This paper contributes a novel method and analysis to investigate such problems as reported by users: We analysed 45,448… ▽ More The complex nature of intelligent systems motivates work on supporting users during interaction, for example through explanations. However, as of yet, there is little empirical evidence in regard to specific problems users face when applying such systems in everyday situations. This paper contributes a novel method and analysis to investigate such problems as reported by users: We analysed 45,448 reviews of four apps on the Google Play Store (Facebook, Netflix, Google Maps and Google Assistant) with sentiment analysis and topic modelling to reveal problems during interaction that can be attributed to the apps' algorithmic decision-making. We enriched this data with users' co** and support strategies through a follow-up online survey (N=286). In particular, we found problems and strategies related to content, algorithm, user choice, and feedback. We discuss corresponding implications for designing user support, highlighting the importance of user control and explanations of output, rather than processes. △ Less

Submitted 4 February, 2020; originally announced February 2020.

Comments: 28 pages, 2 figures, 7 tables

ACM Class: H.m

Enabling Simulation of High-Dimensional Micro-Macro Biophysical Models through Hybrid CPU and Multi-GPU Parallelism

Authors: Steven Cook, Tamar Shinar

Abstract: Micro-macro models provide a powerful tool to study the relationship between microscale mechanisms and emergent macroscopic behavior. However, the detailed microscopic modeling may require tracking and evolving a high-dimensional configuration space at high computational cost. In this work, we present a parallel algorithm for simulation a high-dimensional micro-macro model of a gliding motility as… ▽ More Micro-macro models provide a powerful tool to study the relationship between microscale mechanisms and emergent macroscopic behavior. However, the detailed microscopic modeling may require tracking and evolving a high-dimensional configuration space at high computational cost. In this work, we present a parallel algorithm for simulation a high-dimensional micro-macro model of a gliding motility assay. We utilize a holistic approach aligning the data residency and simulation scales with the hybrid CPU and multi-GPU hardware. With a combination of algorithmic modifications, GPU optimizations, and scaling to multiple GPUs, we achieve speedup factors of up to 27 over our previous hybrid CPU-GPU implementation and up to 540 over our single-threaded implementation. This approach enables micro-macro simulations of higher complexity and resolution than would otherwise be feasible. △ Less

Submitted 12 August, 2019; originally announced August 2019.

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.

Comments: Accepted for publication in IEEE Transactions on Medical Imaging (TMI)

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.

Comments: Accepted in IEEE International Symposium on Biomedical Imaging (ISBI 2019)

Race, Ethnicity and National Origin-based Discrimination in Social Media and Hate Crimes Across 100 U.S. Cities

Authors: Kunal Relia, Zhengyi Li, Stephanie H. Cook, Rumi Chunara

Abstract: We study malicious online content via a specific type of hate speech: race, ethnicity and national-origin based discrimination in social media, alongside hate crimes motivated by those characteristics, in 100 cities across the United States. We develop a spatially-diverse training dataset and classification pipeline to delineate targeted and self-narration of discrimination on social media, accoun… ▽ More We study malicious online content via a specific type of hate speech: race, ethnicity and national-origin based discrimination in social media, alongside hate crimes motivated by those characteristics, in 100 cities across the United States. We develop a spatially-diverse training dataset and classification pipeline to delineate targeted and self-narration of discrimination on social media, accounting for language across geographies. Controlling for census parameters, we find that the proportion of discrimination that is targeted is associated with the number of hate crimes. Finally, we explore the linguistic features of discrimination Tweets in relation to hate crimes by city, features used by users who Tweet different amounts of discrimination, and features of discrimination compared to non-discrimination Tweets. Findings from this spatial study can inform future studies of how discrimination in physical and virtual worlds vary by place, or how physical and virtual world discrimination may synergize. △ Less

Submitted 31 January, 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.

Comments: 76 pages

MSC Class: 03F20; 68Q17; 68Q15; 03F30 ACM Class: F.2.2; F.4.1

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.

Journal ref: Nature Machine Intelligence, 1, 95-104 (2019)

A Comprehensive Approach for Learning-based Fully-Automated Inter-slice Motion Correction for Short-Axis Cine Cardiac MR Image Stacks

Authors: Giacomo Tarroni, Ozan Oktay, Matthew Sinclair, Wenjia Bai, Andreas Schuh, Hideaki Suzuki, Antonio de Marvao, Declan O'Regan, Stuart Cook, Daniel Rueckert

Abstract: In the clinical routine, short axis (SA) cine cardiac MR (CMR) image stacks are acquired during multiple subsequent breath-holds. If the patient cannot consistently hold the breath at the same position, the acquired image stack will be affected by inter-slice respiratory motion and will not correctly represent the cardiac volume, introducing potential errors in the following analyses and visualisa… ▽ More In the clinical routine, short axis (SA) cine cardiac MR (CMR) image stacks are acquired during multiple subsequent breath-holds. If the patient cannot consistently hold the breath at the same position, the acquired image stack will be affected by inter-slice respiratory motion and will not correctly represent the cardiac volume, introducing potential errors in the following analyses and visualisations. We propose an approach to automatically correct inter-slice respiratory motion in SA CMR image stacks. Our approach makes use of probabilistic segmentation maps (PSMs) of the left ventricular (LV) cavity generated with decision forests. PSMs are generated for each slice of the SA stack and rigidly registered in-plane to a target PSM. If long axis (LA) images are available, PSMs are generated for them and combined to create the target PSM; if not, the target PSM is produced from the same stack using a 3D model trained from motion-free stacks. The proposed approach was tested on a dataset of SA stacks acquired from 24 healthy subjects (for which anatomical 3D cardiac images were also available as reference) and compared to two techniques which use LA intensity images and LA segmentations as targets, respectively. The results show the accuracy and robustness of the proposed approach in motion compensation. △ Less

Submitted 3 October, 2018; originally announced October 2018.

Comments: Accepted for publication at MICCAI 2018. arXiv admin note: text overlap with arXiv:1803.09354

Learning Interpretable Anatomical Features Through Deep Generative Models: Application to Cardiac Remodeling

Authors: Carlo Biffi, Ozan Oktay, Giacomo Tarroni, Wenjia Bai, Antonio De Marvao, Georgia Doumou, Martin Rajchl, Reem Bedair, Sanjay Prasad, Stuart Cook, Declan O'Regan, Daniel Rueckert

Abstract: Alterations in the geometry and function of the heart define well-established causes of cardiovascular disease. However, current approaches to the diagnosis of cardiovascular diseases often rely on subjective human assessment as well as manual analysis of medical images. Both factors limit the sensitivity in quantifying complex structural and functional phenotypes. Deep learning approaches have re… ▽ More Alterations in the geometry and function of the heart define well-established causes of cardiovascular disease. However, current approaches to the diagnosis of cardiovascular diseases often rely on subjective human assessment as well as manual analysis of medical images. Both factors limit the sensitivity in quantifying complex structural and functional phenotypes. Deep learning approaches have recently achieved success for tasks such as classification or segmentation of medical images, but lack interpretability in the feature extraction and decision processes, limiting their value in clinical diagnosis. In this work, we propose a 3D convolutional generative model for automatic classification of images from patients with cardiac diseases associated with structural remodeling. The model leverages interpretable task-specific anatomic patterns learned from 3D segmentations. It further allows to visualise and quantify the learned pathology-specific remodeling patterns in the original input space of the images. This approach yields high accuracy in the categorization of healthy and hypertrophic cardiomyopathy subjects when tested on unseen MR images from our own multi-centre dataset (100%) as well on the ACDC MICCAI 2017 dataset (90%). We believe that the proposed deep learning approach is a promising step towards the development of interpretable classifiers for the medical imaging domain, which may help clinicians to improve diagnostic accuracy and enhance patient risk-stratification. △ Less

Submitted 18 July, 2018; originally announced July 2018.

Comments: Accepted at MICCAI 2018

Learning-Based Quality Control for Cardiac MR Images

Authors: Giacomo Tarroni, Ozan Oktay, Wenjia Bai, Andreas Schuh, Hideaki Suzuki, Jonathan Passerat-Palmbach, Antonio de Marvao, Declan P. O'Regan, Stuart Cook, Ben Glocker, Paul M. Matthews, Daniel Rueckert

Abstract: The effectiveness of a cardiovascular magnetic resonance (CMR) scan depends on the ability of the operator to correctly tune the acquisition parameters to the subject being scanned and on the potential occurrence of imaging artefacts such as cardiac and respiratory motion. In the clinical practice, a quality control step is performed by visual assessment of the acquired images: however, this proce… ▽ More The effectiveness of a cardiovascular magnetic resonance (CMR) scan depends on the ability of the operator to correctly tune the acquisition parameters to the subject being scanned and on the potential occurrence of imaging artefacts such as cardiac and respiratory motion. In the clinical practice, a quality control step is performed by visual assessment of the acquired images: however, this procedure is strongly operator-dependent, cumbersome and sometimes incompatible with the time constraints in clinical settings and large-scale studies. We propose a fast, fully-automated, learning-based quality control pipeline for CMR images, specifically for short-axis image stacks. Our pipeline performs three important quality checks: 1) heart coverage estimation, 2) inter-slice motion detection, 3) image contrast estimation in the cardiac region. The pipeline uses a hybrid decision forest method - integrating both regression and structured classification models - to extract landmarks as well as probabilistic segmentation maps from both long- and short-axis images as a basis to perform the quality checks. The technique was tested on up to 3000 cases from the UK Biobank as well as on 100 cases from the UK Digital Heart Project, and validated against manual annotations and visual inspections performed by expert interpreters. The results show the capability of the proposed pipeline to correctly detect incomplete or corrupted scans (e.g. on UK Biobank, sensitivity and specificity respectively 88% and 99% for heart coverage estimation, 85% and 95% for motion detection), allowing their exclusion from the analysed dataset or the triggering of a new acquisition. △ Less

Submitted 15 September, 2018; v1 submitted 25 March, 2018; originally announced March 2018.

Journal ref: IEEE Transactions on Medical Imaging Nov 2018

Anatomically Constrained Neural Networks (ACNN): Application to Cardiac Image Enhancement and Segmentation

Authors: Ozan Oktay, Enzo Ferrante, Konstantinos Kamnitsas, Mattias Heinrich, Wenjia Bai, Jose Caballero, Stuart Cook, Antonio de Marvao, Timothy Dawes, Declan O'Regan, Bernhard Kainz, Ben Glocker, Daniel Rueckert

Abstract: Incorporation of prior knowledge about organ shape and location is key to improve performance of image analysis approaches. In particular, priors can be useful in cases where images are corrupted and contain artefacts due to limitations in image acquisition. The highly constrained nature of anatomical objects can be well captured with learning based techniques. However, in most recent and promisin… ▽ More Incorporation of prior knowledge about organ shape and location is key to improve performance of image analysis approaches. In particular, priors can be useful in cases where images are corrupted and contain artefacts due to limitations in image acquisition. The highly constrained nature of anatomical objects can be well captured with learning based techniques. However, in most recent and promising techniques such as CNN based segmentation it is not obvious how to incorporate such prior knowledge. State-of-the-art methods operate as pixel-wise classifiers where the training objectives do not incorporate the structure and inter-dependencies of the output. To overcome this limitation, we propose a generic training strategy that incorporates anatomical prior knowledge into CNNs through a new regularisation model, which is trained end-to-end. The new framework encourages models to follow the global anatomical properties of the underlying anatomy (e.g. shape, label structure) via learned non-linear representations of the shape. We show that the proposed approach can be easily adapted to different analysis tasks (e.g. image enhancement, segmentation) and improve the prediction accuracy of the state-of-the-art models. The applicability of our approach is shown on multi-modal cardiac datasets and public benchmarks. Additionally, we demonstrate how the learned deep models of 3D shapes can be interpreted and used as biomarkers for classification of cardiac pathologies. △ Less

Submitted 5 December, 2017; v1 submitted 22 May, 2017; originally announced May 2017.

Comments: Published in IEEE Transactions on Medical Imaging (Aug 2017)

Defining UML Family Members Using Prefaces

Authors: Steve Cook, Anneke Kleppe, Richard Mitchell, Bernhard Rumpe, Jos Warmer, Alan Wills

Abstract: The Unified Modeling Language is extensible, and so can be regarded as a family of languages. Implicitly or explicitly, any particular UML model should be accompanied by a definition of the particular UML family member used for the model. The definition should cover syntactic and semantic issues. This paper proposes a mechanism for associating models with such definitions. Any particular definitio… ▽ More The Unified Modeling Language is extensible, and so can be regarded as a family of languages. Implicitly or explicitly, any particular UML model should be accompanied by a definition of the particular UML family member used for the model. The definition should cover syntactic and semantic issues. This paper proposes a mechanism for associating models with such definitions. Any particular definition would form what we call a preface. The name is intended to suggest that the definition of a particular UML family member must conceptually come before any model built using that family member. A preface would be large, and should be organised using packages. This would allow large amounts of sharing between different prefaces. The paper proposes that prefaces should have an axiomatic style of semantics, through not necessarily fully formal, and it offers a general approach to semantics that would reduce problems of inconsistency within a large preface, based on the idea of general cases and special cases △ Less

Submitted 24 September, 2014; originally announced September 2014.

Comments: 13 pages, 5 figures

Journal ref: Technology of Object-Oriented Languages and Systems, TOOLS'99 Pacific. IEEE Computer Society, 1999

The Amsterdam Manifesto on OCL

Authors: Steve Cook, Anneke Kleppe, Richard Mitchell, Bernhard Rumpe, Jos Warmer, Alan Wills

Abstract: In November 1998 the authors participated in a two-day workshop on the Object Constraint Language (OCL) in Amsterdam. The focus was to clarify issues about the semantics and the use of OCL, and to discuss useful and necessary extensions of OCL. Various topics have been raised and clarified. This manifesto contains the results of that workshop and the following work on these topics. Overview of OCL… ▽ More In November 1998 the authors participated in a two-day workshop on the Object Constraint Language (OCL) in Amsterdam. The focus was to clarify issues about the semantics and the use of OCL, and to discuss useful and necessary extensions of OCL. Various topics have been raised and clarified. This manifesto contains the results of that workshop and the following work on these topics. Overview of OCL. △ Less

Submitted 22 September, 2014; originally announced September 2014.

Comments: 35 pages, 4 figures

Journal ref: Object Modeling with the OCL, pp. 115-149 LNCS 2263, Springer Verlag, 2002

Complexity Theory for Operators in Analysis

Authors: Akitoshi Kawamura, Stephen Cook

Abstract: We propose an extension of the framework for discussing the computational complexity of problems involving uncountably many objects, such as real numbers, sets and functions, that can be represented only through approximation. The key idea is to use (a certain class of) string functions as names representing these objects. These are more expressive than infinite sequences, which served as names in… ▽ More We propose an extension of the framework for discussing the computational complexity of problems involving uncountably many objects, such as real numbers, sets and functions, that can be represented only through approximation. The key idea is to use (a certain class of) string functions as names representing these objects. These are more expressive than infinite sequences, which served as names in prior work that formulated complexity in more restricted settings. An advantage of using string functions is that we can define their "size" in the way inspired by higher-type complexity theory. This enables us to talk about computation on string functions whose time or space is bounded polynomially in the input size, giving rise to more general analogues of the classes P, NP, and PSPACE. We also define NP- and PSPACE-completeness under suitable many-one reductions. Because our framework separates machine computation and semantics, it can be applied to problems on sets of interest in analysis once we specify a suitable representation (encoding). As prototype applications, we consider the complexity of functions (operators) on real numbers, real sets, and real functions. For example, the task of numerical algorithms for solving a certain class of differential equations is naturally viewed as an operator taking real functions to real functions. As there was no complexity theory for operators, previous results only stated how complex the solution can be. We now reformulate them and show that the operator itself is polynomial-space complete. △ Less

Submitted 2 May, 2013; originally announced May 2013.

Comments: 22 pages, 9 figures; a few typos fixed after journal publication

MSC Class: 03D15; 65Y20; 68Q05; 68Q15 ACM Class: F.1.1; F.1.3

Journal ref: ACM Transactions on Computation Theory 4(2), Article 5, 2012

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.

Comments: continues the previous work of Cook, Le and Ye [arXiv:1106.4142]

Relativizing Small Complexity Classes and their Theories

Authors: Klaus Aehlig, Stephen Cook, Phuong Nguyen

Abstract: Existing definitions of the relativizations of \NCOne, Ł and \NL\ do not preserve the inclusions $\NCOne \subseteq Ł$, $\NL\subseteq \ACOne$. We start by giving the first definitions that preserve them. Here for Ł and \NL\ we define their relativizations using Wilson's stack oracle model, but limit the height of the stack to a constant (instead of $\log(n)$). We show that the collapse of any two c… ▽ More Existing definitions of the relativizations of \NCOne, Ł and \NL\ do not preserve the inclusions $\NCOne \subseteq Ł$, $\NL\subseteq \ACOne$. We start by giving the first definitions that preserve them. Here for Ł and \NL\ we define their relativizations using Wilson's stack oracle model, but limit the height of the stack to a constant (instead of $\log(n)$). We show that the collapse of any two classes in $\{\ACZm, \TCZ, \NCOne, Ł, \NL\}$ implies the collapse of their relativizations. Next we exhibit an oracle $α$ that makes $\ACk(α)$ a proper hierarchy. This strengthens and clarifies the separations of the relativized theories in [Takeuti, 1995]. The idea is that a circuit whose nested depth of oracle gates is bounded by $k$ cannot compute correctly the $(k+1)$ compositions of every oracle function. Finally we develop theories that characterize the relativizations of subclasses of \Ptime\ by modifying theories previously defined by the second two authors. A function is provably total in a theory iff it is in the corresponding relativized class, and hence the oracle separations imply separations for the relativized theories. △ Less

Submitted 24 April, 2012; originally announced April 2012.

Comments: 28 pages

Relativized Propositional Calculus

Authors: Stephen Cook

Abstract: Proof systems for the Relativized Propositional Calculus are defined and compared. Proof systems for the Relativized Propositional Calculus are defined and compared. △ Less

Submitted 9 March, 2012; originally announced March 2012.

Comments: 8 pages

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.

Comments: This version was substantially rewritten, where several proofs were rewritten and many typos and mistakes were fixed. A shorter version of this paper appeared in CSL 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.

ACM Class: F.2.2, F.4.1

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 3 (August 10, 2012) lmcs:973

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.

Comments: This is a revised journal version of the paper "Formal Theories for Linear Algebra" (Computer Science Logic) for the journal Logical Methods in Computer Science

ACM Class: F.4.0

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 1 (March 16, 2012) lmcs:716

Pebbles and Branching Programs for Tree Evaluation

Authors: Stephen Cook, Pierre McKenzie, Dustin Wehr, Mark Braverman, Rahul Santhanam

Abstract: We introduce the Tree Evaluation Problem, show that it is in logDCFL (and hence in P), and study its branching program complexity in the hope of eventually proving a superlogarithmic space lower bound. The input to the problem is a rooted, balanced d-ary tree of height h, whose internal nodes are labeled with d-ary functions on [k] = {1,...,k}, and whose leaves are labeled with elements of [k]. E… ▽ More We introduce the Tree Evaluation Problem, show that it is in logDCFL (and hence in P), and study its branching program complexity in the hope of eventually proving a superlogarithmic space lower bound. The input to the problem is a rooted, balanced d-ary tree of height h, whose internal nodes are labeled with d-ary functions on [k] = {1,...,k}, and whose leaves are labeled with elements of [k]. Each node obtains a value in [k] equal to its d-ary function applied to the values of its d children. The output is the value of the root. We show that the standard black pebbling algorithm applied to the binary tree of height h yields a deterministic k-way branching program with Theta(k^h) states solving this problem, and we prove that this upper bound is tight for h=2 and h=3. We introduce a simple semantic restriction called "thrifty" on k-way branching programs solving tree evaluation problems and show that the same state bound of Theta(k^h) is tight (up to a constant factor) for all h >= 2 for deterministic thrifty programs. We introduce fractional pebbling for trees and show that this yields nondeterministic thrifty programs with Theta(k^{h/2+1}) states solving the Boolean problem "determine whether the root has value 1". We prove that this bound is tight for h=2,3,4, and tight for unrestricted nondeterministic k-way branching programs for h=2,3. △ Less

Submitted 14 May, 2010; originally announced May 2010.

Comments: Journal version of mostly-previously-published work. 47 pages

The Complexity of Proving the Discrete Jordan Curve Theorem

Authors: Phuong Nguyen, Stephen Cook

Abstract: The Jordan Curve Theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded arithmetic that correspond to small complexity classes. The theory $V^0(2)$ (corresponding to $AC^0(2)$) proves that any set of edges that form disjoint cycle… ▽ More The Jordan Curve Theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded arithmetic that correspond to small complexity classes. The theory $V^0(2)$ (corresponding to $AC^0(2)$) proves that any set of edges that form disjoint cycles divides the grid into at least two regions. The theory $V^0$ (corresponding to $AC^0$) proves that any sequence of edges that form a simple closed curve divides the grid into exactly two regions. As a consequence, the Hex tautologies and the st-connectivity tautologies have polynomial size $AC^0(2)$-Frege-proofs, which improves results of Buss which only apply to the stronger proof system $TC^0$-Frege. △ Less

Submitted 15 February, 2010; originally announced February 2010.

Comments on Beckmann's Uniform Reducts

Authors: Stephen Cook

Abstract: Arnold Beckmann defined the uniform reduct of a propositional proof system f to be the set of those bounded arithmetical formulas whose propositional translations have polynomial size f-proofs. We prove that the uniform reduct of f + Extended Frege consists of all true bounded arithmetical formulas iff f + Extended Frege simulates every proof system. Arnold Beckmann defined the uniform reduct of a propositional proof system f to be the set of those bounded arithmetical formulas whose propositional translations have polynomial size f-proofs. We prove that the uniform reduct of f + Extended Frege consists of all true bounded arithmetical formulas iff f + Extended Frege simulates every proof system. △ Less

Submitted 23 January, 2006; v1 submitted 19 January, 2006; originally announced January 2006.

ACM Class: F.4.1

Computing over the Reals: Foundations for Scientific Computing

Authors: Mark Braverman, Stephen Cook

Abstract: We give a detailed treatment of the ``bit-model'' of computability and complexity of real functions and subsets of R^n, and argue that this is a good way to formalize many problems of scientific computation. In the introduction we also discuss the alternative Blum-Shub-Smale model. In the final section we discuss the issue of whether physical systems could defeat the Church-Turing Thesis. We give a detailed treatment of the ``bit-model'' of computability and complexity of real functions and subsets of R^n, and argue that this is a good way to formalize many problems of scientific computation. In the introduction we also discuss the alternative Blum-Shub-Smale model. In the final section we discuss the issue of whether physical systems could defeat the Church-Turing Thesis. △ Less

Submitted 14 September, 2005; originally announced September 2005.

ACM Class: F.1.1; G.0

Theories for TC0 and Other Small Complexity Classes

Authors: Phuong Nguyen, Stephen Cook

Abstract: We present a general method for introducing finitely axiomatizable "minimal" two-sorted theories for various subclasses of P (problems solvable in polynomial time). The two sorts are natural numbers and finite sets of natural numbers. The latter are essentially the finite binary strings, which provide a natural domain for defining the functions and sets in small complexity classes. We concentrat… ▽ More We present a general method for introducing finitely axiomatizable "minimal" two-sorted theories for various subclasses of P (problems solvable in polynomial time). The two sorts are natural numbers and finite sets of natural numbers. The latter are essentially the finite binary strings, which provide a natural domain for defining the functions and sets in small complexity classes. We concentrate on the complexity class TC^0, whose problems are defined by uniform polynomial-size families of bounded-depth Boolean circuits with majority gates. We present an elegant theory VTC^0 in which the provably-total functions are those associated with TC^0, and then prove that VTC^0 is "isomorphic" to a different-looking single-sorted theory introduced by Johannsen and Pollet. The most technical part of the isomorphism proof is defining binary number multiplication in terms a bit-counting function, and showing how to formalize the proofs of its algebraic properties. △ Less

Submitted 8 March, 2006; v1 submitted 5 May, 2005; originally announced May 2005.

Comments: 40 pages, Logical Methods in Computer Science

ACM Class: F.4.1

Journal ref: Logical Methods in Computer Science, Volume 2, Issue 1 (March 7, 2006) lmcs:2257

The strength of replacement in weak arithmetic

Authors: Stephen Cook, Neil Thapen

Abstract: The replacement (or collection or choice) axiom scheme asserts bounded quantifier exchange. We prove the independence of this scheme from various weak theories of arithmetic, sometimes under a complexity assumption. The replacement (or collection or choice) axiom scheme asserts bounded quantifier exchange. We prove the independence of this scheme from various weak theories of arithmetic, sometimes under a complexity assumption. △ Less

Submitted 8 September, 2004; originally announced September 2004.