Learning to Prove Trigonometric Identities
Not on the map. Why?
Abstract (arXiv)
Automatic theorem proving with deep learning methods has attracted attentions recently. In this paper, we construct an automatic proof system for trigonometric identities. We define the normalized form of trigonometric identities, design a set of rules for the proof and put forward a method which can generate theoretically infinite trigonometric identities. Our goal is not only to complete the proof, but to complete the proof in as few steps as possible. For this reason, we design a model to learn proof data generated by random BFS (rBFS), and it is proved theoretically and experimentally that the model can outperform rBFS after a simple imitation learning. After further improvement through reinforcement learning, we get AutoTrig, which can give proof steps for identities in almost as short steps as BFS (theoretically shortest method), with a time cost of only one-thousandth. In addition, AutoTrig also beats Sympy, Matlab and human in the synthetic dataset, and performs well in many generalization tasks.
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). Builds on 23 of its 56 references that are in the map. First posted on arXiv 14 Jul 2022.
Builds on
23 of 56 references.
References · 23
- 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,399
- 2017Proximal Policy Optimization Algorithmscited by 15,215
- 2016Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translationcited by 1,475
- 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
- 2020Generative Language Modeling for Automated Theorem Provingcited by 388
- 2019Analysing Mathematical Reasoning Abilities of Neural Modelscited by 335
- 2019Deep Learning for Symbolic Mathematicscited by 270
- 2017End-to-End Differentiable Provingcited by 161
- 2018Visual Interpretability for Deep Learning: a Surveycited by 155
- 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
- 2021Interpretable Deep Learning: Interpretation, Interpretability, Trustworthiness, and Beyondcited by 118
- 2018Reinforcement Learning of Theorem Provingcited by 69
11 more
- 2019Graph Representations for Higher-Order Logic and Theorem Provingcited by 55
- 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
- 2020INT: An Inequality Benchmark for Evaluating Generalization in Theorem Provingcited by 44
- 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
- 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
- 2016Holophrasm: a neural Automated Theorem Prover for higher-order logiccited by 29
- 2020First Neural Conjecturing Datasets and Experimentscited by 26
- 2019Improving Graph Neural Network Representations of Logical Formulae with Subgraph Poolingcited by 20
- 2020Learning to Prove from Synthetic Theoremscited by 13
- 2018ATPboost: Learning Premise Selection in Binary Setting with ATP Feedbackcited by 12
- 2019A Survey on Theorem Provers in Formal Methodscited by 8
Built on by
Citing papers per year: 2024: 1.
1 paper.
- 2024A Survey on Deep Learning for Theorem Provingcited by 57
- 2024A Survey on Deep Learning for Theorem Proving15 Apr 2024
Similar, not cited
Close in wording, no citation either way
- 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models
- 2025A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
- 2021Learning Equational Theorem Proving
- 2025Theorem Prover as a Judge for Synthetic Data Generation
- 2025ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
- 2025Mathesis: Towards Formal Theorem Proving from Natural Languages
- 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
- 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data