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.

翻译：项重写在软件验证和编译器优化中起着至关重要的作用。已有数十种高度参数化的技术被开发用于证明各类系统性质，自动项重写工具因此工作在一个广阔的参数空间中。这种复杂性超出了人类进行参数选择的能力，从而推动了对自动化策略发明的研究。本文聚焦于项重写系统的一个重要性质——合流性，并应用机器学习技术开发了首个学习引导的自动合流性证明器。此外，我们通过随机生成大规模数据集来分析项重写系统的合流性。我们的研究成果着重于改进当前最先进的自动合流性证明器CSI：当配备我们发明的策略后，该工具无论在增强数据集上还是在原始人工创建的基准数据集Cops上，其表现均超越了其人工设计的策略，成功证明/证伪了多个此前未知自动证明结果的项重写系统的合流性。