论文标题
学会证明三角学身份
Learning to Prove Trigonometric Identities
论文作者
论文摘要
用深度学习方法证明自动定理最近引起了注意。在本文中，我们为三角身份构建了一个自动证明系统。我们定义了三角身份的归一化形式，为证明设计一组规则，并提出了一种可以生成理论上无限三角身份的方法。我们的目标不仅是完成证明，而且是在尽可能少的步骤中完成证明。因此，我们设计了一个模型来学习由随机BFS（RBF）生成的证明数据，并且在理论上和实验上证明了该模型在简单的模仿学习后可以优于RBF。通过增强学习进一步改进，我们获得了Autotrig，这可以在几乎与BFS（理论上最短的方法）中为身份提供证明步骤，而时间成本仅为千分之一。此外，Autotrig在合成数据集中还击败Sympy，Matlab和人类，并且在许多概括任务中表现良好。
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.
