ML4PG in Computer Algebra verification
This work addresses the challenge of formal verification in computer algebra for researchers and developers, but it is incremental as it applies an existing method to a new domain.
The authors tackled the problem of verifying computer algebra algorithms by using ML4PG, a machine-learning tool, to find proof patterns in the CoqEAL library, specifically aiding in the formalization of an efficient algorithm for computing the inverse of triangular matrices.
ML4PG is a machine-learning extension that provides statistical proof hints during the process of Coq/SSReflect proof development. In this paper, we use ML4PG to find proof patterns in the CoqEAL library -- a library that was devised to verify the correctness of Computer Algebra algorithms. In particular, we use ML4PG to help us in the formalisation of an efficient algorithm to compute the inverse of triangular matrices.