MCMC as an application domain

[reubenharry]

There is a class of MCMC algorithms like Hamiltonian Monte Carlo or HMC (https://arxiv.org/pdf/1701.02434) which numerically integrate Hamiltonian's equations (with some noise) to generate random walks which converge to a desired stationary distribution (this is basically the same thing as molecular dynamics, and I came across this also: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2236769).

I work on algorithms like HMC, and over the next year or so, I'm quite interested in trying to write implementations in SciLean. There are a few extra ingredients this would need, and I'm curious about how difficult you think these would be to add:

• symplectic integrators
• some handling of probability (e.g. ability to sample from bernoulli and gaussian distributions), some probability monad (if that's how Lean does probability)
• some differential geometry (optional): there are variants of these algorithms which are naturally expressed in the language of differential geometry: https://arxiv.org/abs/1410.5110

[lecopivo]

Implementing symplectic integrators should be easy, it is just a simple formula usually.

SciLean has a probability monad here. Unfortunately I'm still not sure about the definition, it is ok to write programs with it but not completely sure how to precisely prove stuff about such programs.

Yeah there is nothing about differential geometry right now.

Anyway, it would be nice to a pick some easy example for HMC and try to write it in SciLean. I would be very happy to help.

[reubenharry]

Cool, thanks so much for your response! What I'll probably try first in that case is just unadjusted (i.e. no Metropolis Hastings step) HMC, on a Gaussian target. This is just harmonic oscillator dynamics, which you already have in the examples, plus random noise at each step for ergodicity.

I wouldn't really be expecting to prove anything at this point about the algorithm - that seems very hard - but mainly I just want to get used to using Lean and familiar with the layout of SciLean.

(Re. differential geometry, I main asked because it seems like it would be nice to phrase classical mechanics in Lean in terms of geometric concepts like the tangent bundle, cotangent bundle and the symplectic form, but really that's orthogonal to this issue.)