Alexander Birch Jensen: Formal verification can be used to develop more reliable AI algorithms
Applications of AI algorithms can be found in our everyday lives more than ever, and the future is likely to bring even more. Current applications include machine learning; e.g. in self-driving cars to recognize objects like other cars, and in natural language tools to recognize and process speech. However, AI is not limited to learning algorithms. In search problems such as route finding, a common example being Google Maps, heuristic methods are used to intelligently and efficiently limit the search space. Computers and AI already govern critical parts of our infrastructure. Consequently, our reliance upon their safety and security has never been more vital.
The motivating idea is to bring AI algorithms up to date and beyond, aiming to achieve practically applicable algorithms where functional correctness and computational complexity are considered. At present, the standard methods for implementation of even basic algorithms, searching, sorting and data structures do not build on computer-verified proofs. However, the formalization of the necessary mathematical foundations is available and can be combined with developments in computational logic, interactive and automatic theorem proving and proof assistants.
State-of-the-art proof assistants such as Coq and Isabelle give unprecedented possibilities for design as well as implementation of algorithms with verifiable properties. Building upon recent advancements, the project strives to combine functional programming languages like SML, Haskell, OCaml and Scala with type systems and programming in the Isabelle proof assistant to achieve robust and efficient AI algorithms based on logical foundations.