Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations

• URL: http://arxiv.org/abs/2604.12747v1
• Date: Tue, 14 Apr 2026 13:58:14 GMT
• Title: Short Version of VERIFAI2026 Paper -- Learning Infused Formal Reasoning: Contract Synthesis, Artefact Reuse and Semantic Foundations
• Abstract summary: 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.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs [10.916179875278326]
  We introduce SKILLFORGE, a framework that decomposes formal code synthesis into a library of atomic, reusable skills.<n>A verification-driven harness orchestrates these skills.<n>On a curated benchmark of natural language to Dafny specification pairs, SKILLFORGE substantially outperforms both state-of-the-art agentic approaches.
  arXiv  Detail & Related papers  (2026-08-30T15:15:00Z)
• AutoVerifier: An Agentic Automated Verification Framework Using Large Language Models [8.006071608749648]
  AutoVerifier is an agentic framework that automates end-to-end verification of technical claims.<n>It decomposes every technical assertion into structured claim triples of the form.<n>It can reliably evaluate the validity and maturity of emerging technologies.
  arXiv  Detail & Related papers  (2026-04-03T01:11:43Z)
• Leveraging LLM Parametric Knowledge for Fact Checking without Retrieval [60.25608870901428]
  Trustworthiness is a core research challenge for agentic AI systems built on Large Language Models (LLMs)<n>We propose the task of fact-checking without retrieval, focusing on the verification of arbitrary natural language claims, independent of their source robustness.
  arXiv  Detail & Related papers  (2026-03-05T18:42:51Z)
• Ontology-to-tools compilation for executable semantic constraint enforcement in LLM agents [0.0]
  We present a proof-of-principle mechanism for coupling large language models (LLMs) with formal domain knowledge semantics.<n>Ontological specifications are compiled into executable tool tools that LLM-based agents must use to create and modify knowledge graph instances.<n>We show how executable ontological semantics guide LLM interfaces and reduce manual schema and prompt engineering, establishing a general paradigm for embedding formal knowledge into generative systems.
  arXiv  Detail & Related papers  (2026-02-03T12:03:26Z)
• Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics [0.0]
  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.
  arXiv  Detail & Related papers  (2026-02-02T22:39:02Z)
• Fundamentals of Building Autonomous LLM Agents [64.39018305018904]
  This paper reviews the architecture and implementation methods of agents powered by large language models (LLMs)<n>The research aims to explore patterns to develop "agentic" LLMs that can automate complex tasks and bridge the performance gap with human capabilities.
  arXiv  Detail & Related papers  (2025-10-10T10:32:39Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1 aims to investigate automated and semi-automated approaches to bridge this gap.<n>This position paper presents a preliminary synthesis of relevant literature to identify recurring challenges and prospective research directions.
  arXiv  Detail & Related papers  (2025-07-18T19:15:50Z)
• Igniting Language Intelligence: The Hitchhiker's Guide From Chain-of-Thought Reasoning to Language Agents [80.5213198675411]
  Large language models (LLMs) have dramatically enhanced the field of language intelligence. LLMs leverage the intriguing chain-of-thought (CoT) reasoning techniques, obliging them to formulate intermediate steps en route to deriving an answer. Recent research endeavors have extended CoT reasoning methodologies to nurture the development of autonomous language agents.
  arXiv  Detail & Related papers  (2023-11-20T14:30:55Z)
• Generating Fact Checking Explanations [52.879658637466605]
  A crucial piece of the puzzle that is still missing is to understand how to automate the most elaborate part of the process. This paper provides the first study of how these explanations can be generated automatically based on available claim context. Our results indicate that optimising both objectives at the same time, rather than training them separately, improves the performance of a fact checking system.
  arXiv  Detail & Related papers  (2020-04-13T05:23:25Z)

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.