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

TL;DR

This paper introduces a novel approach to improve variable ordering in cylindrical algebraic decomposition (CAD) by pre-training a Transformer model on easily obtainable annotated data, significantly outperforming existing heuristics.

Contribution

The authors develop a series of tasks for generating large annotated datasets and demonstrate that pre-trained Transformer models can effectively learn superior variable orderings for CAD.

Findings

Transformer-based model outperforms heuristic methods in CAD ordering

Pre-training on task-specific data enhances variable ordering quality

Significant improvement in efficiency of symbolic computation tasks

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.