@misc{chen2024automated,
author = {Chen, Tianyu and Lu, Shuai and Lu, Shan and Gong, Yeyun and Yang, Chenyuan and Li, Xuheng and Misu, Md Rakib Hossain and Yu, Hao and Duan, Nan and Cheng, Peng and Yang, Fan and Lahiri, Shuvendu and Xie, Tao and Zhou, Lidong},
title = {Automated Proof Generation for Rust Code via Self-Evolution},
year = {2024},
month = {October},
abstract = {Ensuring correctness is crucial for code generation. Formal verification offers a definitive assurance of correctness, but demands substantial human effort in proof construction and hence raises a pressing need for automation. The primary obstacle lies in the severe lack of data - there is much less proof than code for LLMs to train upon. In this paper, we introduce SAFE, a novel framework that overcomes the lack of human-written proof to enable automated proof generation of Rust code. SAFE establishes a self-evolving cycle where data synthesis and fine-tuning collaborate to enhance the model capability, leveraging the definitive power of a symbolic verifier in telling correct proof from incorrect ones. SAFE also re-purposes the large number of synthesized incorrect proofs to train the self-debugging capability of the fine-tuned models, empowering them to fix incorrect proofs based on the verifier's feedback. SAFE demonstrates superior efficiency and precision compared to GPT-4o. Through tens of thousands of synthesized proofs and the self-debugging mechanism, we improve the capability of open-source models, initially unacquainted with formal verification, to automatically write proof for Rust code. This advancement leads to a significant improvement in performance, achieving a 70.50% accuracy rate in a benchmark crafted by human experts, a significant leap over GPT-4o's performance of 24.46%.},
url = {http://approjects.co.za/?big=en-us/research/publication/automated-proof-generation-for-rust-code-via-self-evolution/},
}