Research On Formal Automatic Proof For High Order Logic

In recent years,the credibility of software systems has become one of the key fac-tors for the normal operation of a country's economy.As an effective means to ensure the safety of software systems,formal methods are based on mathematical logic and use protocols,modeling,and verification to verify the reliability of software.Com pared with first-order logic,higher-order logic accepts predicates as parameters,has strong descriptive ability,and is easier to complete the construction of complex soft ware models.In traditional high-level logic proof tools,manual theorem proof methods are mainly used,which is difficult to learn and high labor costs.Therefore,some re searchers have proposed an automated proof method that integrates technology such as pattern matching and machine learning.But these works have the problem of state search explosion in the process of proving the theorem,the verification efficiency is low and the cost is high.In this paper,combined with the proof aid tool Coq,the key technology of syntax tree search in the theorem proof process is studied,and a dynamic search framework based on reinforcement learning Deep Q Network(DQN)is proposed to improve the efficiency of automatic proof.The main works of this paper are as follows:1.Command generation technology based on attention mechanism.In order to predict the commands(strategies and parameters)in the theorem prov-ing process,this paper combines Gated Recurrent Unit(GRU)?Long Short-Term Mem-ory Network(LSTM)and other deep learning networks to design a formal command prediction technology.The traditional command generation method has problems such as inflexible command generation and low accuracy.This article effectively extracts the information in the theorem,constructs a vector based on the three characteristics of the proof goal,the context premise and the current strategy,and designs the strategy and parameters separately Corresponding prediction model.In the training process,the model combines the attention mechanism to capture important information and reduce the interference of useless information.The experimental results show that the proof command predicted by the model in this paper is higher than the existing work in terms of accuracy.2.The theorem syntax tree search technology oriented to higher-order logic.In order to solve the problem of the explosion of search space in the theorem proving process,this paper combines the reinforcement learning DQN and proposes a theorem proving framework based on dynamic strategy.Compared with supervised learning,this method does not require data set for neural network training.DQN can automatically optimize the current selection,find the correct proof path,and complete the proof theorem.In order to abstract the complex proof process into a simple and easy to interact process,this paper saves the extracted target and context information in the nodes of the theorem tree for DQN to learn.In this paper,a one-hot encoding is de-signed to solve the problem that the current proof state is difficult to extract into feature vectors.In addition,this paper designs a detection algorithm to prevent the DQN algo-rithm from generating loops in the process of searching the theorem tree and avoid the failure of the proof.Experiments in the formal project CompCert show that the success rate of this work proof theorem has reached 14.5%.