9 - Advances in automated reasoning for rigorous analysis of ML/AI algorithms with Imandra

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.