Building on deep advances in automated reasoning, we have developed Imandra, a next-generation cloud-native automated reasoning engine. We believe Imandra is the ideal platform to implement the tools and techniques required to analyze ML/AI algorithms used by the US Navy. Imandra is already making real industrial impact: For example, Goldman Sachs is now public with the fact that they use Imandra for the design, verification, certification and auditing of some of their most complex and highly regulated trading algorithms. Fundamentally, the advances in formal verification necessary to make Imandra scale to real-world financial algorithms (including nonlinear decision procedures, SMT modulo recursive functions and automated induction) are deeply needed for the analysis and verification of ML algorithms. We have already begun the application of Imandra to explaining, interrogating and formally verifying opaque ML models (to random forests and DNNs with ReLU activation functions, specifically), and we believe we can bring significant value and advancement to the Navy through the further development and deployment of these techniques.
Benefit: Formal verification and automated reasoning have traditionally been the weapons of choice in providing proof of performance, but applying such techniques to the current machine learning paradigm is highly challenging. With Imandra, we're rising to this challenge by combining formal methods with all three key stages of the machine learning pipeline - data analysis, training, and model evaluation - in order to provide new levels of insight and rigor. We plan to significantly advance our efforts with this project. It's difficult to overestimate the commercial need of these types of techniques. Most industries today rely on AI/ML techniques yet no rigorous, scalable and accessible (to non-experts) techniques for analyzing their behavior. We're working on changing this.
Keywords: Machine Learning, Machine Learning, Robustness, Artificial Intelligence, explainability, Formal methods, Automated Reasoning, Formal Verification, imandra
