Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917244222570496 |
|---|---|
| author | Beg, Arshad O'Donoghue, Diarmuid Monahan, Rosemary |
| author_facet | Beg, Arshad O'Donoghue, Diarmuid Monahan, Rosemary |
| contents | This vision paper articulates a long-term research agenda for formal methods at the intersection with artificial intelligence, outlining multiple conceptual and technical dimensions and reporting on our ongoing work toward realising this agenda. 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 move beyond isolated 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_02881 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics Beg, Arshad O'Donoghue, Diarmuid Monahan, Rosemary Software Engineering Artificial Intelligence D.2.1; D.2.4; D.2.10; F.4.1; F.4.3 This vision paper articulates a long-term research agenda for formal methods at the intersection with artificial intelligence, outlining multiple conceptual and technical dimensions and reporting on our ongoing work toward realising this agenda. 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 move beyond isolated 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. |
| title | Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics |
| topic | Software Engineering Artificial Intelligence D.2.1; D.2.4; D.2.10; F.4.1; F.4.3 |
| url | https://arxiv.org/abs/2602.02881 |