Abstract:With the continuous increase in software scale, software security faces increasingly severe challenges. As an effective means of detecting software system security, formal proof aims to use mathematical methods to complete rigorous verification of software attributes. Commonly used formal proof methods prove theorems with pattern matching, which, however, suffer from defects such as incomplete strategy generation. This study proposes a command prediction framework based on the attention mechanism. It combines long short-term memory (LSTM) with Coq to predict the strategies and parameters during theorem proving. The experimental results show that the model proposed in this study is superior to existing ones in the accuracy of command generation (the accuracy of command prediction is 28.31% in this paper).