Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations
Arshad Beg, Diarmuid O'Donoghue, Rosemary Monahan
TLDR
This paper introduces Learning-Infused Formal Reasoning (LIFR) to integrate ML with formal methods, enabling automated contract synthesis and artifact reuse.
Key contributions
- Automated synthesis of formal contracts directly from natural language requirements.
- Semantic reuse of verification artifacts via graph matching and learning-based embeddings.
- Development of mathematically grounded semantic foundations using UTP and Theory of Institutions.
Why it matters
This paper addresses the challenge of verifying complex AI systems by making formal methods more scalable and accessible. It proposes a novel framework to automate specification creation and enable knowledge reuse, transforming verification into an efficient, cumulative process.
Original Abstract
Artificial intelligence systems have achieved remarkable capability in natural language processing, perception and decision-making tasks. However, their behaviour often remains opaque and difficult to verify, limiting their applicability in safety-critical systems. Formal methods provide mathematically rigorous mechanisms for specifying and verifying system behaviour, yet the creation and maintenance of formal specifications remains labour intensive and difficult to scale. This paper outlines a research vision called Learning-Infused Formal Reasoning (LIFR), which integrates machine learning techniques with formal verification workflows. The framework focuses on three complementary research directions: automated contract synthesis from natural language requirements, semantic reuse of verification artifacts using graph matching and learning-based embeddings, and mathematically grounded semantic foundations based on the Unifying Theories of Programming (UTP) and the Theory of Institutions. Together these research threads aim to transform verification from isolated correctness proofs into a cumulative knowledge-driven process where specifications, contracts and proofs can be synthesised, aligned and reused across systems.
📬 Weekly AI Paper Digest
Get the top 10 AI/ML arXiv papers from the week — summarized, scored, and delivered to your inbox every Monday.