-
Semantically-aware Neural Radiance Fields for Visual Scene Understanding: A Comprehensive Review
Authors:
Thang-Anh-Quan Nguyen,
Amine Bourki,
Mátyás Macudzinski,
Anthony Brunel,
Mohammed Bennamoun
Abstract:
This review thoroughly examines the role of semantically-aware Neural Radiance Fields (NeRFs) in visual scene understanding, covering an analysis of over 250 scholarly papers. It explores how NeRFs adeptly infer 3D representations for both stationary and dynamic objects in a scene. This capability is pivotal for generating high-quality new viewpoints, completing missing scene details (inpainting),…
▽ More
This review thoroughly examines the role of semantically-aware Neural Radiance Fields (NeRFs) in visual scene understanding, covering an analysis of over 250 scholarly papers. It explores how NeRFs adeptly infer 3D representations for both stationary and dynamic objects in a scene. This capability is pivotal for generating high-quality new viewpoints, completing missing scene details (inpainting), conducting comprehensive scene segmentation (panoptic segmentation), predicting 3D bounding boxes, editing 3D scenes, and extracting object-centric 3D models. A significant aspect of this study is the application of semantic labels as viewpoint-invariant functions, which effectively map spatial coordinates to a spectrum of semantic labels, thus facilitating the recognition of distinct objects within the scene. Overall, this survey highlights the progression and diverse applications of semantically-aware neural radiance fields in the context of visual scene interpretation.
△ Less
Submitted 16 February, 2024;
originally announced February 2024.
-
Backpropagation in the Simply Typed Lambda-calculus with Linear Negation
Authors:
Alois Brunel,
Damiano Mazza,
Michele Pagani
Abstract:
Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for efficiently training (deep) neural networks. Recent years have witnessed the quick growth of a research field…
▽ More
Backpropagation is a classic automatic differentiation algorithm computing the gradient of functions specified by a certain class of simple, first-order programs, called computational graphs. It is a fundamental tool in several fields, most notably machine learning, where it is the key for efficiently training (deep) neural networks. Recent years have witnessed the quick growth of a research field called differentiable programming, the aim of which is to express computational graphs more synthetically and modularly by resorting to actual programming languages endowed with control flow operators and higher-order combinators, such as map and fold. In this paper, we extend the backpropagation algorithm to a paradigmatic example of such a programming language: we define a compositional program transformation from the simply-typed lambda-calculus to itself augmented with a notion of linear negation, and prove that this computes the gradient of the source program with the same efficiency as first-order backpropagation. The transformation is completely effect-free and thus provides a purely logical understanding of the dynamics of backpropagation.
△ Less
Submitted 6 November, 2019; v1 submitted 27 September, 2019;
originally announced September 2019.
-
A CNN adapted to time series for the classification of Supernovae
Authors:
Anthony Brunel,
Johanna Pasquet,
Jérôme Pasquet,
Nancy Rodriguez,
Frédéric Comby,
Dominique Fouchez,
Marc Chaumont
Abstract:
Cosmologists are facing the problem of the analysis of a huge quantity of data when observing the sky. The methods used in cosmology are, for the most of them, relying on astrophysical models, and thus, for the classification, they usually use a machine learning approach in two-steps, which consists in, first, extracting features, and second, using a classifier. In this paper, we are specifically…
▽ More
Cosmologists are facing the problem of the analysis of a huge quantity of data when observing the sky. The methods used in cosmology are, for the most of them, relying on astrophysical models, and thus, for the classification, they usually use a machine learning approach in two-steps, which consists in, first, extracting features, and second, using a classifier. In this paper, we are specifically studying the supernovae phenomenon and especially the binary classification "I.a supernovae versus not-I.a supernovae". We present two Convolutional Neural Networks (CNNs) defeating the current state-of-the-art. The first one is adapted to time series and thus to the treatment of supernovae light-curves. The second one is based on a Siamese CNN and is suited to the nature of data, i.e. their sparsity and their weak quantity (small learning database).
△ Less
Submitted 2 January, 2019;
originally announced January 2019.
-
Indexed realizability for bounded-time programming with references and type fixpoints
Authors:
Aloïs Brunel,
Antoine Madet
Abstract:
The field of implicit complexity has recently produced several bounded-complexity programming languages. This kind of language allows to implement exactly the functions belonging to a certain complexity class. We here present a realizability semantics for a higher-order functional language based on a fragment of linear logic called LAL which characterizes the complexity class PTIME. This language…
▽ More
The field of implicit complexity has recently produced several bounded-complexity programming languages. This kind of language allows to implement exactly the functions belonging to a certain complexity class. We here present a realizability semantics for a higher-order functional language based on a fragment of linear logic called LAL which characterizes the complexity class PTIME. This language features recursive types and higher-order store. Our realizability is based on biorthogonality, step-indexing and is moreover quantitative. This last feature enables us not only to derive a semantical proof of termination, but also to give bounds on the number of computational steps needed by typed programs to terminate.
△ Less
Submitted 21 June, 2012;
originally announced June 2012.
-
Quantitative classical realizability
Authors:
Aloïs Brunel
Abstract:
Introduced by Dal Lago and Hofmann, quantitative realizability is a technique used to define models for logics based on Multiplicative Linear Logic. A particularity is that functions are interpreted as bounded time computable functions. It has been used to give new and uniform proofs of soundness of several type systems with respect to certain time complexity classes. We propose a reformulation of…
▽ More
Introduced by Dal Lago and Hofmann, quantitative realizability is a technique used to define models for logics based on Multiplicative Linear Logic. A particularity is that functions are interpreted as bounded time computable functions. It has been used to give new and uniform proofs of soundness of several type systems with respect to certain time complexity classes. We propose a reformulation of their ideas in the setting of Krivine's classical realizability. The framework obtained generalizes Dal Lago and Hofmann's realizability, and reveals deep connections between quantitative realizability and a linear variant of Cohen's forcing.
△ Less
Submitted 19 November, 2012; v1 submitted 20 January, 2012;
originally announced January 2012.
-
Church => Scott = Ptime: an application of resource sensitive realizability
Authors:
Aloïs Brunel,
Kazushige Terui
Abstract:
We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed by a standard non-linear type `Church,' while the Scott encodings (purely linear representations of words) are by a linear type `Scott.' We give a characterization of polynomial time functions, which is derived from (…
▽ More
We introduce a variant of linear logic with second order quantifiers and type fixpoints, both restricted to purely linear formulas. The Church encodings of binary words are typed by a standard non-linear type `Church,' while the Scott encodings (purely linear representations of words) are by a linear type `Scott.' We give a characterization of polynomial time functions, which is derived from (Leivant and Marion 93): a function is computable in polynomial time if and only if it can be represented by a term of type Church => Scott.
To prove soundness, we employ a resource sensitive realizability technique developed by Hofmann and Dal Lago.
△ Less
Submitted 4 May, 2010;
originally announced May 2010.
