# Breaking the Data Barrier in Learning Symbolic Computation: A Case Study on Variable Ordering Suggestion for Cylindrical Algebraic Decomposition

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 21 of its 63 references that are in the map.
- First posted on arXiv 20 Jan 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Neural Machine Translation by Jointly Learning to Align and Translate](https://mlsanity.com/paper/1409.0473/) (2014)
- [Understanding intermediate layers using linear classifier probes](https://mlsanity.com/paper/1610.01644/) (2016)
- [Datasets: A Community Library for Natural Language Processing](https://mlsanity.com/paper/2109.02846/) (2021)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [A Survey of Deep Learning for Mathematical Reasoning](https://mlsanity.com/paper/2212.10535/) (2022)
- [Teaching Arithmetic to Small Transformers](https://mlsanity.com/paper/2307.03381/) (2023)
- [Transformers Can Do Arithmetic with the Right Embeddings](https://mlsanity.com/paper/2405.17399/) (2024)
- [Evaluating Mathematical Reasoning Beyond Accuracy](https://mlsanity.com/paper/2404.05692/) (2024)
- [Understanding Addition in Transformers](https://mlsanity.com/paper/2310.13121/) (2023)
- [Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers](https://mlsanity.com/paper/2410.08304/) (2024)
- [Arithmetic Transformers Can Length-Generalize in Both Operand Length and Count](https://mlsanity.com/paper/2410.15787/) (2024)
- [Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition](https://mlsanity.com/paper/1404.6369/) (2014)
- [Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition](https://mlsanity.com/paper/1904.11061/) (2019)
- [Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition](https://mlsanity.com/paper/2304.12154/) (2023)
- [Algorithmically generating new algebraic features of polynomial systems for machine learning](https://mlsanity.com/paper/1906.01455/) (2019)
- [Layered and Staged Monte Carlo Tree Search for SMT Strategy Synthesis](https://mlsanity.com/paper/2401.17159/) (2024)
- [Local Search for Solving Satisfiability of Polynomial Formulas](https://mlsanity.com/paper/2303.09072/) (2023)
- [Data Augmentation for Mathematical Objects](https://mlsanity.com/paper/2307.06984/) (2023)
- [HATSolver: Learning Groebner Bases with Hierarchical Attention Transformers](https://mlsanity.com/paper/2512.14722/) (2025)

## Abstract (arXiv)

Symbolic computation, powered by modern computer algebra systems, has important applications in mathematical reasoning through exact deep computations. The efficiency of symbolic computation is largely constrained by such deep computations in high dimension. This creates a fundamental barrier on labelled data acquisition if leveraging supervised deep learning to accelerate symbolic computation. Cylindrical algebraic decomposition (CAD) is a pillar symbolic computation method for reasoning with first-order logic formulas over reals with many applications in formal verification and automatic theorem proving. Variable orderings have a huge impact on its efficiency. Impeded by the difficulty to acquire abundant labelled data, existing learning-based approaches are only competitive with the best expert-based heuristics. In this work, we address this problem by designing a series of intimately connected tasks for which a large amount of annotated data can be easily obtained. We pre-train a Transformer model with these data and then fine-tune it on the datasets for CAD ordering. Experiments on publicly available CAD ordering datasets show that on average the orderings predicted by the new model are significantly better than those suggested by the best heuristic methods.
