用机器学习自动发明重写策略，提升自动化证明工具性能。
Automated Strategy Invention for Confluence of Term Rewrite Systems
- 用机器学习从大量生成数据中自动发现重写策略
- 新策略让CSI工具在两个数据集上超越人工设计策略
- 适合形式化验证与编译器优化领域的研究者
术语重写在软件验证和编译器优化中至关重要。现有数十种高度可配置的技术用于证明系统性质，但其参数空间过大，超出人工选择能力，促使我们探索自动化策略发明。本文聚焦术语重写系统的合流性这一关键性质，首次提出基于机器学习的自动合流性证明框架。我们随机生成大规模数据集以分析合流性，并在此基础上改进当前最先进的自动合流性证明工具CSI：当引入所发明的策略后，CSI在扩充数据集和原始人类构建基准数据集Cops上均表现更优，成功证明或反证了多个此前无自动化证明路径的术语重写系统。
原文摘要 · Abstract (English)
Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system properties, automatic term rewriting tools work in an extensive parameter space. This complexity exceeds human capacity for parameter selection, motivating an investigation into automated strategy invention. In this paper, we focus on confluence, an important property of term rewrite systems, and apply machine learning to develop the first learning-guided automatic confluence prover. Moreover, we randomly generate a large dataset to analyze confluence for term rewrite systems. Our results focus on improving the state-of-the-art automatic confluence prover CSI: When equipped with our invented strategies, it surpasses its human-designed strategies both on the augmented dataset and on the original human-created benchmark dataset Cops, proving/disproving the confluence of several term rewrite systems for which no automated proofs were known before.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。