# Generating Symbolic Reasoning Problems with Transformer GANs

arXiv: https://arxiv.org/abs/2110.10054 · HTML: https://mlsanity.com/paper/2110.10054/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 45 of its 94 references that are in the map.
- First posted on arXiv 19 Oct 2021.

## Builds on (most cited first, 30 of 45)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Neural Message Passing for Quantum Chemistry](https://mlsanity.com/paper/1704.01212/) (2017)
- [A Comprehensive Survey on Graph Neural Networks](https://mlsanity.com/paper/1901.00596/) (2019)
- [Improved Training of Wasserstein GANs](https://mlsanity.com/paper/1704.00028/) (2017)
- [Wasserstein GAN](https://mlsanity.com/paper/1701.07875/) (2017)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [SeqGAN: Sequence Generative Adversarial Nets with Policy Gradient](https://mlsanity.com/paper/1609.05473/) (2016)
- [Analysing Mathematical Reasoning Abilities of Neural Models](https://mlsanity.com/paper/1904.01557/) (2019)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [Generative Adversarial Transformers](https://mlsanity.com/paper/2103.01209/) (2021)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [GAN Augmentation: Augmenting Training Data using Generative Adversarial Networks](https://mlsanity.com/paper/1810.10863/) (2018)
- [Long Text Generation via Adversarial Training with Leaked Information](https://mlsanity.com/paper/1709.08624/) (2017)
- [MaskGAN: Better Text Generation via Filling in the______](https://mlsanity.com/paper/1801.07736/) (2018)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Adversarial Feature Matching for Text Generation](https://mlsanity.com/paper/1706.03850/) (2017)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [Adversarial Ranking for Language Generation](https://mlsanity.com/paper/1705.11001/) (2017)
- [GANS for Sequences of Discrete Elements with the Gumbel-softmax Distribution](https://mlsanity.com/paper/1611.04051/) (2016)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving](https://mlsanity.com/paper/2007.02924/) (2020)
- [Maximum-Likelihood Augmented Discrete Generative Adversarial Networks](https://mlsanity.com/paper/1702.07983/) (2017)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Enhancing the Transformer with Explicit Relational Encoding for Math Problem Solving](https://mlsanity.com/paper/1910.06611/) (2019)

## Built on by (most cited first, 5 of 5)

- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Iterative Circuit Repair Against Formal Specifications](https://mlsanity.com/paper/2303.01158/) (2023)
- [NeuroSynt: A Neuro-symbolic Portfolio Solver for Reactive Synthesis](https://mlsanity.com/paper/2401.12131/) (2024)
- [Breaking the Myth: Can Small Models Infer Postconditions Too?](https://mlsanity.com/paper/2507.10182/) (2025)

## Abstract (arXiv)

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.