-
Multi-Scale and Multimodal Species Distribution Modeling
Authors:
Nina van Tiel,
Robin Zbinden,
Emanuele Dalsasso,
Benjamin Kellenberger,
Loïc Pellissier,
Devis Tuia
Abstract:
Species distribution models (SDMs) aim to predict the distribution of species by relating occurrence data with environmental variables. Recent applications of deep learning to SDMs have enabled new avenues, specifically the inclusion of spatial data (environmental rasters, satellite images) as model predictors, allowing the model to consider the spatial context around each species' observations. H…
▽ More
Species distribution models (SDMs) aim to predict the distribution of species by relating occurrence data with environmental variables. Recent applications of deep learning to SDMs have enabled new avenues, specifically the inclusion of spatial data (environmental rasters, satellite images) as model predictors, allowing the model to consider the spatial context around each species' observations. However, the appropriate spatial extent of the images is not straightforward to determine and may affect the performance of the model, as scale is recognized as an important factor in SDMs. We develop a modular structure for SDMs that allows us to test the effect of scale in both single- and multi-scale settings. Furthermore, our model enables different scales to be considered for different modalities, using a late fusion approach. Results on the GeoLifeCLEF 2023 benchmark indicate that considering multimodal data and learning multi-scale representations leads to more accurate models.
△ Less
Submitted 6 November, 2024;
originally announced November 2024.
-
The exponential logic of sequentialization
Authors:
Aurore Alcolei,
Luc Pellissier,
Alexis Saurin
Abstract:
Linear logic has provided new perspectives on proof-theory, denotational semantics and the study of programming languages. One of its main successes are proof-nets, canonical representations of proofs that lie at the intersection between logic and graph theory. In the case of the minimalist proof-system of multiplicative linear logic without units (MLL), these two aspects are completely fused: pro…
▽ More
Linear logic has provided new perspectives on proof-theory, denotational semantics and the study of programming languages. One of its main successes are proof-nets, canonical representations of proofs that lie at the intersection between logic and graph theory. In the case of the minimalist proof-system of multiplicative linear logic without units (MLL), these two aspects are completely fused: proof-nets for this system are graphs satisfying a correctness criterion that can be fully expressed in the language of graphs.
For more expressive logical systems (containing logical constants, quantifiers and exponential modalities), this is not completely the case. The purely graphical approach of proof-nets deprives them of any sequential structure that is crucial to represent the order in which arguments are presented, which is necessary for these extensions. Rebuilding this order of presentation - sequentializing the graph - is thus a requirement for a graph to be logical. Presentations and study of the artifacts ensuring that sequentialization can be done, such as boxes or jumps, are an integral part of researches on linear logic.
Jumps, extensively studied by Faggian and di Giamberardino, can express intermediate degrees of sequentialization between a sequent calculus proof and a fully desequentialized proof-net. We propose to analyze the logical strength of jumps by internalizing them in an extention of MLL where axioms on a specific formula, the jumping formula, introduce constrains on the possible sequentializations. The jumping formula needs to be treated non-linearly, which we do either axiomatically, or by embedding it in a very controlled fragment of multiplicative-exponential linear logic, uncovering the exponential logic of sequentialization.
△ Less
Submitted 17 November, 2023; v1 submitted 13 October, 2023;
originally announced October 2023.
-
Deep learning approximations for non-local nonlinear PDEs with Neumann boundary conditions
Authors:
Victor Boussange,
Sebastian Becker,
Arnulf Jentzen,
Benno Kuckuck,
Loïc Pellissier
Abstract:
Nonlinear partial differential equations (PDEs) are used to model dynamical processes in a large number of scientific fields, ranging from finance to biology. In many applications standard local models are not sufficient to accurately account for certain non-local phenomena such as, e.g., interactions at a distance. In order to properly capture these phenomena non-local nonlinear PDE models are fr…
▽ More
Nonlinear partial differential equations (PDEs) are used to model dynamical processes in a large number of scientific fields, ranging from finance to biology. In many applications standard local models are not sufficient to accurately account for certain non-local phenomena such as, e.g., interactions at a distance. In order to properly capture these phenomena non-local nonlinear PDE models are frequently employed in the literature. In this article we propose two numerical methods based on machine learning and on Picard iterations, respectively, to approximately solve non-local nonlinear PDEs. The proposed machine learning-based method is an extended variant of a deep learning-based splitting-up type approximation method previously introduced in the literature and utilizes neural networks to provide approximate solutions on a subset of the spatial domain of the solution. The Picard iterations-based method is an extended variant of the so-called full history recursive multilevel Picard approximation scheme previously introduced in the literature and provides an approximate solution for a single point of the domain. Both methods are mesh-free and allow non-local nonlinear PDEs with Neumann boundary conditions to be solved in high dimensions. In the two methods, the numerical difficulties arising due to the dimensionality of the PDEs are avoided by (i) using the correspondence between the expected trajectory of reflected stochastic processes and the solution of PDEs (given by the Feynman-Kac formula) and by (ii) using a plain vanilla Monte Carlo integration to handle the non-local term. We evaluate the performance of the two methods on five different PDEs arising in physics and biology. In all cases, the methods yield good results in up to 10 dimensions with short run times. Our work extends recently developed methods to overcome the curse of dimensionality in solving PDEs.
△ Less
Submitted 7 May, 2022;
originally announced May 2022.
-
Gluing resource proof-structures: inhabitation and inverting the Taylor expansion
Authors:
Giulio Guerrieri,
Luc Pellissier,
Lorenzo Tortora de Falco
Abstract:
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing (and deciding in the finite case) those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-stru…
▽ More
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing (and deciding in the finite case) those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures. We also prove semi-decidability of the type inhabitation problem for cut-free MELL proof-structures.
△ Less
Submitted 21 April, 2022; v1 submitted 6 August, 2020;
originally announced August 2020.
-
Lower bounds for algebraic machines, semantically
Authors:
Luc Pellissier,
Thomas Seiller
Abstract:
This paper presents a new semantic method for proving lower bounds in computational complexity. We use it to prove that maxflow, a PTIME complete problem, is not computable in polylogarithmic time on parallel random access machines (PRAMs) working with integers, showing that NCZ \neq PTIME, where NCZ is the complexity class defined by such machines, and PTIME is the standard class of polynomial ti…
▽ More
This paper presents a new semantic method for proving lower bounds in computational complexity. We use it to prove that maxflow, a PTIME complete problem, is not computable in polylogarithmic time on parallel random access machines (PRAMs) working with integers, showing that NCZ \neq PTIME, where NCZ is the complexity class defined by such machines, and PTIME is the standard class of polynomial time computable problems (on, say, a Turing machine). On top of showing this new separation result, we show our method captures previous lower bounds results from the literature: Steele and Yao's lower bounds for algebraic decision trees, Ben-Or's lower bounds for algebraic computation trees, Cucker's proof that NC is not equal to PTIME on the reals, and Mulmuley's lower bounds for "PRAMs without bit operations".
△ Less
Submitted 4 February, 2021; v1 submitted 24 February, 2020;
originally announced February 2020.
-
Glueability of resource proof-structures: inverting the Taylor expansion (long version)
Authors:
Giulio Guerrieri,
Luc Pellissier,
Lorenzo Tortora de Falco
Abstract:
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures.
A Multiplicative-Exponential Linear Logic (MELL) proof-structure can be expanded into a set of resource proof-structures: its Taylor expansion. We introduce a new criterion characterizing those sets of resource proof-structures that are part of the Taylor expansion of some MELL proof-structure, through a rewriting system acting both on resource and MELL proof-structures.
△ Less
Submitted 17 October, 2019;
originally announced October 2019.
-
Unifying lower bounds for algebraic machines, semantically
Authors:
Thomas Seiller,
Luc Pellissier,
Ulysse Léchine
Abstract:
This paper presents a new abstract method for proving lower bounds in computational complexity. Based on the notion of topological and measurable entropy for dynamical systems, it is shown to generalise three previous lower bounds results from the literature in algebraic complexity. We use it to prove that maxflow, a Ptime complete problem, is not computable in polylogarithmic time on parallel ran…
▽ More
This paper presents a new abstract method for proving lower bounds in computational complexity. Based on the notion of topological and measurable entropy for dynamical systems, it is shown to generalise three previous lower bounds results from the literature in algebraic complexity. We use it to prove that maxflow, a Ptime complete problem, is not computable in polylogarithmic time on parallel random access machines (prams) working with real numbers. This improves, albeit slightly, on a result of Mulmuley since the class of machines considered extends the class "prams without bit operations", making more precise the relationship between Mulmuley's result and similar lower bounds on real prams.
More importantly, we show our method captures previous lower bounds results from the literature, thus providing a unifying framework for "topological" proofs of lower bounds: Steele and Yao's lower bounds for algebraic decision trees, Ben-Or's lower bounds for algebraic computation trees, Cucker's proof that NC is not equal to Ptime in the real case, and Mulmuley's lower bounds for "prams without bit operations".
△ Less
Submitted 17 October, 2024; v1 submitted 16 November, 2018;
originally announced November 2018.
-
Relational type-checking for MELL proof-structures. Part 1: Multiplicatives
Authors:
Giulio Guerrieri,
Luc Pellissier,
Lorenzo Tortora de Falco
Abstract:
Relational semantics for linear logic is a form of non-idempotent intersection type system, from which several informations on the execution of a proof-structure can be recovered. An element of the relational interpretation of a proof-structure R with conclusion $Γ$ acts thus as a type (refining $Γ$) having R as an inhabitant. We are interested in the following type-checking question: given a proo…
▽ More
Relational semantics for linear logic is a form of non-idempotent intersection type system, from which several informations on the execution of a proof-structure can be recovered. An element of the relational interpretation of a proof-structure R with conclusion $Γ$ acts thus as a type (refining $Γ$) having R as an inhabitant. We are interested in the following type-checking question: given a proof-structure R, a list of formulae $Γ$, and a point x in the relational interpretation of $Γ$, is x in the interpretation of R? This question is decidable. We present here an algorithm that decides it in time linear in the size of R, if R is a proof-structure in the multiplicative fragment of linear logic. This algorithm can be extended to larger fragments of multiplicative-exponential linear logic containing $λ$-calculus.
△ Less
Submitted 1 June, 2016;
originally announced June 2016.
