Reasoning about ML, control systems

Stream: new members

[S G]

Hi all, Any pointers to work on use of Lean to reason about the behaviour of
1) Machine learning enabled systems (NN, reinforcement learning, learning-agnostic)
2) Feeback control systems, in particular for parameter tuning of PID systems,
(https://en.wikipedia.org/wiki/Control_theory#PID_feedback_control)

Thanks in advance,
S

[Eric Wieser]

https://github.com/dselsam/certigrad may be of interest regarding the first point

[Jason Rute]

Not lean, but https://arxiv.org/abs/2009.11403. (CertRL is proving properties of standard RL algorithms in Coq.)