arXiv subjects

Marco Volpe

Publications and source records attributed to Marco Volpe.

15 recordsLinked to original sources

arXiv2026

Homology manifolds via six functor formalisms

We study homology manifolds through the eyes of the six functor formalism of spectral sheaves on locally compact Hausdorff spaces. As main results, we characterize cohomologically smooth objects by adapting an argument of Scholze, deduce that any hypercomplete locally compact ANR homology manifold is cohomologically smooth, show that compact ANR homology manifolds $X$ are Poincar\'e duality complexes whose Spivak tangent fibration identifies with the dualizing sheaf of $X$, and prove a generalization of Wilder's monotone mapping theorem about cell-like maps. Moreover, we introduce the notion of homotopy manifolds for which we prove an unstable analog of Wilder's orientability conjecture and show that hypercomplete ANR homology manifolds are homotopy manifolds. As a consequence, we show that for a compact $d$-dimensional ANR homology manifold, the Spivak tangent fibration of its associated Poincar\'e duality complex canonically destabilizes to a pointed $S^d$-fibration. Finally, we introduce homotopy manifolds with conical singularities, a generalization of Cohen's triangulated homotopy manifolds, and show that such objects are in fact topological manifolds, generalizing a result of Siebenmann. Along the way, we obtain comparisons between sheaf and singular cohomology and between the shape and the weak homotopy type of a topological space, explore the relation between various notions of cohomological dimension and hypercompleteness, and study six functor formalisms satisfying the K\"unneth formula.

math.AT↗

arXiv2026

A characterization of sheaves among six functor formalisms on $\mathrm{LCH}$

Let $\mathcal{C}$ be any stable presentably symmetric monoidal $\infty$-category. In this paper, we characterize $\mathrm{Shv}(-,\mathcal{C})$ on locally compact Hausdorff spaces as the unique six functor formalism satisfying a list of very natural properties. As a consequence, we deduce that every continuous six functor formalism $D$ in the sense of Zhu is equivalent to $\mathrm{Shv}(-, D(\mathrm{pt}))$.

math.AT↗

arXiv2025

Approximate Fibrations in Higher Topos Theory

The goal of this paper is to put the theory of approximate fibrations into the framework of higher topos theory. We define the notion of an approximate fibration for a general geometric morphism of $\infty$-topoi, give several characterizations in terms of shape theory and compare it to the original definition for maps of topological spaces of Coram and Duvall. Furthermore, we revisit the notion of cell-like maps between topoi, and generalize Lurie's shape-theoretic characterization by giving a purely topos-theoretical proof.

math.GT↗

arXiv2024

Finiteness and finite domination in stratified homotopy theory

In this paper, we study compactness and finiteness of an $\infty$-category $\mathcal{C}$ equipped with a conservative functor to a finite poset $P$. We provide sufficient conditions for $\mathcal{C}$ to be compact in terms of strata and homotopy links of $\mathcal{C}\rightarrow P$. Analogous conditions for $\mathcal{C}$ to be finite are also given. From these, we deduce that, if $X\rightarrow P$ is a conically stratified space with the property that the weak homotopy type of its strata, and of strata of its local links, are compact (respectively finite) $\infty$-groupoids, then $\text{Exit}_P(X)$ is compact (respectively finite). This gives a positive answer to a question of Porta and Teyssier. If $X\rightarrow P$ is equipped with a conically smooth structure (e.g. a Whitney stratification), we show that $\text{Exit}_P(X)$ is finite if and only the weak homotopy types of the strata of $X\rightarrow P$ are finite. The aforementioned characterization relies on the finiteness of $\text{Exit}_P(X)$, when $X\rightarrow P$ is compact and conically smooth. We conclude our paper by showing that the analogous statement does not hold in the topological category. More explicitly, we provide an example of a compact $C^0$-stratified space whose exit paths $\infty$-category is compact, but not finite. This stratified space was constructed by Quinn. We also observe that this provides a non-trivial example of a $C^0$-stratified space which does not admit any conically smooth structure.

math.AT↗

arXiv2024

Are Frontier Large Language Models Suitable for Q&A in Science Centres?

