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

This paper presents a long-term research vision for integrating artificial intelligence with formal methods to create a knowledge-driven verification ecosystem that synthesizes contracts, reuses semantic artifacts via hybrid learning-symbolic frameworks, and evolves systematically through compositional reasoning.

The Gist

Imagine you are trying to build a super-safe, high-tech robot. You have a brilliant team of engineers (the formal methods experts) who can write perfect, mathematical rulebooks to prove the robot will never hurt anyone. But these rulebooks are incredibly hard to write, take forever to check, and are so specific that if you change the robot's design slightly, the whole rulebook becomes useless.

On the other side, you have a very fast, very creative assistant (Artificial Intelligence or AI) who can read your messy, human ideas and write drafts instantly. But this assistant sometimes makes things up, gets confused, and can't be trusted to follow the strict laws of physics or logic.

This paper proposes a new way to build robots by making the Engineer and the Assistant work together in a perfect loop. The authors call this vision "Learning-Infused Formal Reasoning."

Here is how their plan works, broken down into three main parts using simple analogies:

1. The Translator: Turning "Human Talk" into "Robot Rules" (Contract Synthesis)

Currently, if you tell an engineer, "The robot arm shouldn't hit the wall," they have to translate that into complex math. If you ask an AI to do it, it might write a rule that looks right but is actually mathematically broken.

The paper suggests a hybrid translator:

• The AI's Job: It acts like a creative scribe. It takes your rough, natural language ideas and drafts a set of rules (called "contracts").
• The Engineer's Job: A strict math-checker (a formal verification tool) immediately tests these rules. If the AI made a mistake or "hallucinated" a rule that doesn't make sense, the checker says, "No, that's wrong," and sends it back.
• The Loop: The AI tries again, using the feedback to fix the rule. They keep going back and forth until the rule is both understandable to humans and mathematically perfect.

The Analogy: Think of it like a dance instructor and a student. The student (AI) tries to learn a dance move based on a description. The instructor (Math Checker) stops them immediately if they step on the wrong beat. The student tries again, gets it right, and eventually, they can perform the dance perfectly together.

2. The Librarian: Finding Old Solutions for New Problems (Artifact Reuse)

Imagine you have a massive library of old, successful robot designs and their rulebooks. Right now, if you want to build a new robot, you have to read every single book manually to find one that looks similar. It's slow and frustrating because the books might use different words or diagrams.

The paper proposes a Smart Librarian:

• The Map: They turn every old rulebook and code into a map (a graph). On this map, the "roads" are the logic connections, and the "landmarks" are the rules.
• The Search: They use the AI to understand the meaning of the words on the map, not just the spelling. So, even if one book says "avoid obstacles" and another says "don't hit walls," the AI knows they mean the same thing.
• The Match: The system finds the best old map that matches your new project, even if the languages are different. It then helps you adapt that old map to fit your new robot.

The Analogy: It's like having a universal translator for recipes. You have a recipe for "Spaghetti" written in Italian and another for "Pasta" written in French. A normal search might miss the connection. This system understands that "spaghetti" and "pasta" are the same dish, finds the Italian recipe, and helps you adjust it to use the ingredients you have in your French kitchen.

3. The Universal Grammar: Making Sure Everyone Speaks the Same Language (Formal Semantics)

The biggest problem with mixing AI and Math is that they speak different languages. AI speaks in probabilities and patterns; Math speaks in absolute truths. If they don't agree on the definition of a word, the whole system breaks.

The paper suggests building a Universal Grammar (based on existing theories like "Institutions" and "UTP").

• This isn't a new language, but a set of strict rules that defines what "truth" means, no matter which language or tool you are using.
• It ensures that when the AI suggests a change, the Math Checker can verify it without getting confused by different notations or tools.

The Analogy: Think of it like currency exchange. If you have US Dollars, Euros, and Yen, you can't just pile them together to buy a car. You need a central bank that knows the exact exchange rate for every currency. This "Universal Grammar" is the central bank that ensures every piece of code and every AI suggestion is converted into a standard value that the safety system can trust.

The Big Picture

The authors argue that we shouldn't just use AI to guess answers, nor should we rely only on slow, manual math checks. Instead, we should build a system where:

1. AI speeds up the process by generating ideas and finding patterns.
2. Math acts as the safety net, ensuring everything is logically sound.
3. Old work is reused intelligently so we don't have to reinvent the wheel every time.

The goal is to move from a world where we check software once and hope it works, to a world where software learns from its past mistakes, reuses proven safety rules, and evolves into a system that is both powerful and trustworthy.

What the paper does NOT claim:

• It does not say this system is already fully built and ready to buy. It is a "vision" and a "proposal" for how to build it.
• It does not claim to solve every problem in AI safety immediately.
• It does not mention specific medical or clinical applications; it focuses on the general engineering of software and cyber-physical systems (like robots or cars).

Technical Summary

Technical Summary: Learning-Infused Formal Reasoning (LIFR)

Problem Statement

Despite rapid advancements in Artificial Intelligence (AI), particularly in Large Language Models (LLMs), these systems lack the mathematical guarantees required for high-stakes applications. Conversely, traditional formal methods offer rigorous correctness proofs but struggle to scale to modern, complex, and constantly evolving AI-driven systems. Current formal verification pipelines face three primary bottlenecks:

