将AI与形式化方法结合，实现合同自动生成与验证成果复用。
Learning-Infused Formal Reasoning: From Contract Synthesis to Artifact Reuse and Formal Semantics
- 用大模型+图结构实现跨系统验证成果的语义匹配。
- 支持在不同抽象层级间自动合成规范、合同与证明。
- 适合形式化验证与AI融合研究者参考。
本文提出形式化方法与人工智能交叉领域的长期研究愿景，阐述多个概念与技术维度，并报告当前进展。该工作推动下一代形式化方法的发展，其核心是自动化合同合成、语义化验证成果复用及基于精化的理论体系。我们认为，未来的验证系统应从个体正确性证明转向累积性、知识驱动范式，使规范、合同与证明可在系统间持续合成与迁移。为此，我们提出一种混合框架，结合大语言模型与图表示，实现可扩展的语义匹配与严谨的验证成果复用。学习组件提供跨异构符号与抽象层级的语义引导，符号匹配保障形式化可靠性。基于组合推理，该愿景指向可系统演进的验证生态，充分利用历史验证工作加速未来验证进程。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。