arXiv:2410.15756v2 宣布类型: replace-cross 摘要：确保正确性对于代码生成至关重要。正式验证提供了终极的正确性保证，但需要大量的人力在证明构建方面进行工作，因此迫切需要自动化工具。主要障碍在于数据的严重缺乏——为大型语言模型（LLMs）训练的代码片段比人工撰写的证明要少得多。在本文中，我们介绍了SAFE，这是一个框架，它克服了人工撰写的证明不足的问题，以实现对Rust代码自动证明的生成。SAFE 建立了一个自演化循环，其中数据合成和微调协作以增强模型能力，利用符号验证器的最终力量来区分正确的证明和错误的证明。SAFE 还重新利用了大量合成的错误证明来训练微调模型的自我修复能力，使其能够根据验证器的反馈修复错误的证明。与GPT-4o相比，SAFE 在效率和精确性方面表现出优越性。通过成千上万的合成证明和自我修复机制，我们使最初不了解形式验证的开源模型能够自动为Rust代码编写证明。这一进展导致性能有了显著提升，在由人类专家设计的一个基准测试中，实现了52.52%的准确率，这比GPT-4o的14.39%有了显著的提高。