The project aims to advance both the theory and implementation of formal proof certificates for complex specifications that define the safety of probabilistic cyber-physical systems.
On the theoretical side, it will establish a mathematical framework providing formal guarantees for safety and reliability of cyber-physical and software systems, with broad applications to domains such as supply chains, power grids, autonomous robotics, avionics, and beyond.
On the implementation side, the team will develop software tools that automate both the generation of proof obligations for the safety verification of reactive and cyber-physical AI systems and the validation of proof certificates that satisfy these obligations.
This work will lay the foundations for a new generation of trustworthy AI technologies, in which systems are capable of producing formal proofs of probabilistic compliance with safety specifications. Our new theory will enable the design of learnable and efficiently checkable proofs of correctness for stochastic, reactive, cyber-physical systems. Our software will integrate automated reasoning with machine learning infrastructures, bridging the gap between theoretical verification and practical tools for AI safety.
Our goal is to overcome the curse of dimensionality in the formal verification of complex cyber-physical AI systems. The outcome with be a theoretical framework and a software tool for the safety assurance of AI systems, with mathematical certainty.
The funds will provide cash-floats to support research scientists and engineers in the newly founded non-profit organisation Zeroth Research, based in Birmingham, UK, plus travel and compute, enabling the team to achieve their objectives and advance the projects’ goals. As our grant payments on two existing projects are currently in arrears, this funding will allow us to pay salaries, bills, and subcontractors on time while continuing our work beyond the span of the project.
The team consists on global experts in theory and practice of formal verification of cyber-physical systems and software systems, cyber-security and theorem proving: Luca Arnaboldi, Pascal Berrang, Marco Casadio, Marek Chalupa, Mirco Giacobbe, Edoardo Manino, Greg Neustroev, Simon Schmidt, and Ayberk Tosun at Zeroth Research. The broader team includes the external collaborators Alberto Griggio, Giulia Sindoni, Fajar Haifani, and Stefano Tonetta at FBK, Trento, Italy, and Diptarko Roy at the University of Birmingham, UK. The team has an extensive track record in the development of formal verification tools including the award-winning software verifier Symbiotic, the industry-grade SMT-solver MathSAT, and many more.
The curse of dimensionality of complex systems is an our biggest challenge. Nevertheless, several preliminary results published at flagship venues in AI and formal verification such as AAAI, NeurIPS, CAV have already demonstrated the clear potential of proof-certificate-based verification across applications, from automatic control to hardware design. Our project will test these new technical hypotheses at scale.
GBP 1,168,007 from the Advanced Research and Invention Agency.
Mirco Giacobbe
about 1 month ago
Thank you Charbel-Raphael! The agenda builds on proof-certificate-based verification, and there is growing interest in the topic of learnable neural certificates for AI systems safety. I mention two relevant papers from my group and collaborators, but there is much more:
Neustroev, Giacobbe, Lukina, Neural Continuous-time Supermartingale Certificates, AAAI25
Giacobbe, Kroening, Pal, Tautschnig. Neural Model Checking. NeurIPS24
Charbel-Raphael Segerie
2 months ago
Congrats on getting the grant!
I'd be curious which papers or agenda you see as closest to your theoretical framework/broader theory of impact. The project summary mentions preliminary results at AAAI, NeurIPS, CAV—could you link to those?