analiza aiqbench
This research proposes a hybrid framework that integrates large language models with graph-based representations to enhance formal verification systems. By combining learning-based semantic guidance with symbolic matching for soundness, the approach aims to create cumulative ecosystems where proofs and specifications are systematically reused across heterogeneous notations. This work addresses the critical need for scalable assurance mechanisms in software engineering by evolving traditional formal methods into knowledge-driven paradigms powered by AI.
Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics
arXiv:2602.02881v2 Announce Type: replace-cross Abstract: This paper articulates a long-term research vision for formal methods at the intersection with artificial intelligence, outlining multiple conceptual and technical dimensions and reporting on our ongoing work toward realising this vision. It advances a forward-looking perspective on the next generation of formal methods based on the integration of automated contract synthesis, semantic artifact reuse, and refinement-based theory. We argue that future verification systems must builds towards individual correctness proofs toward a cumulative, knowledge-driven paradigm in which specifications, contracts, and proofs are continuously synthesised and transferred across systems. To support this shift, we outline a hybrid framework combining large language models with graph-based representations to enable scalable semantic matching and principled reuse of verification artifacts. Learning-based components provide semantic guidance across heterogeneous notations and abstraction levels, while symbolic matching ensures formal soundness. Grounded in compositional reasoning, this vision points toward verification ecosystems that evolve systematically, leveraging past verification efforts to accelerate future assurance.
Abstract:This paper articulates a long-term research vision for formal methods at the intersection with artificial intelligence, outlining multiple conceptual and technical dimensions and reporting on our ongoing work toward realising this vision. It advances a forward-looking perspective on the next generation of formal methods based on the integration of automated contract synthesis, semantic artifact reuse, and refinement-based theory. We argue that future verification systems must builds towards individual correctness proofs toward a cumulative, knowledge-driven paradigm in which specifications, contracts, and proofs are continuously synthesised and transferred across systems. To support this shift, we outline a hybrid framework combining large language models with graph-based representations to enable scalable semantic matching and principled reuse of verification artifacts. Learning-based components provide semantic guidance across heterogeneous notations and abstraction levels, while symbolic matching ensures formal soundness. Grounded in compositional reasoning, this vision points toward verification ecosystems that evolve systematically, leveraging past verification efforts to accelerate future assurance.
LNCS Proceedings Submitted Version. 17 pages. Accepted and presented at VERIFAI-2026: The Interplay between Artificial Intelligence and Software Verification LASER center, Villebrumier, France, March 8-11, 2026
Software Engineering (cs.SE); Artificial Intelligence (cs.AI)
D.2.1; D.2.4; D.2.10; F.4.1; F.4.3
arXiv:2602.02881 [cs.SE]
(or arXiv:2602.02881v2 [cs.SE] for this version)
Text integral sub licența deschisă a publicației · 198 cuvinte