“Formally Verifying Neural Networks Properties using Łukasiewicz Logic”
Speaker: Prof. Marcelo Finger
Abstract :
This talk presents an overview of a research line on representing neural networks in Łukasiewicz logic and applying this representation to formal property verification. The approach relies on the correspondence between neural network computations and rational McNaughton functions, enabling the translation of certain neural architectures into logical formulas. Formal verification is then performed via automated theorem proving in Łukasiewicz infinitely-valued logic. We present published results on the logical representation of ReLU–TId neural networks and on the encoding of reachability and robustness properties in Łukasiewicz logic.
This is joint work with Sandro Preto.