Aerial view of Pescara

Geometry and Computer Science
Pescara (IT), February 8–10, 2017

Topics

The workshop aims to promote interaction between geometry professionals using computers in their work, both as simple calculation tools or a research topic. The objective is twofold: on the one hand, to promote the emergence of new scientific collaborations on the edge between geometry and computer science, on the other hand, to disseminate among geometers the use of computational techniques, tools and concepts. To this purpose, the invited speakers are both prominent academics and young researchers, Italians and foreigners, whose research activity relies on, or might foster, the interaction between geometry and computer science.

Speakers

Context

The workshop "Geometry and Computer Science" aims to deepen the connection between research in mathematics and research in computer science.

Computer science supports research in mathematics. The simplest case is utilization of computer algebra systems like SageMath, Mathematica, Maple, that enables execution of huge amounts of symbolic computations. A more sophisticated approach is using software tools to generate and explore conjectures [1]. This can be done in several ways: assisted theorem proving, proof certification, automatic theorem proving. Assisted proof means helping a mathematician to refine an existing line of proof [2,3]. Proof certification means providing internal confidence of an existing, complete proof [3] or of complex computations [4]. Automatic proof means exploring empirically the mathematical problem, to support intuition [5]. Beyond this, computational geometry has traditionally seen a massive utilization of algorithms to address geometrical problems [6].

On the other hand, geometry supports research in computer science. Abstract interpretation, for instance, is a field where geometrical objects in the configuration space of the variables of a program are used to prove that the program is correct [7,8]. Recently, the seminal work of Voevodsky in the homotopy type theory and the univalent foundation of mathematics [9] showed a deep connection between homotopy theory (geometry), logic and theory of types (computer science). Topics like neural networks and deep learning benefit from Riemannian optimization techniques and differential geometry [10].

  1. Hales – Gonthier – Harrison – Wiedijk.
    A special issue on formal proof.
    Notices Amer. Math. Soc. 55(11), 2008.
  2. Hales.
    A proof of the Kepler conjecture.
    Annals of Mathematics 162(3), 2005.
  3. Ciolli – Gentili – Maggesi.
    A certified proof of the cartan fixed point theorems.
    Journal of Automated Reasoning 47(3), 2011.
  4. Théry.
    Certified version of Buchberger’s algorithm.
    Automated Deduction - CADE-15, 1998.
  5. Fuchs – Théry.
    A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry.
    Automated Deduction in Geometry: 8th International Workshop, 2011.
  6. Boucetta – Morvan.
    Differential Geometry and Topology, Discrete and Computational Geometry.
    IOS press, 2005.
  7. Rodríguez-Carbonell – Kapur.
    Automatic generation of polynomial invariants of bounded degree using abstract interpretation.
    Science of Computer Programming, 64(1), 2007.
  8. Cousot – Halbwachs.
    Automatic discovery of linear restraints among variables of a program.
    POPL, 1978.
  9. The Univalent Foundations Program Institute for Advanced Study
    Homotopy Type Theory: Univalent Foundations of Mathematics.
    http://homotopytypetheory.org/book, 2013.
  10. Luigi Malagò.
    Research Project "Riemannian Optimization Methods for Deep Learning".
    Romanian Institute of Science and Technology, 2016.

Schedule

Wed, 8th FebThu, 9th FebFri, 10th Feb
09:30–10:30registrationAngellaHasler
10:30–11:00opening/coffee breakcoffee breakcoffee break
11:00–12:00GourgoulhonFerrarioMonniaux
12:00–13:00MaggesiUrbanSacerdoti Coen
13:00–15:00lunchlunchlunch & panel discussion
15:00–16:00ZaffanellaThéry
16:00–17:00PistoneRodolà
17:00–17:30coffee breakcoffee break
17:30–18:30AhrensBergomi
18:30–19:30Speroni di Fenizio
19:30–dinnersocial dinner
Benedikt Ahrens

Introduction to homotopy type theory (Slides)


