Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Davide Barbarossa, Paolo Pistone

TL;DR

The paper develops a rigorous bridge between tropical geometry and higher-order probabilistic programming by treating probabilistic programs as tropical analytic objects. It introduces the tropical degree to compress potentially infinite trajectory spaces into finite tropical polynomials, and then uses minimal Newton polytopes to efficiently extract the most likely runs. A parametric weighted relational semantics grounds the interpretation in formal power series, while the tropical intersection type system $\mathbf{P}_{\mathrm{trop}}$ provides a compositional framework to approximate the most likely behavior, with a Viterbi-like algorithm encoded in the type system. Together, these tools yield a scalable reduction from infinitary models to finite combinatorial data, enabling principled inference tasks (I1) and (I2) for higher-order probabilistic programs and paving the way for practical implementations and future extensions such as differential privacy considerations.

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.

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

TL;DR

The paper develops a rigorous bridge between tropical geometry and higher-order probabilistic programming by treating probabilistic programs as tropical analytic objects. It introduces the tropical degree to compress potentially infinite trajectory spaces into finite tropical polynomials, and then uses minimal Newton polytopes to efficiently extract the most likely runs. A parametric weighted relational semantics grounds the interpretation in formal power series, while the tropical intersection type system provides a compositional framework to approximate the most likely behavior, with a Viterbi-like algorithm encoded in the type system. Together, these tools yield a scalable reduction from infinitary models to finite combinatorial data, enabling principled inference tasks (I1) and (I2) for higher-order probabilistic programs and paving the way for practical implementations and future extensions such as differential privacy considerations.

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.
Paper Structure (45 sections, 35 theorems, 60 equations, 10 figures)

This paper contains 45 sections, 35 theorems, 60 equations, 10 figures.

Table of Contents

  1. Introduction
  2. From Probabilistic Models to Probabilistic Programming Languages
  3. The Tropical Geometry of Probabilistic Models
  4. The Tropical Geometry of PPLs
  5. The Tropical Degree
  6. Statistical Inference via Intersection Types and the Newton Polytope
  7. Outline of the Paper
  8. Parametric PCF: Specifying Models via Higher-Order Programs
  9. The language $\mathrm{PCF}\langle \vec{X}\rangle$
  10. $\mathrm{PCF}\langle \vec{X}\rangle$ and Graphical Probabilistic Models
  11. Can We Do Statistical Inference over PCF Programs?
  12. Most Likely Explanations and the Tropical Degree
  13. Most Likely Explanations Efficiently, via the Newton Polytope
  14. Parametric Weighted Relational Semantics
  15. Formal Power Series
  16. ...and 30 more sections

Key Result

Proposition 4.1

${\mathbb{N}^\infty}\{\!\!\{\Sigma\}\!\!\}$ is the free continuous commutative semiring on a finite set $\Sigma$. For any continuous commutative semiring $Q$ and $q\in Q^\Sigma$, the unique map realizing the universal property is $\texttt{ev}_q: {\mathbb{N}^\infty}\{\!\!\{\Sigma\}\!\!\} \to Q$, defi

Figures (10)

  • Figure 1: Rules of $\mathrm{PCF}\langle \vec{X}\rangle$.
  • Figure 2: Examples of Bayesian Networks.
  • Figure 3: Illustrations of the Newton polytope.
  • Figure 4: Typing Rules of $\mathbf{P}_{\mathrm{trop}}$. In rules $@$ and $\mathrm{Y}$, $m_i = [m_{i1},\dots, m_{ip_i}]$ and $p_i= \mathrm{Card}(J_i)$.
  • Figure 5: Derivations from Example \ref{['example62']}.
  • ...and 5 more figures

Theorems & Definitions (105)

  • Definition 2.1
  • Example 2.1
  • Remark 2.1: relation with probabilistic PCF
  • Remark 2.2
  • Example 2.2
  • Proposition 4.1
  • Example 4.1
  • Example 4.2
  • Example 4.3
  • Example 4.4
  • ...and 95 more