Learning to Prove Trigonometric Identities
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingImitation LearningSimilar Papers 제목 키워드 기반
Towards Symmetry-sensitive Pose Estimation: A Rotation Representation for Symmetric Object Classes
Symmetric objects are common in daily life and industry, yet their inherent orientation ambiguities that impede the training of deep learning networks for pose estimation are rarely discussed in the literature. To cope w…
6D Pose EstimationA new trigonometric kernel function for support vector machine
In the last few years, various types of machine learning algorithms, such as Support Vector Machine (SVM), Support Vector Regression (SVR), and Non-negative Matrix Factorization (NMF) have been introduced. The kernel app…
ClassificationPositive Trigonometric Polynomials on the Stability of Spatially Interconnected Systems
This paper is devoted to the stability analysis of spatially interconnected systems (SISs) via the sum-of-squares (SOS) decomposition of positive trigonometric polynomials. For each spatial direction of SISs, three types…
Constructive sparse trigonometric approximation for functions with small mixed smoothness
The paper gives a constructive method, based on greedy algorithms, that provides for the classes of functions with small mixed smoothness the best possible in the sense of order approximation error for the $m$-term appro…
LArctan-SKAN: Simple and Efficient Single-Parameterized Kolmogorov-Arnold Networks using Learnable Trigonometric Function
This paper proposes a novel approach for designing Single-Parameterized Kolmogorov-Arnold Networks (SKAN) by utilizing a Single-Parameterized Function (SFunc) constructed from trigonometric functions. Three new SKAN vari…
Computational EfficiencyKolmogorov-Arnold Networks