Formal methods for safety-critical machine learning: a systematic literature review

Area of Science:

• Computer Science
• Artificial Intelligence
• Formal Methods

Background:

• Machine Learning (ML) systems are increasingly used in safety-critical domains, necessitating robust safety assurances.
• Traditional verification methods are inadequate for complex, data-driven ML behaviors.
• Formal methods offer mathematical guarantees for system property adherence, making them crucial for ML safety.

Purpose of the Study:

• To conduct a comprehensive Systematic Literature Review (SLR) on the application of formal methods to enhance ML safety.
• To analyze peer-reviewed research from 2020 to mid-2025 focusing on safety-critical applications.
• To identify application domains, gaps, limitations, and challenges in current research.

Main Methods:

• Systematic Literature Review of 46 peer-reviewed studies.
• Studies selected based on empirical research applying formal methods to modern ML approaches.
• Classification of identified studies into eight distinct formal method categories.

Main Results:

• Identified eight categories of formal methods applied to ML safety: Reachability, SMT-based, MILP/ILP, Model Checking, Runtime Verification, Shielding, Control Barrier Functions, and Risk Verification.
• Synthesized methodological advances, application areas, and comparative strengths against traditional verification.
• Presented bibliometric trends indicating growing research interest.

Conclusions:

• Persistent challenges include scalability, integration with training, and limited real-world validation.
• Future research should focus on integrated training-verification loops, scalable frameworks, hybrid methods, and techniques for new ML paradigms like Large Language Models.
• This review provides a state-of-the-art reference and roadmap for advancing safe ML deployment.