> They are wrapping unverified C++ code (Eigen) for the primitive kernels anyway, such as gemm, so AFAIK it could be extended to launch kernels on GPUs without any modification to the part in Lean that they proved correct.
That is correct. Our Lean development assumes that we have primitive kernels that we trust, and it is otherwise agnostic about how they are implemented. It would be straightforward to have kernels run on GPUs.
> Since most ML users are happy to trust TensorFlow, one could also wrap (unverified) TensorFlow and then use their approach to prove properties about real TensorFlow programs, e.g. that various model-transformations are sound.
This is a great idea. There are a bunch of useful properties TensorFlow users could prove about their programs. For example, a user could prove that their TensorFlow program will never produce a NaN, or that a mutation operation is "safe" and won't corrupt the gradients (see https://groups.google.com/a/tensorflow.org/forum/#!topic/dis... for an example of unsafe usage). Moreover, since verifying specific properties of specific programs is much more routine than verifying algorithms, most of the proofs could be push-button.
To TensorFlow users reading this: what are some common errors you make that are annoying to track down, that we may be able to catch (or prove the absence of) using formal methods? If there is enough demand perhaps we will work on this next.
> They are wrapping unverified C++ code (Eigen) for the primitive kernels anyway, such as gemm, so AFAIK it could be extended to launch kernels on GPUs without any modification to the part in Lean that they proved correct.
That is correct. Our Lean development assumes that we have primitive kernels that we trust, and it is otherwise agnostic about how they are implemented. It would be straightforward to have kernels run on GPUs.
> Since most ML users are happy to trust TensorFlow, one could also wrap (unverified) TensorFlow and then use their approach to prove properties about real TensorFlow programs, e.g. that various model-transformations are sound.
This is a great idea. There are a bunch of useful properties TensorFlow users could prove about their programs. For example, a user could prove that their TensorFlow program will never produce a NaN, or that a mutation operation is "safe" and won't corrupt the gradients (see https://groups.google.com/a/tensorflow.org/forum/#!topic/dis... for an example of unsafe usage). Moreover, since verifying specific properties of specific programs is much more routine than verifying algorithms, most of the proofs could be push-button.
To TensorFlow users reading this: what are some common errors you make that are annoying to track down, that we may be able to catch (or prove the absence of) using formal methods? If there is enough demand perhaps we will work on this next.