Using proof assistants to analyze probabilistic models (identifiability in particular)

Question

I recently had an idea that proof assistants/theorem provers might be useful for static analysis of probabilistic models. My familiarity with proof assistants/theorem provers is shallow (some intro in university course long time ago). I am looking for references/hints/previous work and/or reasons why this might be a bad idea :-) I tried searching Google Scholar and the web, but it appears almost nobody has done anything close yet (so maybe it is a bad idea and I shouldn't invest in learning theorem provers)

A class of problems I'd particularly like to be able to at least sometimes automatically solve would be identifiability of models. To start simple, let's say:

$$ y_i \sim N(\mu_i, \sigma) $$

Where we have $\mu_i = f_i(\theta)$ as a function of some unknown vector of parameters $\theta \in \mathbb{R}^K$. Here, a sufficient condition for identifiability is that:

$$ \left(\forall_i : f_i(\bar{\theta}) = f_i(\theta^\prime)\right) \implies \bar{\theta} = \theta^\prime $$

Now it would be cool to be able to automatically prove/disprove such statements at least in some smaller cases.

To be specific some simple examples of what I could extract from a model description + data and present to a prover:

First a case where the model is non-identifiable: $$ \mu_1 = \theta_1 \theta_3 \\ \mu_2 = \theta_2 \theta_3 \\ \mu_3 = \theta_1 \theta_4 \\ \mu_4 = \theta_2 \theta_4 $$

Now e.g. $\bar{\theta} = (1, 1, 1, 1), \theta^\prime = (-1, -1, -1, -1)$ is a counterexample and disproves the statement.

The model becomes identifiable if we set $\theta_1 = 1$ (and thus get a problem with on fewer parameters):

Does that sound at least roughly within the realm of feasible for a modern theorem prover?

I'll note that if $f_i$ are all linear in $\theta$, the problem reduces to computing matrix rank. There are also specific methods for models like factor analysis (which the example above is an isntance of), I am however interested in models that have more complex structures and where those methods no longer work. An alternative is just to try to find the counterexamples numerically, but a prover might provide more assurance (if it works at least sometimes)

UPDATE: To clarify, I am interested in making this into an automatic workflow for a user of my system, i.e. get to a point where I can present a prover/proof assistant with input that for some non-trivial cases can prove/disprove statements like the example above without any additional user interaction.

Answer 1

I would say this is definitely reachable, but nowhere easy.

As your last question suggests, you would like to use proof assistants compared to other tools because they give you more assurance. This is definitely true, because you can teach a proof assistant the theory you are interested in, so that you can prove a statement such as “if this computation of the matrix rank returns this value, then it means the model is identifiable” (and on the way of course also prove that a computation you describe correctly computes the matrix rank).

However, this means that you will likely have to build a whole body of theory before you can get to the results you are interested in. This is feasible (I think most in the PA community are by now convinced there are no fields that cannot be mechanized), but will require quite some work (depending on the availability of results/definitions you can build on, I would guess the order of magnitude man-months to man-years). You might try and mitigate this by admitting some results you want to build upon, and only mechanize specific parts of your work. While this may reduce the burden of proofs, there is no free lunch: the more trust you want to put in the result of your computations, the more proofs you'll have to go through.

Finally, on the topic of computations specifically: not all proof assistants are equal on this. I would strongly advise going for a proof assistant based on (dependent) type theory, like Coq or Lean: by the virtue of the Curry-Howard correspondence, these systems both embed and expressive logics and a proper programming language. This makes expressing computations, showing their correctness and running them very natural and easy.