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.