1. Specification Difficulty: Converting informal, natural-language requirements into precise, machine-verifiable contracts is hindered by ambiguity, missing domain models, and the instability of current LLMs.
2. Lack of Reuse: Verification artifacts (contracts, proofs, specifications) are rarely reused systematically. Existing repositories are difficult to navigate due to syntactic and semantic heterogeneity, forcing developers to manually search and adapt artifacts.
3. Theoretical Fragmentation: Existing AI-assisted formal methods often operate at the syntactic surface of specific tools (e.g., ACSL, Event-B) without a unifying semantic substrate, preventing interoperability, scalable refinement, and principled cross-tool reasoning.

The paper argues that a unified foundation is missing to bridge the gap between learning-based automation and formal soundness.

Methodology and Research Vision

The paper proposes Learning-Infused Formal Reasoning (LIFR), a long-term research vision that integrates automated contract synthesis, semantic artifact reuse, and refinement-based theory. The methodology is structured around three interconnected pillars:

1. Contract Synthesis (VERIFYAI Framework)

Rather than direct translation, the vision proposes an iterative, neuro-symbolic synthesis process:

• Structured Prompting: Utilizing controlled prompting strategies and domain templates to scaffold LLMs in extracting candidate behavioral obligations from natural language.
• Generative Loop with Verification: Integrating formal verification engines (e.g., Frama-C, Z3, Alt-Ergo) as active components. These tools provide feedback (counterexamples, proof failures) to reshape and constrain subsequent LLM outputs, ensuring semantic discipline and reducing hallucinations.
• Traceability: Explicitly recording mappings between requirements, generated annotations, and revision histories to support human-in-the-loop curation and auditability.

2. Artifact Reuse via Graph Matching

To address the reuse bottleneck, the paper proposes a hybrid framework combining LLMs with graph-based representations:

• Graph Construction: Transforming imperative programs and their specifications into typed, attributed graphs where nodes represent semantic entities (variables, predicates, proof obligations) and edges encode relations (dataflow, control-flow, refinement).
• Semantic Enrichment: Using LLM-derived embeddings (e.g., CodeBERT, SentenceTransformer) to enrich graph nodes with linguistic and latent domain knowledge, bridging heterogeneous notations.
• Approximate Matching: Employing graph matching algorithms that combine structural constraints (ensuring formal soundness) with semantic similarity (provided by LLMs) to discover correspondences between existing artifacts.
• Adaptation: Leveraging graph transformation theory to rewrite and refine aligned artifacts to fit new contexts while preserving semantic invariants.

3. Underlying Theory Foundations

To ensure interoperability and soundness, the vision grounds the LIFR framework in two mathematical theories:

• Unifying Theories of Programming (UTP): Provides an algebraic relational calculus to unify diverse programming paradigms through healthiness conditions and design theories.
• Theory of Institutions: Offers an abstract account of logical systems (signatures, sentences, models, satisfaction) to enable the comparison, translation, and combination of formalisms while preserving semantic meaning.
• Integration: These theories allow AI-generated predicates to be checked against healthiness conditions and enable "satisfaction-preserving translations" across different verification logics.

Key Contributions and Empirical Results

The paper reports on ongoing work and recent empirical studies that validate the feasibility of these concepts:

• Contract Synthesis Evaluation (Beg et al., 2026a): An empirical study on generating ACSL annotations for C programs compared rule-based approaches, the Frama-C RTE plugin, and three LLMs (DeepSeek, GPT-5, OLMo3).
  • Results: Rule-based methods provided consistent performance for safety properties. LLMs demonstrated competitive effectiveness with verification success rates between 83% and 95%. Crucially, LLMs generated a broader range of functional constraints not typically captured by rule-based techniques, suggesting a complementary role for learning-based generation in verification workflows.
• Large-Scale Survey (Beg et al., 2025b): A synthesis of over 100 studies mapping the landscape of AI-enabled requirements formalization.
  • Findings: Identified dominant methodological patterns (e.g., pattern-based rule extraction, hybrid neuro-symbolic pipelines) and highlighted unresolved ecosystem challenges, including toolchain integration barriers and insufficient traceability.
• Graph Construction Pipeline (Beg et al., 2026b): A pipeline transforming programs (C/ACSL, Java/JML, Dafny) into typed graphs.
  • Results: Demonstrated that embedding-enhanced graphs improve the identification of related artifacts across datasets, even when surface syntax differs, validating the approach for scalable semantic analysis.
• Toolchain Evaluation: Empirical investigations into Frama-C's ecosystem (RTE analyser, EVA plugin, PathCrawler) revealed persistent issues like solver instability and path-coverage constraints, motivating the need for coordinated, multi-tool, human-guided workflows.

Significance and Claims

The paper positions LIFR not as a completed system but as a conceptual blueprint for the next generation of formal methods. Its significance lies in:

1. Paradigm Shift: Moving from isolated, ad-hoc tool combinations to a cumulative, knowledge-driven paradigm where specifications and proofs are continuously synthesized and transferred.
2. Hybrid Soundness: Establishing a division of labor where LLMs provide semantic guidance and discovery across heterogeneous notations, while symbolic matching and graph structures ensure formal soundness and structural coherence.
3. Scalability and Reuse: Addressing the inability to systematically transfer verification knowledge across projects by treating artifacts as structured semantic objects rather than isolated syntactic entities.
4. Theoretical Rigor: Grounding AI-assisted verification in UTP and Institution theory to ensure that learning components operate within constraints that guarantee correctness, traceability, and interoperability.

The authors conclude that while current AI-assisted formal methods face challenges regarding dataset fidelity, prompt instability, and scalability, the proposed LIFR framework offers a principled path toward verification ecosystems that evolve systematically, leveraging past efforts to accelerate future assurance.