AlphaIntegrator: Transformer Action Search for Symbolic Integration Proofs

Mert Ünsal, Timon Gehr, Martin Vechev

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 mo…