Topic

Automated Formal Verification and Trusted Code Generation

In recent years, large language models have demonstrated excellent code generation capabilities. However, big models do not guarantee the accuracy of generated code, especially for more complex algorithmic implementations or engineering code, and it is often difficult to generate the correct program in a single attempt. In order to solve this problem, the report will introduce how to introduce program testing and formal verification in software engineering in the era of big models, and leverage the powerful generative capabilities of big models to, on the one hand, allow big models to self-validate and thus improve the credibility of code generation. On the other hand, the report will focus on how to automate the complex formal verification process using big models to verify code reliability from the perspective of theoretical proofs. 1. previous work has utilized the multi-perspective self-consistency of the model to improve the credibility of code generation by introducing testing and validation 2. advantages and challenges of formal verification for trustworthy code generation 3. Self-evolution of large language models for automated formal verification using data synthesis