# Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics

arXiv: https://arxiv.org/abs/2602.02881 · HTML: https://mlsanity.com/paper/2602.02881/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 4 of its 39 references that are in the map.
- First posted on arXiv 2 Feb 2026.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 4 of 4)

- [Iteratively Prompt Pre-trained Language Models for Chain of Thought](https://mlsanity.com/paper/2203.08383/) (2022)
- [Knowledge Graph-based Retrieval-Augmented Generation for Schema Matching](https://mlsanity.com/paper/2501.08686/) (2025)
- [Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP](https://mlsanity.com/paper/1905.05500/) (2019)
- [Automating Verification of State Machines with Reactive Designs and Isabelle/UTP](https://mlsanity.com/paper/1807.08588/) (2018)

## Built on by (most cited first, 1 of 1)

- [Graph Construction and Matching for Imperative Programs using Neural and Structural Methods](https://mlsanity.com/paper/2604.26578/) (2026)

## Abstract (arXiv)

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.