Scaling Trust: A Domain-Specific Relational Extraction for Formal Verification with Limited Data Annotation in NextG Security Protocols

Formal modeling and verification are essential for ensuring the reliability and security of domain-specific protocols, including 5G RRC and Department of Defense (DoD) network specifications. These tasks, however, face significant challenges due to the complexity and jargon of technical language, the limited availability of annotated data, and the difficulty of adapting machine learning models to handle out-of-vocabulary (OOV) scenarios effectively. To address these challenges, this research proposes a hybrid framework that integrates Large Language Models (LLMs) with domain-specific models Mφ, leveraging a Monte Carlo Tree Search (MCTS) approach to dynamically balance generative and classification-based strategies for relation extraction and formal property generation. The proposed framework systematically analyzes the performance of generative and classification models under diverse conditions. Generative models excel in structured and context-aware environments but suffer from error propagation in OOV scenarios due to their sequential dependencies. Classification models, on the other hand, demonstrate robustness to OOV data but lack the ability to leverage contextual dependencies effectively in structured datasets. The MCTS-based model unifies these approaches, dynamically adjusting its reliance on prior information and independence to achieve superior robustness and adaptability. Experimental evaluations highlight the MCTS model's ability to outperform traditional models, maintaining high accuracy even in challenging OOV conditions. By combining insights from information theory with experimental validation, this research introduces a scalable and resilient solution for relation extraction and formal modeling in scenarios with limited annotated data. Future work will focus on optimizing the MCTS framework with advanced reward mechanisms, extending its application to diverse domain-specific protocols, and integrating explainability features to enhance trust and transparency. This work contributes to automating formal verification in complex systems, offering a significant step forward for both academia and industry in advancing the reliability of critical systems.