Abstract: In this talk, I give an introduction to homotopy type theory and univalent foundations. Homotopy type theory is a field of mathematics exploring the connection between type theory (a formal language suitable for programming) and homotopy theory. Univalent foundations are foundations of mathematics based on homotopical interpretations of type theory, and actively used as a logical basis for formalization of mathematics in computer proof assistants.
Daniele Angella

SageMath experiments in Differential and Complex Geometry (Slides)


Abstract: We present how SageMath can help in research in Complex and Differential Geometry, with two simple applications. We consider two "classification problems" on quotients of Lie groups, namely, "computing cohomological invariants", and "classifying special geometric structures", and we set the problems to be solved with SageMath.
Mattia Bergomi

Word embedding: Deep Learning and Computational Topology for the evaluation of context-based semantic change


Abstract: We recently witnessed the fast ascent of artificial intelligence and deep learning as an invaluable tool in many applications. Despite the effectiveness of these methods, it is often hard to interpret the inner representation that neural networks create to achieve a certain task. Our aim is to show through an intuitive application, how geometry and topology can allow to better grasp the nature of the output of a layer of a neural network, or the final representation of the dataset used during training. We will tackle the problem of semantic shift of words, when used in completely different contexts, in particular lyrics of songs belonging to different genres. Word embedding, in particular the "shallow" neural models used in word2vec [1], will allow us to produce a meaningful, high-dimensional representation of words, given the frame of reference in which they lie (the genre). Thereafter, we will generate a low-dimensional representation of these spaces [2], to be explored both from the semantic and geometric viewpoint. To do so, we will use persistent homology [3,4], a topological technique that allows to grasp both the geometric and topological features of a manifold. This technique makes possible to compute relevant regions within the representations we obtained, and measure a distance between different word embeddings.
[1] Goldberg, Yoav, and Omer Levy. "word2vec Explained: deriving Mikolov et al.'s negative-sampling word-embedding method.", arXiv:1402.3722 (2014).
[2] Maaten, Laurens van der, and Geoffrey Hinton. "Visualizing data using t-SNE." Journal of Machine Learning Research 9.Nov (2008): 2579-2605.
[3] Frosini, Patrizio, and Claudia Landi. "Size theory as a topological tool for computer vision." Pattern Recognition and Image Analysis 9.4 (1999): 596-603.
[4] Kurlin, Vitaliy. "A fast and robust algorithm to count topologically persistent holes in noisy clouds." Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 2014.
Davide Ferrario

Symmetries, computers, and periodic orbits for the n-body problem (Slides)


Abstract: Periodic orbits play a central role in the n-body problem. In the attempt of understanding them, in the sense of computing their existence, qualitative and quantitative properties, and classifying such orbits and symmetries, computers have been extensively used in many ways since decades. I will focus on some very special symmetric orbits, which occur as symmetric critical points of the gravitational Lagrangian action functional. The exploration of the realm where such critical points live, i.e. the loop space of the n-point configuration space, raised computational, epistemological and mathematical questions that needed to be addressed and that I have found interesting. The aim of the talk is to explain how such questions and issues were (more or less naively) considered in the development of a software package that combined symbolic algebra, numerical and scientific libraries, human interaction and visualization.
Eric Gourgoulhon

Differential Geometry with SageMath (Slides) (Slides on running SageMath)


Abstract: The SageManifolds project [1] is devoted to implementing differential geometry and tensor calculus in the free computer algebra system SageMath [2]. The functionalities included in the latest version of SageMath (7.5) are maps between manifolds, with pullback and pushforward operators, curves, standard tensor calculus, exterior calculus, Lie derivatives, affine connections and pseudo-Riemannian metrics, as well as some plotting capabilities. I shall discuss briefly the SageManifolds implementation, before illustrating some of its features by specific examples.
[1] http://sagemanifolds.obspm.fr
[2] http://www.sagemath.org/
Maximilian Hasler

Overview of Computer Algebra Software for Tensor Calculus


