Breaking the Data Barrier in Learning Symbolic Computation: A Case Study on Variable Ordering Suggestion for Cylindrical Algebraic Decomposition
Rui-Juan Jing, Yuegang Zhao, Changbo Chen
TL;DR
The study tackles data scarcity in learning optimal variable orderings for Cylindrical Algebraic Decomposition ($ ext{CAD}$) by introducing a pre-training and fine-tuning Transformer framework. It designs CAD-related pre-training tasks, generates large labelled corpora, and demonstrates that pre-trained models substantially surpass traditional heuristics and non-pretrained transformers on multiple CAD datasets, including SMT-derived data. Through extensive ablations, the work analyzes task difficulty, model capacity, data scaling, feature usage, multi-stage pre-training, and tokenization, revealing where deep projection knowledge most benefits ordering decisions. The results indicate meaningful speedups in CAD computations and practical potential for accelerating symbolic reasoning tasks, supported by publicly available datasets and a transparent experimental protocol for future extensions into basic symbolic operations and broader CAD-related methods.
Abstract
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.