Bayesian inference prover

Stream: new members

[Riccardo Buscicchio]

Hi all,
I am new to Lean and I am trying to gauge whether it fits my purposes.
I'd like to use it to prove some results in a Bayesian inference model (i.e. showing that the expression I have obtained for a joint posterior is implied by the prior and likelihood assumptions). Do you have any suggestions on where to start? I am physicist by training with a solid background in statistics.

[Michal Wallace (tangentstorm)]

I don't see the lettersBayes anywhere in the mathlib docs, or from my 2 minutes of searching on google, so you'd probably have to write the support yourself.

There is docs#Probability.

[Michal Wallace (tangentstorm)]

It's not clear to me yet how necessary all that MeasureTheory stuff is if all you want to do is write proofs using Bayesian inference.

[Michal Wallace (tangentstorm)]

If there isn't already some way to do this (I have no idea)...

I wonder what would happen if you started with something like this, and just implemented all the normal Boolean operations on top of it?

inductive Bayes (E : Prop) : Prop where
  | Zero
  | Conf (e : E) (c: { c:Rat // c>0 ∧ c≤ 1 })

e : E is some lean proposition representing a probabilistic event.

Zero E indicates zero confidence in the event. Therefore, you treat it as false and discard any proof.

Conf e c is true as far as Lean is concerned (because e is an instance of E, and therefore a proof of E). But then you also attach a non-zero confidence level c to it.

[Michal Wallace (tangentstorm)]

Well... here's a mockup. It's weird because you have to act as if every statement was 100% true and prove it (disregarding the probabilities), but if you do that, then you can attach confidence levels to it.

import Mathlib.Tactic

inductive Bayes (E : Prop) : Type where
  | BZero
  | BConf (e : E) (c:Rat) -- { r:Rat // r>0 ∧ r ≤ 1 }
deriving Repr

open Bayes

def bAnd {P Q: Prop} (bp: Bayes P) (bq:Bayes Q) : Bayes (P ∧ Q) :=
  match (bp, bq) with
  | (BConf p pc, BConf q qc) => BConf ⟨p,q⟩ (pc*qc)
  | _ => BZero

-- you have to provide a demonstration that the fact is true
-- as if all your confidence levels were 1
def bp : Bayes (Nat.Prime 5) := BConf Nat.prime_five 1
def bq : Bayes (2 < 5) := BConf (by aesop) 0.5
def br : Bayes (2 > 5) := BZero

#eval bAnd bp bq -- confidence 1/2
#eval bAnd bq br -- confidence zero

Again, I have no idea if there's already some way to do this sort of thing in Lean, or even if this is a good approach. It's just what came to mind. Hope it helps.

[Michal Wallace (tangentstorm)]

Thinking about this a bit further, it seems like Xor (or "not equals") and its generalizations operation might require some special handling. Suppose n ∈ { 0, 1, 2, 3 }, and you're trying to gather evidence that n has one of those specific values. You'd want to assign a confidence score to each of the 4 possibilities.

But, the way I've described it above, you would have to carry around proofs that all four propositions were true at the same time, which is not possible without sorry or introducing contradictory axioms.

But for statements like these, you could instead have a structure that carried around the actual statement n ∈ { 0, 1, 2, 3 } and then also had a list of probabilities / confidence levels for each possible value.

I still can't tell if the MeasureTheory stuff is doing anything in this direction...