Applying Autoencoder to Automated Theorem Proving
Wei Y · 2022
Interactive Theorem Provers (ITPs) provide a set of formalized theorems and proof techniques that allow humans to interact with them by choosing problem-solving tactics. The prover continuously transforms the current proof goal according to the input tactics, and finally realizes the proof of the overall goal. In recent years, there have been many attempts to apply deep neural networks to automated theorem proving. Most of them take the current proof goal and premises as input to the neural network and output the proof tactic to choose at the current step. The current context information is usually encoded by a structured neural network. We introduce an autoencoder in the encoding process to encourage the model to extract the semantic-level information of terms and filter out the syntactic-level information. In addition, during the decoding process, we added skip-connection to the attention mechanism, so that the model can obtain the target information more directly. Experiments show that our model accelerates the convergence of the training process, reduces the loss on the validation set, and slightly improves the success rate of theorem proving when using a pure neural network model.