Comment by mdritch
2 days ago
I love z3. I used it for the first time for Jane Street's puzzle last year involving a hashing alg disguised as a neural network. I use a lot of MCMC at work and I have made a few small investigations into MCMC model formal verification via z3, but nothing real yet. This has inspired me to pick that back up.
Can you share more about the connection between MCMC and SAT/SMT? That's a crossover I never thought I'd see.
Sure! Roughly we are using hierarchical models for reads on underlying count or prevalence data. We use those higher-order means or other fit params to kick off remediation tasks at different levels of that hierarchy depending on those higher level params. We assume some correlation between sibling nodes in that hierarchy.
Question: Can one or another of those thresholds in sibling or parent nodes ever be met if some number of the samples are below some floor reading? Or, how many zeros does it take to silence a threshold check on the node itself, a sibling, or a parent?
To make this tractable I have tried gridding fit parameters, freezing randomness, and using simplified algs like original Metropolis-Hastings