NASA has awarded Galois, Inc. a Small Business Innovation Research award to conduct research into the application of formal verification to machine learning systems. From the abstract:
Automated tools are quickly making inroads into casual computing environments, solving progressively more complex tasks. However, these advancements still require trading reliability for convenience. Frequent minor failures are acceptable in casual environments, but critical systems cannot make the same exchange. The software systems that NASA develops could greatly benefit from machine learning technologies that have been applied to casual computing, if the software developed by learning algorithms could be verified.
The work will be conducted under Galois’ Formal Methods research program, and seeks to demonstrate increased verification capabilities through the application of model checking to aid the construction of machine learning tools.
For more information about the project, contact Rogan Creswick or John Matthews.