Abstract: In this talk, we review and compare several software packages for differential geometry and tensor calculus in particular.
To start with, we describe a few situations where such software can be useful for mathematicians and theoretical physicist, in particular. Then we discuss the most popular but also some less known existing solutions. They come in various flowers such as (sometimes several different) "libraries" or "packages" for the well known Computer Algebra Systems (Mathematica, Maple, Sage....), but also as independent "stand-alone" implementations.
We give a preview of how a user would interact with the software, give a summary of the features, advantages and drawbacks of the different products, and compare them among each other.
Finally, we summarize the main distinguishing characteristics of the individual solutions and attempt to give recommendations about the most suitable choice(s) depending on the particular problem to be tackled.
Marco Maggesi

A formalization of metric spaces in HOL (Slides) (Page on the speaker's web site)


Abstract: We present a computer formalization of metric spaces in the HOL Light theorem prover. Basic results of the theory of complete metric spaces are provided, including the Banach Fixed-Point Theorem, the Baire Category Theorem and the completeness of the space of continuous bounded functions. A decision procedure for a fragment of the elementary theory of metric spaces is also implemented. As an application, the Picard-Lindelöf theorem on the existence of the solutions of ordinary differential equations is proved by using the well-known argument which appeals to the Banach theorem.
David Monniaux

A survey of Satisfiability Modulo Theory (Slides)


Abstract: Satisfiability modulo theory (SMT) consists in testing the satisfiability of first-order formulas over linear integer or real arithmetic, or other theories. In this survey, we explain the combination of propositional satisfiability and decision procedures for conjunctions known as DPLL(T), and the alternative "natural domain" approaches. We also cover quantifiers, Craig interpolants, polynomial arithmetic, and how SMT solvers are used in automated software analysis.
Giovanni Pistone

Information Geometry: background and applications in Machine Learning (Slides)


Abstract: Information Geometry (IG) is the name given by S. Amary to the study of statistical models with the tools of Differential Geometry. The subject is old, as it was started by the observation made by Rao in 1945 that the Fisher information matrix of a statistical model defines a Riemannian manifold on the space of parameters. An important advancement was obtained by Efron in 1975 by observing that there is further relevant affine manifold structure induced by exponential families. Today we know that there are at least 3 differential geometrical structure of interest: the Fisher-Rao Riemannian manifold, the Nagaoka dually flat affine manifold, the Takatsu Wasserstein Riemannian manifold.
In the first part of the talk I will present a synthetic unified view of IG based on a non-parametric approach, see Pistone and Sempi (1995), and Pistone (2013). The basic structure is the *statistical bundle* consisting of all couples of a probability measure in a model and a random variable whose expected value is zero for that measure.
The vector space of random variables is a statistically meaningful expression of the tangent space of the manifold of probabilities.
In the central part of the talk I will present simple examples of applications of IG in Machine Learning developed jointly Luigi Malagò (RIST, Cluj-Napoca). In particular, the examples consider either discrete or Gaussian models to discuss such topics as the natural gradient, the gradient flow, the IG of Deep Learning, see R. Pascanu and Y. Bengio (2014), and Amari (2016). In particular, the last example points to a research project just started by Luigi as principal investigator, see details in http://www.luigimalago.it/.
S. Amari (2016) *Information geometry and its Applications* Springer
S. Amari and H. Nagaoka (2000) *Methods of Information Geometry* AMS & OUP
L. Malagò, M. Matteucci, and G. Pistone (2011) Towards the geometry of estimation of distribution algorithms based on the exponential family *Proceedings of FOGA '11* 230--242 ACM
L. Malagò and G. Pistone (2015) Natural Gradient Flow in the Mixture Geometry of a Discrete Exponential Family *Entropy* 17 4215-4254
R. Pascanu and Y. Bengio (2014) Revisiting natural gradient for deep networks arXiv:1301.3584
G. Pistone and C. Sempi (1995) An Infinite-Dimensional Geometric Structure on the Space of all the Probability Measures Equivalent to a Given One *Ann. Statist.* 23 1543-1561
G. Pistone (2013) Examples of Application of Nonparametric Information Geometry to Statistical Physics i*Entropy* 15 4042-4065
A. Takatsu (2011) Wasserstein geometry of Gaussian measures *Osaka Journal of Mathematics* 48 1005–1026.
Emanuele Rodolà

Geometric Deep Learning (Slides)


Abstract: Many signal processing problems involve data whose underlying structure is non-Euclidean, but may be modeled as a manifold or (combinatorial) graph. For instance, in social networks, the characteristics of users can be modeled as signals on the vertices of the social graph. Sensor networks are graph models of distributed interconnected sensors, whose readings are modelled as time-dependent signals on the vertices. In genetics, gene expression data are modeled as signals defined on the regulatory network. In computer graphics and vision, 3D objects are modeled as Riemannian manifolds (surfaces) endowed with properties such as color texture. The complexity of geometric data and the availability of very large datasets (in the case of social networks, on the scale of billions) suggest the use of machine learning techniques. In particular, deep learning has recently proven to be a powerful tool for problems with large datasets with underlying Euclidean structure. The purpose of this talk is to overview the problems arising in relation to geometric deep learning (i.e. on non-Euclidean domains) and present solutions existing today for this class of problems, as well as key difficulties and future research directions.
Claudio Sacerdoti Coen

Formalizing a Result in Formal Topology in Type Theory


Abstract: Formal Topology is a generalization by Sambin, Martin-Löf et alt. of both Point-Set and Point-Free topologies that can be carried out in a very weak foundation that is a type-theory that is both intuitionistic (as a logic) and predicative. Both requisites create strong links with the computational interpretation: by being intuitionistic, all proofs can be extracted to programs; by being predicative there is a clear distinction between sets, whose elements can be represented concretely in a computer, and classes whose elements are ideal objects geometrical intuition can be used on.
In the talk I will discuss a formalization of a result of Formal Topology that was carried out in a predicative version of the Calculus of Constructions. The result is stated categorically, as the existence of a full, faithful and dense functor between two categories, and it does not hold for classical topology. Therefore the formalization also deals with a bit of category theory, and it does so in an intensional foundation where quotients are not available.
Moreover, we will also introduce Sambin's Overlap Algebras that are an algebrization of the structure of the powerset in an intuitionistic setting and that are to intuitionistic logic what boolean algebras are to classical logic. In our formalization Overlap Algebras will be a tool to force the theorem prover to reason algebraically, at an high level, avoding the unwanted expansion of definitions.
Pietro Speroni di Fenizio

An introduction to Artificial Chemistries: Algebra applied to Informatics applied to Biology (Slides)


Abstract: We are going to see an example of how mathematics helped unravel the relations between the emerging structures in a non mathematical field, Artificial Chemistries.
Artificial Chemistries came out of Artificial Life.
Artificial Life came out of Cybernetics, (the study of) Complex Systems and Artificial Intelligence.
And Complex Systems came out of (the study of) Chaotic Systems.
When scientists, often IT scientists, started approaching complex systems they observed that complex systems, systems that had Universal Computation Capabilities, for example, lived between simpler cyclic systems, and more complicated chaotic ones. Also Complex Systems appeared to have different layers of complexity. With sometimes some complex systems containing others as sub systems. As such the idea of a hierarchy of complex system was born. This was inherited directly inside the field of Artificial Chemistries, were special emerging structures (organisations) were observed. And were observed being hierarchically contained one in the other. All this were simple observations made by biologists, chemists, IT scientists.
Using mathematical formalism to study all this, it was then observed how those system were not strictly "hierarchical", but had a "partially ordered" structure. Organisations not only were partially ordered, but formed a lattice. And the fact that it was a lattice was later used to simplify the research of the set (lattice) of all organisations. In other words mathematical formalism was necessary to classify correctly a number of phenomenon observed in non mathematical fields. And then its theorems could be applied to find all those emerging structures.
Laurent Théry

Proof Assistant and Planar Geometry (Slides)


Abstract: A proof assistant is a computer tool that helps mechanizing mathematical reasoning.
Planar geometry has been one of the areas of mathematics where such a tool has been applied successfully.
In our talk, we will consider three examples of formalisations that have been carried out in the Coq proof assistant: an educational formalisation of high-school geometry, the generation of certificates via Gröbner basis and the formalisation of Grassmann-Cayley algebras.
Josef Urban

Learning-assisted Theorem Proving and Formalization (Slides)


Abstract: The talk will start by briefly introducing the setting of formal mathematics and several large formalization projects. Then we will discuss several AI methods for learning and reasoning developed over large formal math corpora. We will show examples of AI systems implementing positive feedback loops between learning and deduction, and show the performance of the current methods over the Flyspeck, Isabelle, and Mizar libraries. Finally, we will discuss AI methods that we have recently started to develop for automating the translation of informal mathematics to formal. These methods combine statistical parsing of informal mathematics with the large-theory theorem proving methods.
Enea Zaffanella

Polyhedra to reason about software (Slides)


Abstract: In computer science, formal methods are used to assign meaning to programs and other computational entities, so as to enable reasoning about them. Undecidability and complexity results motivate the adoption of sound, but incomplete, approximations. We will informally show how computations based on polyhedra arise as natural choices when trying to approximate numerical properties. We will thus focus our interest on the polyhedral operations that are needed by automatic analyzers and verifiers, describing a few results in some more detail.
Warning! Conference is over and registration is no longer possible.
#NameAffiliation

Workshop's Location

The workshop will be held here:
Room 16B
University of Chieti–Pescara
viale Pindaro 42, Pescara

Reaching Pescara

Pescara has a small airport, Abruzzo Airport, very close to downtown. If traveling directly to Abruzzo Airport is not an option (very likely!), consider going through Rome Fiumicino Airport From there, there are many bus connections (~3h 20m travel time), with either Prontobus or Di Carlo Bus.

Another option is landing in Rome Ciampino Airport: from there you can find bus connections to Pescara with Prontobus (~2h 30m). If you are in Rome but not at the airport, in addition to Prontobus and Di Carlo Bus, you may consider Flixbus and Arpa-Di Febo-Capuani-Di Fonzo buses.

Technically you could reach Pescara by train, with trains departing from Rome Tiburtina station. However, trains on the line Rome–Pescara are quite slow. On the bright side, the trip by train is interesting since trains pass trough many small rural villages in the innermost part of Italy. If you have time to spare (and no work to do... probably no Internet connection there) it could be an alternative.

If you are in Italy everywhere else, you can reach Pescara by bus with Flixbus or by train.

Accomodations

This is a list of hotels in downtown Pescara or near the place of the workshop.

Hotel Esplanade
4-stars hotel
Location: center of Pescara, at the seafront (the workshop place can be reached by bus in 15 minutes)
Hotel Plaza
4-stars hotel
Location: center of Pescara (the workshop place can be reached by bus in 15 minutes)
Hotel Alba
3-stars hotel
Location: center of Pescara (the workshop place can be reached by bus in 15 minutes)
Hotel Holiday
3-stars hotel
Location: close to the university, at the seafront (the workshop place can be reached on foot in 15 minutes)
Jolie bed & breakfast
Location: close to the university (the workshop place can be reached on foot in 5 minutes)
Hotel Regent
3-stars hotel
Location: at the seafront (the workshop place can be reached on foot in 15 minutes)

Organizers

Gianluca Amato
Università degli Studi “G. d'Annunzio”, Italy

Giovanni Bazzoni
Philipps-Universität Marburg, Germany

Marco Maggesi
Università degli Studi di Firenze, Italy

Francesca Scozzari
Università degli Studi “G. d'Annunzio”, Italy

Maurizio Parton
Università degli Studi “G. d'Annunzio”, Italy

Sponsors

INDAM -- logo
Dipartimento di Economia -- Università d'Annunzio -- logo