-
Euclid Quick Data Release (Q1). Active galactic nuclei identification using diffusion-based inpainting of Euclid VIS images
Authors:
Euclid Collaboration,
G. Stevens,
S. Fotopoulou,
M. N. Bremer,
T. Matamoro Zatarain,
K. Jahnke,
B. Margalef-Bentabol,
M. Huertas-Company,
M. J. Smith,
M. Walmsley,
M. Salvato,
M. Mezcua,
A. Paulino-Afonso,
M. Siudek,
M. Talia,
F. Ricci,
W. Roster,
N. Aghanim,
B. Altieri,
S. Andreon,
H. Aussel,
C. Baccigalupi,
M. Baldi,
S. Bardelli,
P. Battaglia
, et al. (249 additional authors not shown)
Abstract:
Light emission from galaxies exhibit diverse brightness profiles, influenced by factors such as galaxy type, structural features and interactions with other galaxies. Elliptical galaxies feature more uniform light distributions, while spiral and irregular galaxies have complex, varied light profiles due to their structural heterogeneity and star-forming activity. In addition, galaxies with an acti…
▽ More
Light emission from galaxies exhibit diverse brightness profiles, influenced by factors such as galaxy type, structural features and interactions with other galaxies. Elliptical galaxies feature more uniform light distributions, while spiral and irregular galaxies have complex, varied light profiles due to their structural heterogeneity and star-forming activity. In addition, galaxies with an active galactic nucleus (AGN) feature intense, concentrated emission from gas accretion around supermassive black holes, superimposed on regular galactic light, while quasi-stellar objects (QSO) are the extreme case of the AGN emission dominating the galaxy. The challenge of identifying AGN and QSO has been discussed many times in the literature, often requiring multi-wavelength observations. This paper introduces a novel approach to identify AGN and QSO from a single image. Diffusion models have been recently developed in the machine-learning literature to generate realistic-looking images of everyday objects. Utilising the spatial resolving power of the Euclid VIS images, we created a diffusion model trained on one million sources, without using any source pre-selection or labels. The model learns to reconstruct light distributions of normal galaxies, since the population is dominated by them. We condition the prediction of the central light distribution by masking the central few pixels of each source and reconstruct the light according to the diffusion model. We further use this prediction to identify sources that deviate from this profile by examining the reconstruction error of the few central pixels regenerated in each source's core. Our approach, solely using VIS imaging, features high completeness compared to traditional methods of AGN and QSO selection, including optical, near-infrared, mid-infrared, and X-rays. [abridged]
△ Less
Submitted 19 March, 2025;
originally announced March 2025.
-
Monoidal Rips: Stable Multiparameter Filtrations of Directed Networks
Authors:
Nello Blaser,
Morten Brun,
Odin Hoff Gardaa,
Lars M. Salbu
Abstract:
We introduce the monoidal Rips filtration, a filtered simplicial set for weighted directed graphs and other lattice-valued networks. Our construction generalizes the Vietoris-Rips filtration for metric spaces by replacing the maximum operator, determining the filtration values, with a more general monoidal product. We establish interleaving guarantees for the monoidal Rips persistent homology, cap…
▽ More
We introduce the monoidal Rips filtration, a filtered simplicial set for weighted directed graphs and other lattice-valued networks. Our construction generalizes the Vietoris-Rips filtration for metric spaces by replacing the maximum operator, determining the filtration values, with a more general monoidal product. We establish interleaving guarantees for the monoidal Rips persistent homology, capturing existing stability results for real-valued networks. When the lattice is a product of totally ordered sets, we are in the setting of multiparameter persistence. Here, the interleaving distance is bounded in terms of a generalized network distance. We use this to prove a novel stability result for the sublevel Rips bifiltration. Our experimental results show that our method performs better than flagser in a graph regression task, and that combining different monoidal products in point cloud classification can improve performance.
△ Less
Submitted 18 March, 2025;
originally announced March 2025.
-
Multiparty Session Types with a Bang!
Authors:
Matthew Alan Le Brun,
Simon Fowler,
Ornela Dardha
Abstract:
Replication is an alternative construct to recursion for describing infinite behaviours in the pi-calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-passing programs. We introduce MPST!, a session-typed multiparty process calculus with replication and first-class roles. We show that repli…
▽ More
Replication is an alternative construct to recursion for describing infinite behaviours in the pi-calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-passing programs. We introduce MPST!, a session-typed multiparty process calculus with replication and first-class roles. We show that replication is not an equivalent alternative to recursion in MPST, and that using both replication and recursion in one type system in fact allows us to express both context-free protocols and protocols that support mutual exclusion and races. We demonstrate the expressiveness of MPST! on examples including binary tree serialisation, dining philosophers, and a model of an auction, and explore the implications of replication on the decidability of typechecking.
△ Less
Submitted 24 January, 2025;
originally announced January 2025.
-
HoloSpot: Intuitive Object Manipulation via Mixed Reality Drag-and-Drop
Authors:
Pablo Soler Garcia,
Petar Lukovic,
Lucie Reynaud,
Andrea Sgobbi,
Federica Bruni,
Martin Brun,
Marc Zünd,
Riccardo Bollati,
Marc Pollefeys,
Hermann Blum,
Zuria Bauer
Abstract:
Human-robot interaction through mixed reality (MR) technologies enables novel, intuitive interfaces to control robots in remote operations. Such interfaces facilitate operations in hazardous environments, where human presence is risky, yet human oversight remains crucial. Potential environments include disaster response scenarios and areas with high radiation or toxic chemicals. In this paper we p…
▽ More
Human-robot interaction through mixed reality (MR) technologies enables novel, intuitive interfaces to control robots in remote operations. Such interfaces facilitate operations in hazardous environments, where human presence is risky, yet human oversight remains crucial. Potential environments include disaster response scenarios and areas with high radiation or toxic chemicals. In this paper we present an interface system projecting a 3D representation of a scanned room as a scaled-down 'dollhouse' hologram, allowing users to select and manipulate objects using a straightforward drag-and-drop interface. We then translate these drag-and-drop user commands into real-time robot actions based on the recent Spot-Compose framework. The Unity-based application provides an interactive tutorial and a user-friendly experience, ensuring ease of use. Through comprehensive end-to-end testing, we validate the system's capability in executing pick-and-place tasks and a complementary user study affirms the interface's intuitive controls. Our findings highlight the advantages of this interface in improving user experience and operational efficiency. This work lays the groundwork for a robust framework that advances the potential for seamless human-robot collaboration in diverse applications. Paper website: https://holospot.github.io/
△ Less
Submitted 14 October, 2024;
originally announced October 2024.
-
Core Bifiltration
Authors:
Nello Blaser,
Morten Brun,
Odin Hoff Gardaa,
Lars M. Salbu
Abstract:
The motivation of this paper is to recognize a geometric shape from a noisy sample in the form of a point cloud. Inspired by the HDBSCAN clustering algorithm, we introduce the core dissimilarity, from which we construct the core bifiltration. We also consider the Delaunay core bifiltration by intersecting with Voronoi cells, giving us a filtered simplicial complex of smaller size. A major advantag…
▽ More
The motivation of this paper is to recognize a geometric shape from a noisy sample in the form of a point cloud. Inspired by the HDBSCAN clustering algorithm, we introduce the core dissimilarity, from which we construct the core bifiltration. We also consider the Delaunay core bifiltration by intersecting with Voronoi cells, giving us a filtered simplicial complex of smaller size. A major advantage of the (Delaunay) core bifiltration is that, for each filtration value, it admits a good cover of balls. By the persistent nerve theorem, the nerve of this cover is homotopy equivalent to the (Delaunay) core bifiltration. We show that the multicover-, core- and Delaunay core bifiltrations are all interleaved, and that they enjoy similar stability properties with respect to the Prohorov distance. We have performed experiments with the Delaunay core bifiltration. In the experiments, we calculated persistent homology along lines in the two-dimensional persistence parameter space, and computed multipersistence module approximations.
△ Less
Submitted 17 February, 2025; v1 submitted 2 May, 2024;
originally announced May 2024.
-
MAG$π$!: The Role of Replication in Typing Failure-Prone Communication
Authors:
Matthew Alan Le Brun,
Ornela Dardha
Abstract:
MAG$π$ is a Multiparty, Asynchronous and Generalised $π$-calculus that introduces timeouts into session types as a means of reasoning about failure-prone communication. Its type system guarantees that all possible message-loss is handled by timeout branches. In this work, we argue that the previous is unnecessarily strict. We present MAG$π$!, an extension serving as the first introduction of repli…
▽ More
MAG$π$ is a Multiparty, Asynchronous and Generalised $π$-calculus that introduces timeouts into session types as a means of reasoning about failure-prone communication. Its type system guarantees that all possible message-loss is handled by timeout branches. In this work, we argue that the previous is unnecessarily strict. We present MAG$π$!, an extension serving as the first introduction of replication into Multiparty Session Types (MPST). Replication is a standard $π$-calculus construct used to model infinitely available servers. We lift this construct to type-level, and show that it simplifies specification of distributed client-server interactions. We prove properties relevant to generalised MPST: subject reduction, session fidelity and process property verification.
△ Less
Submitted 24 April, 2024;
originally announced April 2024.
-
Verus: Verifying Rust Programs using Linear Ghost Types (extended version)
Authors:
Andrea Lattuada,
Travis Hance,
Chanhee Cho,
Matthias Brun,
Isitha Subasinghe,
Yi Zhou,
Jon Howell,
Bryan Parno,
Chris Hawblitzel
Abstract:
The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such systems, formal verification can be useful to prove functional correctness properties beyond type safety. This paper presents Verus, an SMT-based tool…
▽ More
The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such systems, formal verification can be useful to prove functional correctness properties beyond type safety. This paper presents Verus, an SMT-based tool for formally verifying Rust programs. With Verus, programmers express proofs and specifications using the Rust language, allowing proofs to take advantage of Rust's linear types and borrow checking. We show how this allows proofs to manipulate linearly typed permissions that let Rust code safely manipulate memory, pointers, and concurrent resources. Verus organizes proofs and specifications using a novel mode system that distinguishes specifications, which are not checked for linearity and borrowing, from executable code and proofs, which are checked for linearity and borrowing. We formalize Verus' linearity, borrowing, and modes in a small lambda calculus, for which we prove type safety and termination of specifications and proofs. We demonstrate Verus on a series of examples, including pointer-manipulating code (an xor-based doubly linked list), code with interior mutability, and concurrent code.
△ Less
Submitted 10 March, 2023; v1 submitted 9 March, 2023;
originally announced March 2023.
-
MAG$π$: Types for Failure-Prone Communication
Authors:
Matthew Alan Le Brun,
Ornela Dardha
Abstract:
Multiparty Session Types (MPST) are a typing discipline for communication-centric systems, guaranteeing communication safety, deadlock freedom and protocol compliance. Several works have emerged which model failures and introduce fault-tolerance techniques. However, such works often make assumptions on the underlying network, e.g., TCP-based communication where messages are guaranteed to be delive…
▽ More
Multiparty Session Types (MPST) are a typing discipline for communication-centric systems, guaranteeing communication safety, deadlock freedom and protocol compliance. Several works have emerged which model failures and introduce fault-tolerance techniques. However, such works often make assumptions on the underlying network, e.g., TCP-based communication where messages are guaranteed to be delivered; or adopt centralised reliable nodes and an ad-hoc notion of reliability; or only address a single kind of failure, such as node crash failures. In this work, we develop MAG$π$ -- a Multiparty, Asynchronous and Generalised $π$-calculus, which is the first language and type system to accommodate in unison: (i) the widest range of non-Byzantine faults, including message loss, delays and reordering; crash failures and link failures; and network partitioning; (ii) a novel and most general notion of reliability, taking into account the viewpoint of each participant in the protocol; (iii) a spectrum of network assumptions from the lowest UDP-based network programming to the TCP-based application level. We prove subject reduction and session fidelity; process properties (deadlock freedom, termination, etc.); failure-handling safety and reliability adherence.
△ Less
Submitted 25 January, 2023;
originally announced January 2023.
-
The Parameterized Complexity of Finding Minimum Bounded Chains
Authors:
Nello Blaser,
Morten Brun,
Lars M. Salbu,
Erlend Raa Vågset
Abstract:
Finding the smallest $d$-chain with a specific $(d-1)$-boundary in a simplicial complex is known as the \textsc{Minimum Bounded Chain} (MBC$_d$) problem. The MBC$_d$ problem is NP-hard for all $d\geq 2$. In this paper, we prove that it is also W[1]-hard for all $d\geq 2$, if we parameterize the problem by solution size. We also give an algorithm solving the MBC$_1$ problem in polynomial time and i…
▽ More
Finding the smallest $d$-chain with a specific $(d-1)$-boundary in a simplicial complex is known as the \textsc{Minimum Bounded Chain} (MBC$_d$) problem. The MBC$_d$ problem is NP-hard for all $d\geq 2$. In this paper, we prove that it is also W[1]-hard for all $d\geq 2$, if we parameterize the problem by solution size. We also give an algorithm solving the MBC$_1$ problem in polynomial time and introduce and implemented two fixed parameter tractable (FPT) algorithms solving the MBC$_d$ problem for all $d$. The first algorithm is a generalized version of Dijkstra's algorithm and is parameterized by solution size and coface degree. The second algorithm is a dynamic programming approach based on treewidth, which has the same runtime as a lower bound we prove under the exponential time hypothesis.
△ Less
Submitted 12 August, 2021; v1 submitted 10 August, 2021;
originally announced August 2021.
-
A Comparison of the Delta Method and the Bootstrap in Deep Learning Classification
Authors:
Geir K. Nilsen,
Antonella Z. Munthe-Kaas,
Hans J. Skaug,
Morten Brun
Abstract:
We validate the recently introduced deep learning classification adapted Delta method by a comparison with the classical Bootstrap. We show that there is a strong linear relationship between the quantified predictive epistemic uncertainty levels obtained from the two methods when applied on two LeNet-based neural network classifiers using the MNIST and CIFAR-10 datasets. Furthermore, we demonstrat…
▽ More
We validate the recently introduced deep learning classification adapted Delta method by a comparison with the classical Bootstrap. We show that there is a strong linear relationship between the quantified predictive epistemic uncertainty levels obtained from the two methods when applied on two LeNet-based neural network classifiers using the MNIST and CIFAR-10 datasets. Furthermore, we demonstrate that the Delta method offers a five times computation time reduction compared to the Bootstrap.
△ Less
Submitted 4 July, 2021;
originally announced July 2021.
-
Epistemic Uncertainty Quantification in Deep Learning Classification by the Delta Method
Authors:
Geir K. Nilsen,
Antonella Z. Munthe-Kaas,
Hans J. Skaug,
Morten Brun
Abstract:
The Delta method is a classical procedure for quantifying epistemic uncertainty in statistical models, but its direct application to deep neural networks is prevented by the large number of parameters $P$. We propose a low cost variant of the Delta method applicable to $L_2$-regularized deep neural networks based on the top $K$ eigenpairs of the Fisher information matrix. We address efficient comp…
▽ More
The Delta method is a classical procedure for quantifying epistemic uncertainty in statistical models, but its direct application to deep neural networks is prevented by the large number of parameters $P$. We propose a low cost variant of the Delta method applicable to $L_2$-regularized deep neural networks based on the top $K$ eigenpairs of the Fisher information matrix. We address efficient computation of full-rank approximate eigendecompositions in terms of either the exact inverse Hessian, the inverse outer-products of gradients approximation or the so-called Sandwich estimator. Moreover, we provide a bound on the approximation error for the uncertainty of the predictive class probabilities. We observe that when the smallest eigenvalue of the Fisher information matrix is near the $L_2$-regularization rate, the approximation error is close to zero even when $K\ll P$. A demonstration of the methodology is presented using a TensorFlow implementation, and we show that meaningful rankings of images based on predictive uncertainty can be obtained for two LeNet-based neural networks using the MNIST and CIFAR-10 datasets. Further, we observe that false positives have on average a higher predictive epistemic uncertainty than true positives. This suggests that there is supplementing information in the uncertainty measure not captured by the classification alone.
△ Less
Submitted 28 February, 2021; v1 submitted 2 December, 2019;
originally announced December 2019.
-
Efficient Computation of Hessian Matrices in TensorFlow
Authors:
Geir K. Nilsen,
Antonella Z. Munthe-Kaas,
Hans J. Skaug,
Morten Brun
Abstract:
The Hessian matrix has a number of important applications in a variety of different fields, such as optimzation, image processing and statistics. In this paper we focus on the practical aspects of efficiently computing Hessian matrices in the context of deep learning using the Python scripting language and the TensorFlow library. We define a general feed-forward neural network model and show how t…
▽ More
The Hessian matrix has a number of important applications in a variety of different fields, such as optimzation, image processing and statistics. In this paper we focus on the practical aspects of efficiently computing Hessian matrices in the context of deep learning using the Python scripting language and the TensorFlow library. We define a general feed-forward neural network model and show how to efficiently compute two quantities: the cost function's exact Hessian matrix, and the cost function's approximate Hessian matrix, known as the Outer Product of Gradients (OPG) matrix. Furthermore, as the number of parameters (weights and biases) in deep learning usually is very large, we show how to reduce the quadratic space complexity by an efficient implementation based on approximate eigendecompositions.
△ Less
Submitted 7 April, 2021; v1 submitted 14 May, 2019;
originally announced May 2019.
-
Contribution à la modélisation explicite des plates-formes d'exécution pour l'IDM
Authors:
Frédéric Thomas,
Jérôme Delatour,
François Terrier,
Matthias Brun,
Sébastien Gérard
Abstract:
One foundation of the model driven engineering (MDE) is to separate the modelling application description from its technological implementation (i.e. platform). Some of them are dedicated to the system execution. Hence, one promise solution of the MDE is to automate transformations from platform independent models to platform specific models. Little work has explicitly described platform character…
▽ More
One foundation of the model driven engineering (MDE) is to separate the modelling application description from its technological implementation (i.e. platform). Some of them are dedicated to the system execution. Hence, one promise solution of the MDE is to automate transformations from platform independent models to platform specific models. Little work has explicitly described platform characteristics. Yet, an explicit modelling allows taking in account their characteristics more easily (par ex., performances, maintainability,portability). This paper presents both an execution platform modelling state of art and a pattern to describe execution platform modelling framework. It intends to confirm the feasibility and the interests in describing an execution platform metamodel.
△ Less
Submitted 24 July, 2014;
originally announced July 2014.
