RESI launched a working group on formal verification of AI

RESI (The Institute for Responsible Superintelligence) has announced the creation of a dedicated working group focused on applying formal verification methods to ensure the safety of neural network systems.

Adam Chlipala, a renowned expert in interactive theorem proving, has been appointed to lead the initiative. The group also includes Shafi Goldwasser and Vinod Vaikuntanathan, who specialize in cryptography and the theoretical foundations of computational security.

The group’s primary task is to develop mathematically rigorous methods for verifying the correctness of AI models. Its members plan to use formal verification tools to minimize risks in the architectures of systems that could potentially have superintelligence-level capabilities.

The group’s work aims to address cybersecurity challenges posed by the unpredictable behavior of neural networks. Researchers intend to integrate methods for proving code properties directly into model training and deployment processes to guarantee compliance with specified safety constraints.

The group’s creation marks a shift from empirical AI testing methods toward approaches based on rigorous mathematical verification. This will allow developers to obtain safety guarantees that standard benchmarks or red-teaming methods cannot provide.