# Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 12 references that are in the map.
- First posted on arXiv 27 Feb 2023.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [ImageNet-trained CNNs are biased towards texture; increasing shape bias improves accuracy and robustness](https://mlsanity.com/paper/1811.12231/) (2018)
- [Generalisation in humans and deep neural networks](https://mlsanity.com/paper/1808.08750/) (2018)
- [Generalization in Deep Learning](https://mlsanity.com/paper/1710.05468/) (2017)
- [Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition](https://mlsanity.com/paper/1904.11061/) (2019)
- [Using Machine Learning to Improve Cylindrical Algebraic Decomposition](https://mlsanity.com/paper/1804.10520/) (2018)

## Built on by (most cited first, 1 of 1)

- [Data Augmentation for Mathematical Objects](https://mlsanity.com/paper/2307.06984/) (2023)

## Abstract (arXiv)

Cylindrical Algebraic Decomposition (CAD) is a key proof technique for formal verification of cyber-physical systems. CAD is computationally expensive, with worst-case doubly-exponential complexity. Selecting an optimal variable ordering is paramount to efficient use of CAD. Prior work has demonstrated that machine learning can be useful in determining efficient variable orderings. Much of this work has been driven by CAD problems extracted from applications of the MetiTarski theorem prover. In this paper, we revisit this prior work and consider issues of bias in existing training and test data. We observe that the classical MetiTarski benchmarks are heavily biased towards particular variable orderings. To address this, we apply symmetries to create a new dataset containing more than 41K MetiTarski challenges designed to remove bias. Furthermore, we evaluate issues of information leakage, and test the generalizability of our models on the new dataset.