4
$\begingroup$

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.

$\endgroup$

1 Answer 1

1
+50
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ One thing that might have been unclear from my initial formulation of the question (will update) is that I'd like to get to a point where a user of the system enters a model, a sufficient condition for identifiability is automatically extracted, passed to a prover and either proven or disproven without additional user interaction in at least some practical cases. Your answer suggests that you believe that I can get (with a lot of work) to a point where I can interactively prove certain stuff, which would imply automatic workflow is likely infeasible, am I reading this right? $\endgroup$ Jul 3, 2023 at 19:22
  • $\begingroup$ 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). $\endgroup$ Jul 4, 2023 at 8:15
  • $\begingroup$ If you do not want the user to get into a prover, you can build an extra interface around your tests. You can build something rough that simply parses an input and turns it into something the proof assistant understands, or a more elaborate tool that relies on extraction of your test functions at its core, with some input/output infrastructure around them. $\endgroup$ Jul 4, 2023 at 8:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.