# Automated Strategy Invention for Confluence of Term Rewrite Systems

arXiv: https://arxiv.org/abs/2411.06409 · HTML: https://mlsanity.com/paper/2411.06409/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 69 references that are in the map.
- First posted on arXiv 10 Nov 2024.

## Builds on (most cited first, 10 of 10)

- [SMAC3: A Versatile Bayesian Optimization Package for Hyperparameter Optimization](https://mlsanity.com/paper/2109.09831/) (2021)
- [Automated Algorithm Selection: Survey and Perspectives](https://mlsanity.com/paper/1811.11597/) (2018)
- [ParamILS: An Automatic Algorithm Configuration Framework](https://mlsanity.com/paper/1401.3492/) (2014)
- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [MCTS-GEB: Monte Carlo Tree Search is a Good E-graph Builder](https://mlsanity.com/paper/2303.04651/) (2023)
- [Lash 1.0 (System Description)](https://mlsanity.com/paper/2205.06640/) (2022)
- [AC-KBO Revisited](https://mlsanity.com/paper/1403.0406/) (2014)
- [Layer Systems for Proving Confluence](https://mlsanity.com/paper/1404.1225/) (2014)
- [The Certification Problem Format](https://mlsanity.com/paper/1410.8220/) (2014)
- [Smarter Features, Simpler Learning?](https://mlsanity.com/paper/1911.06578/) (2019)

## Abstract (arXiv)

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.