Publikation
On Using Large Language Models Pre-trained on Digital Twins as Oracles to Foster the Use of Formal Methods in Practice
Serge Autexier
In: Tiziana Margaria; Bernhard Steffen (Hrsg.). 12th International Symposium Leveraging Applications of Formal Methods, Verification and Validation, (ISOLA 2024),Crete, Greece, October 27–31, 2024, Part IV. International Symposium Leveraging Applications of Formal Methods, Verification and Validation (ISOLA-2024), October 27-31, Heraklion, Greece, LNCS, Vol. 15222, Springer Cham, 10/2024.
Zusammenfassung
Formal methods based on formal logical or mathematical symbolic techniques provide the highest standards to analyse and ensure safety and security properties of cyber-physical systems—but require a large overhead to specify and especially to verify system properties. The laborious and often manual and creative tasks consist of coming up with the appropriate specifications, to specify required lemmas or to guide the verification process. Once properties, lemmas, proof guidance or a proof itself is given, checking it rigorously for correctness is an easy task. Large Language Models (LLMs) have demonstrated remarkable proficiency in a variety of domains, and there is a recent trend of research that tries to leverage that potential for the creative parts of formal verification. On the other hand, digital twins as virtual replicas of physical systems or processes are used to simulate and analyse real-world systems or scenarios, allowing for predictive maintenance, optimization, and testing of the systems. They can be used to predict and prevent failures, optimize processes, and test different designs in a virtual environment. They can also aid monitoring of real systems and offer support to adapt systems to new situations, e.g., in case of failures to simulate how to reestablish safe operations. Starting from examples of research results using LLMs for symbolic techniques, we advocate researching how to systematically design digital twins for systems under investigation, use simulation capabilities to explore system behaviours and assess their formal properties to create high-quality training data sets to pre-trained LLMs offline. Such LLMs shall then serve in specific verification tasks in practice, to take care of the difficult and, so far, manual task of generating appropriate candidate properties, lemmas or proofs that are subsequently automatically and efficiently checked for correctness using formal techniques.