Automated Strategy Invention for Confluence of Term Rewrite Systems

Zhang, Liao; Mitterwallner, Fabian; Jakubuv, Jan; Kaliszyk, Cezary

doi:10.24963/ijcai.2025/526

Automated Strategy Invention for Confluence of Term Rewrite Systems

Liao Zhang, Fabian Mitterwallner, Jan Jakubuv, Cezary Kaliszyk

Download BibTeX Cite

Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 4724-4732.

https://doi.org/10.24963/ijcai.2025/526

Keywords

Search: S: Algorithm portfolios and configuration
Knowledge Representation and Reasoning: KRR: Automated reasoning and theorem proving

Abstract

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 of term rewrite systems, and apply AI techniques to invent strategies for automatic confluence proving. Moreover, we randomly generate a large dataset to analyze confluence for term rewrite systems. We improve 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 ARI-COPS, proving/disproving the confluence of several term rewrite systems for which no automated proofs were known before.

Liao Zhang, Fabian Mitterwallner, Jan Jakubuv, and Cezary Kaliszyk. 2025. Automated Strategy Invention for Confluence of Term Rewrite Systems. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-25. IJCAI, 4724–4732. https://doi.org/10.24963/ijcai.2025/526

@inproceedings{ijcai2025p526,
  title     = {Automated Strategy Invention for Confluence of Term Rewrite Systems},
  author    = {Zhang, Liao and Mitterwallner, Fabian and Jakubuv, Jan and Kaliszyk, Cezary},
  booktitle = {Proceedings of the Thirty-Fourth International Joint Conference on
               Artificial Intelligence, {IJCAI-25}},
  publisher = {International Joint Conferences on Artificial Intelligence Organization},
  editor    = {James Kwok},
  pages     = {4724--4732},
  year      = {2025},
  month     = {8},
  note      = {Main Track},
  doi       = {10.24963/ijcai.2025/526},
  url       = {https://doi.org/10.24963/ijcai.2025/526},
}

TY  - CPAPER
TI  - Automated Strategy Invention for Confluence of Term Rewrite Systems
AU  - Zhang, Liao
AU  - Mitterwallner, Fabian
AU  - Jakubuv, Jan
AU  - Kaliszyk, Cezary
T2  - Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-25
PB  - International Joint Conferences on Artificial Intelligence Organization
PY  - 2025
SP  - 4724
EP  - 4732
DO  - 10.24963/ijcai.2025/526
UR  - https://doi.org/10.24963/ijcai.2025/526
ER  -