Journal Home
Login
Register
Open Access Journal
Submit a Paper
Propose a Special lssue
Open Access
ARTICLE
Formal Verification of Learning-Based Neural Agents in Non-Deterministic and Hybrid Environments
Issue Vol. 2 No. 01 (2025): Volume 02 Issue 01 --- Section Articles
pdf
Abstract
The rapid integration of learning-based neural agents into safety-critical and autonomy-intensive domains has fundamentally reshaped contemporary discussions in artificial intelligence, formal methods, and systems engineering. Neural agents, particularly those based on deep learning and recurrent architectures, are increasingly deployed in environments characterized by non-determinism, partial observability, and complex continuous-discrete interactions. While such agents demonstrate remarkable empirical performance, their opaque decision-making processes and susceptibility to unforeseen environmental behaviors raise profound concerns regarding reliability, accountability, and safety. These concerns are especially pronounced in domains such as autonomous robotics, cyber-physical systems, and multiagent coordination, where failures can result in significant physical, economic, or societal harm. Consequently, formal verification has emerged as a critical research direction aimed at providing rigorous, mathematically grounded guarantees about the behavior of neural agents under all admissible conditions.
This article presents an extensive theoretical and methodological examination of the formal verification of neural agents operating in non-deterministic and hybrid environments. Building upon foundational work in neural network verification, satisfiability modulo theories, and hybrid systems analysis, the article synthesizes and critically analyzes the evolution of verification techniques for learning-enabled systems. Particular emphasis is placed on the formal verification of neural agent-environment systems, including those incorporating recurrent neural networks and non-deterministic environmental dynamics, as explored in seminal studies on neural agents interacting with uncertain environments (Akintunde et al., 2020). The discussion situates this line of research within broader verification paradigms, including abstraction-based methods, reachability analysis, and game-theoretic formulations.
Through a detailed methodological exposition, the article elucidates how neural agents can be modeled as components of closed-loop systems, how environmental non-determinism complicates verification objectives, and how existing tools and frameworks address these challenges. The results section offers an interpretive synthesis of verification outcomes reported across the literature, highlighting patterns of scalability, expressiveness, and limitation. The discussion section provides an in-depth theoretical interpretation, engaging with competing scholarly viewpoints and articulating unresolved tensions between expressivity and tractability. The article concludes by outlining future research trajectories, emphasizing the need for integrated verification-learning paradigms and more expressive formal specifications capable of capturing ethical, social, and safety constraints in learning-based autonomous systems.
Keywords
References
1. Bak, S., Liu, C., Johnson, T. T. The second international verification of neural networks competition summary and results.
2. Akintunde, M. E., Botoeva, E., Kouvaros, P., Lomuscio, A. Formal verification of neural agents in non-deterministic environments. Proceedings of the International Conference on Autonomous Agents and Multiagent Systems.
3. Barrett, C., Tinelli, C. Satisfiability modulo theories. Handbook of Model Checking.
4. Akintunde, M. E., Kevorchian, A., Lomuscio, A., Pirovano, E. Verification of recurrent neural network based agent-environment systems. Proceedings of the AAAI Conference on Artificial Intelligence.
5. Bak, S., Tran, H. D., Hobbs, K., Johnson, T. T. Improved geometric path enumeration for verifying neural networks.
6. Avni, G., Bloem, R., Chatterjee, K., Henzinger, T., Könighofer, B., Pranger, S. Run-time optimization for learned controllers through quantitative games.
7. Ehlers, R. Formal verification of piecewise linear feed-forward neural networks.
8. Elboher, Y., Gottschlich, J., Katz, G. An abstraction-based framework for neural network verification.
9. Baluta, T., Shen, S., Shinde, S., Meel, K., Saxena, P. Quantitative verification of neural networks and its security applications.
10. Althoff, M. An introduction to CORA.
11. Chen, X., Abraham, E., Sankaranarayanan, S. Flow star: an analyzer for non-linear hybrid systems.
12. Amir, G., Schapira, M., Katz, G. Towards scalable verification of deep reinforcement learning.
13. Esteva, A., Robicquet, A., Ramsundar, B., Kuleshov, V., DePristo, M., Chou, K., Cui, C., Corrado, S., Thrun, S., Dean, J. A guide to deep learning in healthcare.
