Generating Symbolic Reasoning Problems with Transformer GANs

Abstract

We study the capabilities of GANs and Wasserstein GANs equipped with Transformer encoders to generate sensible and challenging training data for symbolic reasoning domains. We conduct experiments on two problem domains where Transformers have been successfully applied recently: symbolic mathematics and temporal specifications in verification. Even without autoregression, our GAN models produce syntactically correct instances. We show that the generated data can be used as a substitute for real training data when training a classifier, and, especially, that training data can be generated from a dataset that is too small to be trained on directly. Using a GAN setting also allows us to alter the target distribution: We show that by adding a classifier uncertainty part to the generator objective, we obtain a dataset that is even harder to solve for a temporal logic classifier than our original dataset.

References in corpus (20)

• Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translation
• Neural Message Passing for Quantum Chemistry
• MaskGAN: Better Text Generation via Filling in the______
• TransGAN: Two Pure Transformers Can Make One Strong GAN, and That Can Scale Up
• GANS for Sequences of Discrete Elements with the Gumbel-softmax Distribution
• Maximum-Likelihood Augmented Discrete Generative Adversarial Networks
• Long Text Generation via Adversarial Training with Leaked Information
• Learning-Assisted Automated Reasoning with Flyspeck
• DeepMath - Deep Sequence Models for Premise Selection
• Adversarial Text Generation via Feature-Mover's Distance
• GamePad: A Learning Environment for Theorem Proving
• Generative Language Modeling for Automated Theorem Proving
• TacticToe: Learning to Prove with Tactics
• Learning Continuous Semantic Representations of Symbolic Expressions
• Enhancing the Transformer with Explicit Relational Encoding for Math Problem Solving
• Learning to Discover Efficient Mathematical Identities
• Generative Adversarial Transformers
• Style Example-Guided Text Generation using Generative Adversarial Transformers
• Guiding High-Performance SAT Solvers with Unsat-Core Predictions
• Neural Circuit Synthesis from Specification Patterns