Speaker
Description
In the past years, we have witnessed an exponential growth of machine learning applications in practically any industry and any aspect of our daily lives. Particle accelerators are no exception. Many references of using Artificial Neural Networks (ANN) in particle accelerators can be found in the literature. Robotics, industrial controls, accelerator operations or beam optimizations are some of domain where researchers have started to use ANNs.
However, when ANNs are deployed in critical systems, an unexpected behavior of the ANN could have serious consequences, including significant accelerator downtime, damage of expensive equipment, or even compromise the personnel safety. For this reason, the late ISO/IEC 24029-2:2023 standard recommends the use of formal methods to guarantee the safety and robustness of ANNs.
Formal methods are techniques used to model complex systems as mathematical entities. They are commonly used to verify hardware designs or to guarantee that critical programs are compliant with their specifications. Formal methods are not only advanced academic techniques. Nowadays they are widely used in critical installations from the aerospace or nuclear industries.
At CERN, we have experience in applying formal methods to PLC (Programmable Logic Controllers) programs that are widely used to control and protect industrial processes. In this presentation, we explain our initial steps on the application of formal methods to verify critical ANNs and to avoid unexpected dangerous behaviors. Subsequently, we present the challenges and benefits faced when applying these techniques to CERN real case studies. Finally, we introduce our future research activities and interests in this domain.
