Stream: Miscellaneous

Topic: Coq and statistics - any suggestions for bachelor thesis?

Lessness (Mar 26 2022 at 19:15):

What would you suggest for someone who is interested both in Coq (formal proofs and maybe even formally verified software) and statistics? A topic for bachelor thesis, it is.

Thanks in advance!

Karl Palmskog (Mar 26 2022 at 19:16):

one interesting intersection between formal proofs, logic, and statistics is statistical model checking

Karl Palmskog (Mar 26 2022 at 19:19):

if someone wants to do this in Coq I would probably recommend using the Infotheo library, since for basics only discrete random variables are needed

Karl Palmskog (Mar 26 2022 at 19:23):

so a bachelor thesis topic might be to formalize a logic like PCTL (or adapt someone else's formalization of a similar logic) and write a verified procedure for probabilistic verification of PCTL formulas using traces assumed to be randomly sampled - e.g., Wald's SPRT or something even simpler

Lessness (Mar 28 2022 at 21:50):

Karl Palmskog said:

if someone wants to do this in Coq I would probably recommend using the Infotheo library, since for basics only discrete random variables are needed

If one wants to use continuous random variables, they has to make a library for that, right?

Avi Shinnar (Mar 29 2022 at 11:56):

Another possibility is the FormalML library, available at https://github.com/IBM/FormalML
We plan on making an announcement about it in the next day or so. It includes general probability (including over continuous random variables), and provides tools for working with Expectations, ConditionalExpectations (over general random variables, not just discrete ones), some martingale theory, and more.

Karl Palmskog (Mar 29 2022 at 13:03):

@Avi Shinnar nice, please consider submitting a package for the library to the Coq opam archive for easier reuse: https://github.com/coq/opam-coq-archive/ (recommended name for package: coq-formal-ml)

Lessness (Mar 29 2022 at 18:25):

Had a chat with potential supervisor (?) of bachelor's thesis. :) Now my task is to prepare some presentation which motivates SMC - why it is necessary and how it was created, what it achieves, few practical examples, how good it is (compared to other methods)...

So, I will ask questions here but I will try not to spam too much. Is it okay?

Karl Palmskog (Mar 29 2022 at 18:36):

@Lessness sure, go ahead

Karl Palmskog (Mar 29 2022 at 18:37):

the survey I linked has quite a lot of the answers to those questions, though. The main reason for SMC is scaling better than other verification methods with the size of the random process state space

Karl Palmskog (Mar 29 2022 at 18:42):

I can give a direct link to the survey PDF in private message if you want

Karl Palmskog (Mar 29 2022 at 20:02):

this paper cited in the survey compares SMC performance against numerical methods and explains the case in more detail (but a bit out of date now): https://www.prismmodelchecker.org/papers/sttt_stat.pdf

Lessness (May 01 2022 at 18:35):

I'm still thinking about this etc., I just have exams, tests, homeworks and work too to do. A bit busy right now... So I will post random brain bits here rarely, until I get more time. :|

I was reading the https://dl.acm.org/doi/pdf/10.1007/BF01211866 and there is my attempt to formalize syntax of PCTL formulas.

Require Import Reals.
Open Scope R.

Module PCTL.
  Variable A: Type. (* A should be finite, right? *)
  Variable atom: A -> Prop.

  Definition probability := { p: R | 0 <= p <= 1 }.

  Inductive formula :=
  | atomic: A -> formula
  | negation: formula -> formula
  | conjunction: formula -> formula -> formula
  | until_finite: formula -> formula -> nat -> probability -> formula
  | until_infinite: formula -> formula -> probability -> formula
  | until_strong_finite: formula -> formula -> nat -> probability -> formula
  | until_strong_infinite: formula -> formula -> probability -> formula.

End PCTL.

Print PCTL.formula.

But I don't get what's the difference between "until" operator and "strong until" operator... isn't it the same thing because for continuous probabilities <= and < are the same?

Karl Palmskog (May 01 2022 at 19:01):

what you call until and strong until are not the same, since they are different at the purely logical level (e.g., when you set probability bound to 1, $\geq 1$). See for example "until" vs. "weak until" here: https://en.wikipedia.org/wiki/Computation_tree_logic#Operators

Karl Palmskog (May 01 2022 at 19:03):

the idea with PCTL is that it is compatible with regular CTL at the edges of the probability range, so it's a good idea to understand (and possibly encode in Coq) regular CTL first to get a better understanding of meanings of operators.

Lessness (May 01 2022 at 19:22):

Thank you!

Karl Palmskog (May 01 2022 at 19:26):

here's one encoding of CTL (not saying it's a simple one, but maybe useful): https://github.com/coq-community/comp-dec-modal/blob/master/theories/CTL/CTL_def.v

Last updated: May 31 2023 at 04:01 UTC