分析近五年AI在形式化方法中的应用趋势，发现定理证明领域最活跃但缺乏统一标准。
Application of AI to formal methods - an analysis of current trends
- 系统梳理2019-2023年189篇相关论文，识别研究热点与空白
- 定理证明是主要应用方向，其他子领域研究较少
- 指出缺少理论基础、共享数据集和标准评测基准
背景：人工智能（AI）已在科研社区广泛应用，我们转向形式化方法（FM）。FM旨在为计算机科学问题提供可靠且可验证的推理。目标：通过系统映射研究，全面概述近五年（2019–2023）将AI应用于FM的研究现状，识别FM如何受益于AI技术，并指出未来研究方向。方法：遵循系统映射研究指南，在四个主要数据库中检索文献，设定纳入与排除标准，并采用广泛滚雪球法挖掘潜在来源。结果：共获得189项研究，分析显示该领域聚焦于定理证明，其他子领域覆盖较少。结论：本研究提供了当前AI应用于FM的定量图景。目前趋势尚未成熟，多数研究关注实际应用，但缺乏理论基础、标准基准或案例研究，且存在训练数据集共享困难与基准不统一的问题。
原文摘要 · Abstract (English)
Context: With artificial intelligence (AI) being well established within the daily lives of research communities, we turn our gaze toward formal methods (FM). FM aim to provide sound and verifiable reasoning about problems in computer science. Objective: We conduct a systematic mapping study to overview the current landscape of research publications that apply AI to FM. We aim to identify how FM can benefit from AI techniques and highlight areas for further research. Our focus lies on the previous five years (2019-2023) of research. Method: Following the proposed guidelines for systematic mapping studies, we searched for relevant publications in four major databases, defined inclusion and exclusion criteria, and applied extensive snowballing to uncover potential additional sources. Results: This investigation results in 189 entries which we explored to find current trends and highlight research gaps. We find a strong focus on AI in the area of theorem proving while other subfields of FM are less represented. Conclusions: The mapping study provides a quantitative overview of the modern state of AI application in FM. The current trend of the field is yet to mature. Many primary studies focus on practical application, yet we identify a lack of theoretical groundwork, standard benchmarks, or case studies. Further, we identify issues regarding shared training data sets and standard benchmarks.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。