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

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.

• If you have a class of models, say models, a function test : models -> bool and a proof that if test m = true then the model is identifiable (ie your test is a sufficient condition for identifiability), or a function test' such that if test m = false then the model is not identifiable (ie your test is a necessary condition), then a user can load your development, describe their own model as some m : models, and run your function(s) (of course you can have more than one test, necessary or sufficient). Jul 4 at 8:15