Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic Programming Languages

TL;DR

This paper explores how tropical geometry can be applied to higher-order probabilistic programming languages to perform statistical inference, linking algebraic geometry with computational semantics.

Contribution

It introduces a novel approach combining tropical geometry with probabilistic programming, enabling efficient estimation of most likely runs through an intersection type system.

Findings

Each probabilistic program is associated with a degree and polyhedron encoding likely runs.

Tropical geometry tools facilitate a compositional estimation of most likely runs.

The approach bridges algebraic geometry and probabilistic semantics effectively.

Abstract

In the last few years there has been a growing interest towards methods for statistical inference and learning based on computational geometry and, notably, tropical geometry, that is, the study of algebraic varieties over the min-plus semiring. At the same time, recent work has demonstrated the possibility of interpreting higher-order probabilistic programming languages in the framework of tropical mathematics, by exploiting algebraic and categorical tools coming from the semantics of linear logic. In this work we combine these two worlds, showing that tools and ideas from tropical geometry can be used to perform statistical inference over higher-order probabilistic programs. Notably, we first show that each such program can be associated with a degree and a n-dimensional polyhedron that encode its most likely runs. Then, we use these tools in order to design an intersection type system that estimates most likely runs in a compositional and efficient way.