Research On Automatic Theorem Proving Method Based On Context Awareness

Software security has always attracted people's attention,and it is also one of the main research directions in academia.Once the software finds a loophole,it is likely to cause huge losses.For example,in 2009,Air France Flight 447 caused the autopilot to disengage automatically because its sensors could not measure the aircraft's accurate speed,which eventually caused hundreds of deaths.In software development,testing methods are generally used to find vulnerabilities,but this method can only find vulner-abilities and cannot prove that the program has no vulnerabilities.Therefore,software with high security requirements now uses formal theorem proving methods to ensure the security and reliability of the software.The existing theorem proving methods mainly rely on manual manual assistance machines to complete the verification of software security attributes,which is difficult to get started,high cost,and long verification period.This makes it difficult to apply theorem proving methods on a large scale.Although there are some auxiliary tools that can be automatically verified,they are all based on simple logic or first-order logic,and there are few security attributes that can be automatically verified.In addition,the success rate of automatic theorem proving largely depends on the choice of given facts,that is,the need to recommend relevant lemmas.Recommend a more relevant lemma,the higher the probability of successful automatic proof.The more abstract the logic,the easier the modeling,but the more difficult it is to automate the proof.In fact,in recent years,there have been a lot of work on ITP automation technology,but these work have obvious shortcomings,the method used is complicated,but the automation efficiency achieved is very low.In response to the above-mentioned problems and challenges,this paper has carried out the following research work:1.Premise selection technology based on machine learning classification al-gorithm.In order to improve the success rate of Automated theorem provers(ATP)and nteractive theorem provers(ITP)automatic certification,this paper improves and opti-mizes the existing prerequisite selection technology,and designs a combination scheme based on machine learning classification algorithm.The machine learning classifica-tion algorithm is used to train a scoring function.Any formula f can be mapped to a score vector s(f)of size f.The i_th position of the vector represents the lemmal_i and The correlation score of the formula f.Among them,one of the innovations of this scheme is to use Latent Dirichlet Allocation(LDA)to capture the association between symbols and the association between symbols and dependencies,and extract new com-bined features to enhance the performance of K-Nearest Neighbor(K-NN)and Naive Bayes(NB)classifiers.This method is more relevant than the lemma recommended by the existing premise selection algorithm,and can effectively improve the success rate of the automatic proof of the theorem.2.Proof command generation scheme based on context-aware engine.In or-der to improve the efficiency of theorem proving,this paper designs and implements a general automatic proof framework—utoMagic.The framework can automatically try the proof of the theorem with just one click.It contains two core modules,namely the automatic construction of proof command module and the proof path search module.The automatic construction of proof command module uses the context-aware engine and mathematical induction to realize the automatic generation of proof commands,that is,the proof strategy and parameters are selected according to the context information,and the proof commands are automatically constructed.The proof path search module uses the depth-first search algorithm to find the complete proof path according to the generated proof command.