This paper investigates the suitability of frontier Large Language Models (LLMs) for Q&A interactions in science centres, with the aim of boosting visitor engagement while maintaining factual accuracy. Using a dataset of questions collected from the National Space Centre in Leicester (UK), we evaluated responses generated by three leading models: OpenAI's GPT-4, Claude 3.5 Sonnet, and Google Gemini 1.5. Each model was prompted for both standard and creative responses tailored to an 8-year-old audience, and these responses were assessed by space science experts based on accuracy, engagement, clarity, novelty, and deviation from expected answers. The results revealed a trade-off between creativity and accuracy, with Claude outperforming GPT and Gemini in both maintaining clarity and engaging young audiences, even when asked to generate more creative responses. Nonetheless, experts observed that higher novelty was generally associated with reduced factual reliability across all models. This study highlights the potential of LLMs in educational settings, emphasizing the need for careful prompt engineering to balance engagement with scientific rigor.

cs.AI↗

arXiv2024

Do LLMs Agree on the Creativity Evaluation of Alternative Uses?

This paper investigates whether large language models (LLMs) show agreement in assessing creativity in responses to the Alternative Uses Test (AUT). While LLMs are increasingly used to evaluate creative content, previous studies have primarily focused on a single model assessing responses generated by the same model or humans. This paper explores whether LLMs can impartially and accurately evaluate creativity in outputs generated by both themselves and other models. Using an oracle benchmark set of AUT responses, categorized by creativity level (common, creative, and highly creative), we experiment with four state-of-the-art LLMs evaluating these outputs. We test both scoring and ranking methods and employ two evaluation settings (comprehensive and segmented) to examine if LLMs agree on the creativity evaluation of alternative uses. Results reveal high inter-model agreement, with Spearman correlations averaging above 0.7 across models and reaching over 0.77 with respect to the oracle, indicating a high level of agreement and validating the reliability of LLMs in creativity assessment of alternative uses. Notably, models do not favour their own responses, instead they provide similar creativity assessment scores or rankings for alternative uses generated by other models. These findings suggest that LLMs exhibit impartiality and high alignment in creativity evaluation, offering promising implications for their use in automated creativity assessment.

cs.AI↗

arXiv2022

Generating Realistic Synthetic Relational Data through Graph Variational Autoencoders

Synthetic data generation has recently gained widespread attention as a more reliable alternative to traditional data anonymization. The involved methods are originally developed for image synthesis. Hence, their application to the typically tabular and relational datasets from healthcare, finance and other industries is non-trivial. While substantial research has been devoted to the generation of realistic tabular datasets, the study of synthetic relational databases is still in its infancy. In this paper, we combine the variational autoencoder framework with graph neural networks to generate realistic synthetic relational databases. We then apply the obtained method to two publicly available databases in computational experiments. The results indicate that real databases' structures are accurately preserved in the resulting synthetic datasets, even for large datasets with advanced data types.

cs.LG↗

arXiv2022

Verdier duality on conically smooth stratified spaces

In this paper we prove a duality for constructible sheaves on conically smooth stratified spaces. Here we consider sheaves with values in a stable and bicomplete $\infty$-category equipped with a closed symmetric monoidal structure, and in this setting constructible means locally constant along strata and with dualizable stalks. The crucial point where we need to employ the geometry of conically smooth structures is in showing that Lurie's version of Verdier duality restricts to an equivalence between constructible sheaves and cosheaves: this requires a computation of the exit path $\infty$-category of a compact stratified space, that we obtain via resolution of singularities.

math.AT↗

arXiv2021

The six operations in topology

In this paper we show that the six functor formalism for sheaves on locally compact Hausdorff topological spaces, as developed for example in Kashiwara and Schapira's book Sheaves on Manifolds, can be extended to sheaves with values in any closed symmetric monoidal $\infty$-category which is stable and bicomplete. Notice that, since we do not assume that our coefficients are presentable or restrict to hypercomplete sheaves, our arguments are not obvious and are substantially different from the ones explained by Kashiwara and Schapira. Along the way we also study locally contractible geometric morphisms and prove that, if $f:X\rightarrow Y$ is a continuous map which induces a locally contractible geometric morphism, then the exceptional pullback functor $f^!$ preserves colimits and can be related to the pullback $f^*$. At the end of our paper we also show how one can express Atiyah duality by means of the six functor formalism.

