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

• URL: http://arxiv.org/abs/2602.02881v1
• Date: Mon, 02 Feb 2026 22:39:02 GMT
• Title: Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics
• Abstract summary: Vision paper articulates a long-term research agenda for formal methods at the intersection with artificial intelligence.<n>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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Knowledge Graph Re-engineering Along the Ontological Continuum (extended version) [0.5461938536945722]
  We aim to define a theoretical construct whose conceptual framework is defined by two distinctions: semantics vs pragmatics, and properties vs affordances.<n>We articulate open research challenges and invite the community to develop the ontological continuum as a shared research agenda.
  arXiv  Detail & Related papers  (2026-05-21T07:33:36Z)
• Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations [0.0]
  This paper outlines a research vision called Learning-Infused Formal Reasoning (LIFR), which integrates machine learning techniques with formal verification.<n>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.
  arXiv  Detail & Related papers  (2026-04-14T13:58:14Z)
• Coordinated Semantic Alignment and Evidence Constraints for Retrieval-Augmented Generation with Large Language Models [4.023398871264227]
  This paper proposes a retrieval augmented generation method that integrates semantic alignment with evidence constraints.<n>It improves factual reliability and verifiability while preserving natural language fluency.
  arXiv  Detail & Related papers  (2026-03-04T22:21:04Z)
• Beyond Pixels: Visual Metaphor Transfer via Schema-Driven Agentic Reasoning [56.24016465596292]
  A visual metaphor constitutes a high-order form of human creativity, employing cross-domain semantic fusion to transform abstract concepts into impactful visual rhetoric.<n>We introduce the task of Visual Metaphor Transfer (VMT), which challenges models to autonomously decouple the "creative essence" from a reference image and re-materialize that abstract logic onto a user-specified subject.<n>Our method significantly outperforms SOTA baselines in metaphor consistency, analogy appropriateness, and visual creativity, paving the way for automated high-impact creative applications in advertising and media.
  arXiv  Detail & Related papers  (2026-02-01T17:01:36Z)
• Integrating Ontologies with Large Language Models for Enhanced Control Systems in Chemical Engineering [1.0674471416489186]
  This work presents an ontology-integrated large language model (LLM) framework for chemical engineering that unites structured domain knowledge with generative reasoning.<n>The proposed pipeline aligns model training and inference with the COPE ontology through a sequence of data acquisition, semantic preprocessing, information extraction, and ontology mapping steps.<n>This integration of symbolic structure and neural generation provides a transparent, auditable approach for applying LLMs to process control, safety analysis, and other critical engineering contexts.
  arXiv  Detail & Related papers  (2025-10-30T18:04:20Z)
• Real-Time Intuitive AI Drawing System for Collaboration: Enhancing Human Creativity through Formal and Contextual Intent Integration [26.920087528015205]
  This paper presents a real-time generative drawing system that interprets and integrates both formal intent and contextual intent.<n>The system achieves low-latency, two-stage transformation while supporting multi-user collaboration on shared canvases.
  arXiv  Detail & Related papers  (2025-08-12T01:34:23Z)
• Beyond Prediction -- Structuring Epistemic Integrity in Artificial Reasoning Systems [0.0]
  It supports structured reasoning, propositional commitment, and contradiction detection.<n>It formalises belief representation, metacognitive processes, and normative verification, integrating symbolic inference, knowledge graphs, and blockchain-based justification.
  arXiv  Detail & Related papers  (2025-06-19T04:20:55Z)
• Continuous Representation Methods, Theories, and Applications: An Overview and Perspectives [55.22101595974193]
  Recently, continuous representation methods emerge as novel paradigms that characterize the intrinsic structures of real-world data.<n>This review focuses on three aspects: (i) Continuous representation method designs such as basis function representation, statistical modeling, tensor function decomposition, and implicit neural representation; (ii) Theoretical foundations of continuous representations such as approximation error analysis, convergence property, and implicit regularization; and (iii) Real-world applications of continuous representations derived from computer vision, graphics, bioinformatics, and remote sensing.
  arXiv  Detail & Related papers  (2025-05-21T07:50:19Z)
• Visual and Semantic Prompt Collaboration for Generalized Zero-Shot Learning [58.73625654718187]
  Generalized zero-shot learning aims to recognize both seen and unseen classes with the help of semantic information that is shared among different classes.<n>Existing approaches fine-tune the visual backbone by seen-class data to obtain semantic-related visual features.<n>This paper proposes a novel visual and semantic prompt collaboration framework, which utilizes prompt tuning techniques for efficient feature adaptation.
  arXiv  Detail & Related papers  (2025-03-29T10:17:57Z)
• Prompt-based Logical Semantics Enhancement for Implicit Discourse Relation Recognition [4.7938839332508945]
  We propose a Prompt-based Logical Semantics Enhancement (PLSE) method for Implicit Discourse Relation Recognition (IDRR) Our method seamlessly injects knowledge relevant to discourse relation into pre-trained language models through prompt-based connective prediction. Experimental results on PDTB 2.0 and CoNLL16 datasets demonstrate that our method achieves outstanding and consistent performance against the current state-of-the-art models.
  arXiv  Detail & Related papers  (2023-11-01T08:38:08Z)
• Discrete, compositional, and symbolic representations through attractor dynamics [51.20712945239422]
  We introduce a novel neural systems model that integrates attractor dynamics with symbolic representations to model cognitive processes akin to the probabilistic language of thought (PLoT) Our model segments the continuous representational space into discrete basins, with attractor states corresponding to symbolic sequences, that reflect the semanticity and compositionality characteristic of symbolic systems through unsupervised learning, rather than relying on pre-defined primitives. This approach establishes a unified framework that integrates both symbolic and sub-symbolic processing through neural dynamics, a neuroplausible substrate with proven expressivity in AI, offering a more comprehensive model that mirrors the complex duality of cognitive operations
  arXiv  Detail & Related papers  (2023-10-03T05:40:56Z)
• Multimodal Relation Extraction with Cross-Modal Retrieval and Synthesis [89.04041100520881]
  This research proposes to retrieve textual and visual evidence based on the object, sentence, and whole image. We develop a novel approach to synthesize the object-level, image-level, and sentence-level information for better reasoning between the same and different modalities.
  arXiv  Detail & Related papers  (2023-05-25T15:26:13Z)
• AIGenC: An AI generalisation model via creativity [1.933681537640272]
  Inspired by cognitive theories of creativity, this paper introduces a computational model (AIGenC) It lays down the necessary components to enable artificial agents to learn, use and generate transferable representations. We discuss the model's capability to yield better out-of-distribution generalisation in artificial agents.
  arXiv  Detail & Related papers  (2022-05-19T17:43:31Z)
• A Dependency Syntactic Knowledge Augmented Interactive Architecture for End-to-End Aspect-based Sentiment Analysis [73.74885246830611]
  We propose a novel dependency syntactic knowledge augmented interactive architecture with multi-task learning for end-to-end ABSA. This model is capable of fully exploiting the syntactic knowledge (dependency relations and types) by leveraging a well-designed Dependency Relation Embedded Graph Convolutional Network (DreGcn) Extensive experimental results on three benchmark datasets demonstrate the effectiveness of our approach.
  arXiv  Detail & Related papers  (2020-04-04T14:59:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.