Probability monad resources

Stream: general

[Ashley Blacquiere]

I'm trying to wrap my head around probability monads for discrete measures. I've found this paper by Bart Jacobs and this MSc thesis by Julian Asilis, both of which have been a good help to start, but I wonder if there is any Lean-specific resource out there, or any resources that closely match Lean's PMF monad, in particular.

I think I've seen @Adam Topaz mention before that the Giry Monad is impossible in Lean - but I'm not sure I understand why that's the case. Any enlightenment anyone can is appreciated. :pray:

[Geoffrey Irving]

Not sure it’s relevant, but I did a bunch of finitely supported probability monad stuff for https://github.com/google-deepmind/debate and it was very pleasant.

[Geoffrey Irving]

The finitely supported case is simpler to work with, since all functions are integrable.

[Benedikt Peterseim]

Hi Ashley, I would be very surprised if Adam said that, since the Giry monad (either on the category of measurable spaces or that of Polish spaces) is an ordinary piece of mathematics, so of course it’s possible to formalize it in Lean. However, judging from the first paragraph, you’re more interested in the computational/CS aspects of probability monads, for which the classical Giry monad(s) aren’t very useful, as classical measure theory is probably as far from constructive as one can get.

Incidentally, I’m currently working on a “toy probabilistic programming language” implemented in Lean, whose purpose is mainly to illustrate the concept of a probability monad, for whenever people ask me about it. A first version should be ready soon, I can let you know if you like.

[Kevin Buzzard]

Indeed we already have the Giry monad in mathlib: docs#MeasCat.Giry

[Kevin Buzzard]

