AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs

TL;DR

This paper introduces AlphaIntegrator, a learning-based system using a GPT transformer to guide symbolic integration, achieving accurate step-by-step solutions with fewer search steps and highlighting the need for hybrid LLM-symbolic approaches.

Contribution

It presents the first correct-by-construction learning system for symbolic integration using a transformer-guided search, with a new dataset and symbolic engine demonstrating superior efficiency.

Findings

Transformer-guided search reduces steps by 50%

Synthetic training data improves generalization

Fine-tuning LLMs alone is insufficient for symbolic math

Abstract

We present the first correct-by-construction learning-based system for step-by-step mathematical integration. The key idea is to learn a policy, represented by a GPT transformer model, which guides the search for the right mathematical integration rule, to be carried out by a symbolic solver. Concretely, we introduce a symbolic engine with axiomatically correct actions on mathematical expressions, as well as the first dataset for step-by-step integration. Our GPT-style transformer model, trained on this synthetic data, demonstrates strong generalization by surpassing its own data generator in accuracy and efficiency, using 50% fewer search steps. Our experimental results with SoTA LLMs also demonstrate that the standard approach of fine-tuning LLMs on a set of question-answer pairs is insufficient for solving this mathematical task. This motivates the importance of discovering creative methods for combining LLMs with symbolic reasoning engines, of which our work is an instance.