Formalization of Machine Learning Theory with Applications to Program Synthesis
This repository contains
- a partial formalization of key results from https://arxiv.org/abs/1804.07795
- The CertRL library as reported in https://arxiv.org/abs/2009.11403
- a formalization of Dvoretzky's stochastic approximation theorem as reported in https://arxiv.org/abs/2202.05959
To compile the Rocq (previously known as Coq) code in this repository, Install Rocq. For example:
- first install opam opam (ocaml package manager).
- Add support for rocq ocaml repositories:
opam repo add rocq-released https://rocq-prover.org/opam/released - If you want to create a local environment (switch), you can run
opam switch create formalml 4.14.2. - Next, run
opam install . --deps-only. This should install all the dependencies needed, including Rocq. - Once the prerequisites are installed, run
maketo compile it.
Alternatively, the included Docker file can be built using Docker to compile the rocq code in a suitable environment.
docker build --pull -t formalml .
This repository is distributed under the terms of the Apache 2.0 License, see LICENSE.txt. It is currently in an Alpha release, without warranties of any kind. Keep in mind that this is an active exploratory research project.