I suspect the Giry monad might be tricky in a simple type theory like Isabelle/HOL, maybe this is where the confusion lies (or maybe I'm just adding to the confusion)

[Adam Topaz]

Ashley Blacquiere said:

I think I've seen Adam Topaz mention before that the Giry Monad is impossible in Lean - but I'm not sure I understand why that's the case. Any enlightenment anyone can is appreciated. :pray:

I don't remember saying this :thinking: .... On the contrary, I think the Giry monad should make its way to mathlib! Note that the one Kevin mentioned is not the monad of probability measures, but rather all measures.

[Adam Topaz]

Benedikt Peterseim said:

Hi Ashley, I would be very surprised if Adam said that, since the Giry monad (either on the category of measurable spaces or that of Polish spaces) is an ordinary piece of mathematics, so of course it’s possible to formalize it in Lean. However, judging from the first paragraph, you’re more interested in the computational/CS aspects of probability monads, for which the classical Giry monad(s) aren’t very useful, as classical measure theory is probably as far from constructive as one can get.

Incidentally, I’m currently working on a “toy probabilistic programming language” implemented in Lean, whose purpose is mainly to illustrate the concept of a probability monad, for whenever people ask me about it. A first version should be ready soon, I can let you know if you like.

Concerning this, I wrote a bit of code along these lines here: https://github.com/adamtopaz/lean_pdist

[Adam Topaz]

It's certainly nowhere near a probabalistic programming language, so I would be curious to see what Benedikt has been working on!

[Jason Rute]

Ashley Blacquiere said:

I think I've seen Adam Topaz mention before that the Giry Monad is impossible in Lean - but I'm not sure I understand why that's the case. Any enlightenment anyone can is appreciated. :pray:

In Lean, there are two types of monads. Programming monads (docs#Monad and docs#LawfulMonad) and category theory monads (docs#CategoryTheory.Monad). The first includes things like Option and the IO monad and supports do notation. There used to be a programming monad for the Giry monad. 5 years ago I said that was impossible even though it existed at the time, but that was based on a subtlety on my part. The (programming) Giry Monad was conditional on the functions being measurable, so it wasn't a lawful monad. (For example, if you tried to do map with a non-measurable function it would be a junk result.) But that didn't necessarily stop it from being useful as long as you only used it with measurable functions.

[Jason Rute]

This looks to be the remnants of the programming Giry Monad: GiryMonad All the monatic operations are implemented, but I guess it isn't an instance of docs#Monad.

[Adam Topaz]

It can't be an instance of docs#Monad because there's a typeclass assumption on the type you feed in.

[Jason Rute]

Ok. Yes, that makes sense (and goes back to my confusion 5 years ago).

[Ashley Blacquiere]

Benedikt Peterseim said:

Incidentally, I’m currently working on a “toy probabilistic programming language” implemented in Lean, whose purpose is mainly to illustrate the concept of a probability monad, for whenever people ask me about it. A first version should be ready soon, I can let you know if you like.

Thanks for the insight. Definitely interested to take a look at your probabilistic DSL, whenever you are ready to share!

[Jason Rute]

Ok, so in summary about the two Giry Monads in Lean:

• The closest you can get an instance of docs#Monad: GiryMonad
• An instance of docs#CategoryTheory.Monad: docs#MeasCat.Giry

[Ashley Blacquiere]

Adam Topaz said:

I don't remember saying this :thinking: .... On the contrary, I think the Giry monad should make its way to mathlib! Note that the one Kevin mentioned is not the monad of probability measures, but rather all measures.

Sorry, @Adam Topaz that was a complete misinterpretation on my part - you were just referring to the do notation for the Giry monad, which I guess is in line with @Jason Rutes comments?

[Ashley Blacquiere]

Jason Rute said:

In Lean, there are two types of monads. Programming monads (docs#Monad and docs#LawfulMonad) and category theory monads (docs#CategoryTheory.Monad). The first includes things like Option and the IO monad and supports do notation.

This is super helpful. I don't know much about category theory, so I wasn't sure that they weren't, in fact, the same thing. Thanks for clarifying.

[Adam Topaz]

Oh yes, I did say that :) this is essentially because of what was said above here, that the Giry monad as it appears in mathlib (e.g. Jason's links) require a measurability typeclass hypothesis, so you can't provide a monad instance.

[Adam Topaz]

So unless do notation is generalized a bit (right now it requires a monad instance), it won't work out of the box.

[Jason Rute]

And to be clear, you could implement the same Giry monad implementation with docs#Monad that you see programmers write with Haskell and Scala. It wouldn't be truly a lawful monad but it could still be convenient and/or fun to implement.

[Patrick Massot]

Benedikt Peterseim said:

Incidentally, I’m currently working on a “toy probabilistic programming language” implemented in Lean, whose purpose is mainly to illustrate the concept of a probability monad, for whenever people ask me about it. A first version should be ready soon, I can let you know if you like.

@Tomas Skrivan is also currently working on probabilistic programming in Lean, so you may want to talk to him.

[Jason Rute]

(And in some sense, all computable functions are continuous for the "natural" topology on a type, so the non-lawfulness wouldn't be a serious issue in practice I think if you are writing executable probabilistic code.)

[Tomas Skrivan]

Yes I'm looking into probabilistic programming. Right now, I'm refining the specifications and skipping most of the proofs. Here is what I can do (see the full file):

Define a probabilistic program

def test (θ : R) : Rand R :=
  let b ~ (flip θ)
  if b then
    Rand.pure 0
  else
    Rand.pure (-θ/2)

Derive a new probabilistic programs, such that the derivative of the mean of test θ w.r.t. to θ is equal to the mean of fdtest_v1

def fdtest_v1 :=
  derive_mean_fwdDeriv R :
    (fun θ : R => test θ)
  by
    enter [θ,dθ]; dsimp
    unfold test

    rand_AD
    rand_push_E
    rand_fdE_as_E R, (flip θ)
    simp'
    rand_pull_E

Derive closed form formula for the mean of fdtest_v1

def fdtest_v1_mean (θ dθ : R) := (fdtest_v1 θ dθ).mean
  rewrite_by
    unfold fdtest_v1
    rand_compute_mean

The random monad is:

structure Rand (X : Type) [MeasurableSpace X] where
  μ : Erased (Measure X)
  is_prob : IsProbabilityMeasure μ.out
  rand : _root_.Rand X   -- ugh why doesn't mathlib have `Mathlib` namespace?

which uses Giry monad(i.e. Measure) for specification and Mathlib's Rand for computation. Currently there is nothing connecting those two and I try to prove stuff under this axiom

@[ext]
axiom ext (x y : Rand X) : x.μ = y.μ → x = y

Which is effectively saying that all random number generators are the same and you can ignore them.

It would be great to somehow combine efforts in this direction. I also noticed that @Fabian Zaiser is interested in Lean and doing probabilistic programming.

[Tomas Skrivan]

As mentioned above there are issues in using Measure as a monad. In Lean, you can't even provide instance Monad Measure because Measure consumes only measurable spaces and when proving LawfulMonad you get into trouble with measurability.

Here is my proposed solution to that, instead of Measure use the continuation(into complete normed spaces) monad:

structure Distribution (X : Type u) where
  action : {Y : Type u} → [NormedAddCommGroup Y] → [NormedSpace ℝ Y] → [CompleteSpace Y] → (X → Y) → Y

I call it Distribution as it relates to generalized functions/distributions. The idea is that f : Distribution X is a distribution on X for Y-valued test functions but if you provide φ : (X → Y) that is not a test function then f.action φ is just a zero.

The great thing is thatDistribution is now Monad and LawfulMonad by rfl.

You can embed Measure X into Distribution X by:

def _root_.MeasureTheory.Measure.toDistribution {X} {_ : MeasurableSpace X} (μ : Measure X) :
    Distribution X := ⟨fun φ => ∫ x, φ x ∂μ⟩

Another great thing is that it is easy to define what a derivative of f : X → Distribution Y should be. Do it in distributional sense.

noncomputable
def distribDeriv
    (f : X → Distribution Y) (x dx : X) : Distribution Y :=
  ⟨fun φ => fderiv ℝ (⟪f ·, φ⟫) x dx⟩

Here is the file defining Distribution and here is the file defining distribDeriv

[Benedikt Peterseim]

Very interesting, @Tomas Skrivan. My approach is a bit different and only really gives a toy version of probabilistic programming which is only supposed to demonstrate how “do elementary probability theory with monads” (see below for what that’s supposed to mean). In particular, it won’t be useful for any serious statistical applications. But you can solve the Monty Hall problem:

def winCar : random Bool := conditionally do  -- Define event "winCar" conditionally.
  let carDoor <- UniformDist (Finset.range 3)  -- A car is placed uniformly at random behind one of three doors.
  let initialDoor <- UniformDist (Finset.range 3)  -- You choose a door, uniformly at random.
  let montysDoor <- UniformDist ((Finset.range 3) \ {carDoor, initialDoor})     -- Monty Hall picks a door (neither your initially chosen door, nor the one with the car).
  return carDoor = 1 | initialDoor = 0 ∧ montysDoor = 2  -- The event that the car is behind Door 1, given that you chose Door 0, and Monty Door 2.

theorem MontyHallProblem : Probability winCar = 2/3 := by rfl

Or a version of the Birthday Paradox:

def numberOfPeople := 3

-- What's the probability that among three people, two of them were born in the same quarter of the year?
def twoPeopleWithSameQuarterOfBirth : random Bool := do
  let l <- IID (UniformDist (Finset.range 4)) numberOfPeople
  return ∃ i j : (Fin numberOfPeople), l[i]! = l[j]! ∧ i ≠ j

-- #eval Probability twoPeopleWithSameMonthOfBirth

theorem BirthdayParadox : Probability twoPeopleWithSameQuarterOfBirth = 5/8 := by rfl

The monad is defined as a submonad of the double dualization (a.k.a. continuation monad) for the rationals:

structure random (α : Type) where
  expectation : (α → ℚ) → ℚ  -- expectation functional
  nonnegative : ∀ f : (α → ℚ), f ≥ 0 → expectation f ≥ 0
  additive : ∀ f g : (α → ℚ), expectation (f + g) = expectation f + expectation g
  normalized : expectation (fun _ ↦ 1) = 1

def Probability (event : random Bool) : ℚ := event.expectation (fun x ↦ if x then 1 else 0)

As a consequence, modeling continuous distributions is not really possible using this "baby Giry monad". But given that (anecdotally) even Paul Erdős struggled with the Monty Hall problem, maybe elementary probability theory can already be quite interesting.

[Tomas Skrivan]

Very nice! I'm impressed and confused that those proofs are by rfl. Do you have a repo somewhere with your code I could have a look at?

I gave up on the nonnegative, additive and normalized conditions and have them under LawfulRand. That way I can keep Rand to be LawfulMonad.

[Kim Morrison]

I just want to call out Tomas's comment here:

rand : _root_.Rand X   -- ugh why doesn't mathlib have `Mathlib` namespace?

and give my extreme endorsement of this sentiment. :-)

I encourage anyone who disagrees to look at the list of short identifiers Mathlib exports!

[Johan Commelin]

Is this list easy to find?

[Benedikt Peterseim]

Tomas Skrivan said:

Very nice! I'm impressed and confused that those proofs are by rfl. Do you have a repo somewhere with your code I could have a look at?

Can't change the visibility to public at the moment (possibly a browser issue), but if you DM me, I can add you as a collaborator.

[Benedikt Peterseim]

Benedikt Peterseim said:

Can't change the visibility to public at the moment (possibly a browser issue), but if you DM me, I can add you as a collaborator.

Okay, now it worked. You can find the repo here.

[Kim Morrison]

Johan Commelin said:

Is this list easy to find?

Found the old gist: https://gist.github.com/semorrison/378c198a657a138c3831f7df8ce1d18f

I think this is Lean+Std+Mathlib jumbled together.

[Tomas Skrivan]

Benedikt Peterseim said:

Benedikt Peterseim said:

Can't change the visibility to public at the moment (possibly a browser issue), but if you DM me, I can add you as a collaborator.

Okay, now it worked. You can find the repo here.

Thank you very much! Really nice approach.

[John Tristan]

Benedikt Peterseim said:

Incidentally, I’m currently working on a “toy probabilistic programming language” implemented in Lean, whose purpose is mainly to illustrate the concept of a probability monad, for whenever people ask me about it. A first version should be ready soon, I can let you know if you like.

With colleagues of mine, we verified a toy "probabilistic program" using the Giry monad in Lean3. This was partly meant as a tutorial on what it means and how it is done. You can read more about it if you're interested and the code is available. These days, I use the PMF monad that's already available in mathlib4 and supports do notation out of the box.

[Benedikt Peterseim]

Thanks for the pointer!

[Benedikt Peterseim]

In case anyone is interested (e.g. @Tomas Skrivan , @Adam Topaz or @Ashley Blacquiere), I have a small update on BabyGiry. It now looks a lot like an actual probabilistic programming language, including an observe statement to condition on events. Here's a Bayesian statistics example:

def Posterior : Random ℚ := randomly do
  let p <-~ Unif (Linspace 0 1) -- Let p be uniformly distributed on {0/10, 1/10, ..., 10/10}.
  let k <-~ Binomial 5 p -- Let k be the number of successes in 5 Bernoulli trials with success probability p.
  observe <| k = 3 -- Observe that k = 3.
  return p

-- #eval ℙ[p ≥ 4/10 ∧ p ≤ 6/10 | p ~ Posterior]
-- >> (1777 : Rat)/3333

example : ℙ[p ≥ 4/10 ∧ p ≤ 6/10 | p ~ Posterior] = 1777/3333 := by rfl

The nice thing is that everything actually has a proper mathematical definition -- and can be used in proofs. In contrast to "real-world" probabilistic programming, it doesn't use sampling, but directly computes the precise probability. This in turn also makes it inefficient for larger examples, of course. So I guess you can now use Lean to solve every first problem sheet of intro to probability theory ever. Not yet sure what this could be useful for, but I had a lot of fun. :)

[Ashley Blacquiere]

Ooh interesting. Thanks for sharing. I still haven't had time to dig more deeply into some of the other details you had added above, but will hopefully examine both more carefully soon.