math.AT↗

arXiv2021

Whitney stratifications are conically smooth

The notion of conically smooth structure on a stratified space was introduced by Ayala, Francis and Tanaka. This is a very well behaved analogue of a differential structure in the context of stratified topological spaces, satisfying good properties such as the existence of resolutions of singularities and handlebody decompositions. In this paper we prove Ayala, Francis and Tanaka's conjecture that any Whitney stratified space admits a canonical conically smooth structure. We thus establish a connection between the theory of conically smooth spaces and the classical examples of stratified spaces from differential topology.

math.DG↗

arXiv2018

A general proof certification framework for modal logic

One of the main issues in proof certification is that different theorem provers, even when designed for the same logic, tend to use different proof formalisms and produce outputs in different formats. The project ProofCert promotes the usage of a common specification language and of a small and trusted kernel in order to check proofs coming from different sources and for different logics. By relying on that idea and by using a classical focused sequent calculus as a kernel, we propose here a general framework for checking modal proofs. We present the implementation of the framework in a Prolog-like language and show how it is possible to specialize it in a simple and modular way in order to cover different proof formalisms, such as labeled systems, tableaux, sequent calculi and nested sequent calculi. We illustrate the method for the logic K by providing several examples and discuss how to further extend the approach.

cs.LO↗

arXiv2016

Certification of Prefixed Tableau Proofs for Modal Logic

Different theorem provers tend to produce proof objects in different formats and this is especially the case for modal logics, where several deductive formalisms (and provers based on them) have been presented. This work falls within the general project of establishing a common specification language in order to certify proofs given in a wide range of deductive formalisms. In particular, by using a translation from the modal language into a first-order polarized language and a checker whose small kernel is based on a classical focused sequent calculus, we are able to certify modal proofs given in labeled sequent calculi, prefixed tableaux and free-variable prefixed tableaux. We describe the general method for the logic K, present its implementation in a prolog-like language, provide some examples and discuss how to extend the approach to other normal modal logics

cs.LO↗

arXiv2014

Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics

The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a mechanism for producing a classic-like description of them in terms of an effective variety of bivalent semantics; (ii) a mechanism for extracting, from the bivalent semantics so obtained, uniform (classically-labeled) cut-free standard analytic tableaux with possibly branching invertible rules and paired with proof strategies designed to guarantee termination of the associated proof procedure; (iii) a mechanism to also provide, for the same logics, uniform cut-based tableau systems with linear rules. The latter tableau systems are shown to be adequate even when restricted to analytic cuts, and they are also shown to polynomially simulate truth-tables, a feature that is not enjoyed by the former standard type of tableau systems (not even in the 2-valued case). The results are based on useful generalizations of the notions of analyticity and compositionality, and illustrate a theory that applies to many other classes of non-classical logics.

cs.LO↗

arXiv2009

A History of Until

Until is a notoriously difficult temporal operator as it is both existential and universal at the same time: A until B holds at the current time instant w iff either B holds at w or there exists a time instant w' in the future at which B holds and such that A holds in all the time instants between the current one and w'. This "ambivalent" nature poses a significant challenge when attempting to give deduction rules for until. In this paper, in contrast, we make explicit this duality of until to provide well-behaved natural deduction rules for linear-time logics by introducing a new temporal operator that allows us to formalize the "history" of until, i.e., the "internal" universal quantification over the time instants between the current one and w'. This approach provides the basis for formalizing deduction systems for temporal logics endowed with the until operator. For concreteness, we give here a labeled natural deduction system for a linear-time logic endowed with the new operator and show that, via a proper translation, such a system is also sound and complete with respect to the linear temporal logic LTL with until.

cs.LO↗

arXiv2008

Labeled Natural Deduction Systems for a Family of Tense Logics

We give labeled natural deduction systems for a family of tense logics extending the basic linear tense logic Kl. We prove that our systems are sound and complete with respect to the usual Kripke semantics, and that they possess a number of useful normalization properties (in particular, derivations reduce to a normal form that enjoys a subformula property). We also discuss how to extend our systems to capture richer logics like (fragments of) LTL.

cs.LO↗