项重写系统合流性的自动策略发明
计算机科学中的逻辑
2025-08-01 v2 人工智能
摘要
项重写在软件验证和编译器优化中发挥着关键作用。随着数十种高度参数化的技术被开发用于证明各种系统属性，自动项重写工具在广泛的参数空间中工作。这种复杂性超出了人类进行参数选择的能力，促使对自动策略发明的研究。在本文中，我们聚焦于项重写系统的一个重要性质——合流性，并应用机器学习开发了首个学习引导的自动合流性证明器。此外，我们随机生成了一个大型数据集来分析项重写系统的合流性。我们的结果聚焦于改进最先进的自动合流性证明器 CSI：当配备我们发明的策略时，它在增强数据集和原始人工创建的基准数据集 Cops 上均超越了其人工设计的策略，证明/否定了此前尚无自动证明的若干项重写系统的合流性。
引用
@article{arxiv.2411.06409,
title = {Automated Strategy Invention for Confluence of Term Rewrite Systems},
author = {Liao Zhang and Fabian Mitterwallner and Jan Jakubuv and Cezary Kaliszyk},
journal= {arXiv preprint arXiv:2411.06409},
year = {2025}
}