Formalizing Artificial Neural Networks

Artificial neural networks are a type of machine learning models. They have many applications, including function approximation, classification, and data processing. For instance, large language models, such as those enabling ChatGPT and other recent AI-based tools, are a type of artificial neural networks.

In this project, you will formalize artificial neural networks in the interactive proof assistant Isabelle. Isabelle is a software tool that allows the user to build formal models using a precise language with clear (formal) semantics. This language offers both concepts from programming (e.g., datatypes, recursive functions) and mathematical concepts (e.g., real numbers, quantifiers).

This project will allow you to become familiar with Isabelle, one of the world's leading software tools to assist with the development of formal proofs.

Work environment:: Isabelle (Windows/macOS/Linux)
Useful knowledge/skills:: Machine learning, first-order logic, basic functional programming
Contact:: Tjark Weber

Last modified: 2023-11-05