Despite the vast body of research literature proposing algorithms with formal guarantees, the amount of verifiable code in today's systems remains minimal. This discrepancy stems from the inherent difficulty of verifying code, particularly due to the time-consuming nature and strict formalism of proof details that formal verification tools require. However, the emergence of transformers in Large Language Models presents a promising solution to this challenge. In this position paper, we believe that transformers have the potential to read research papers that propose algorithms with formal proofs and translate these proofs into verifiable code. We leverage transformers to first build a formal structure of the proof using the original text from the paper, and then to handle the tedious, low-level aspects of proofs that are often omitted by humans. We argue that this approach can significantly reduce the barrier to formal verification. The above idea of reading papers to write verifiable code opens new avenues for automating the verification of complex systems, enabling a future where formally verified algorithms from academic research can more seamlessly transition into real-world software systems, thereby improving code reliability and security.

本研究解决了可验证代码在当前系统中稀缺的问题，揭示了变换器在自动化形式验证中的潜力。通过利用变换器从研究论文中提取形式化证明并转换为可验证代码，可以显著降低形式验证的门槛。该方法有望增强学术研究中的正式验证算法与现实软件系统之间的无缝衔接，从而提高代码的可靠性和安全性。

从科学文本到可验证代码：利用变换器自动化该过程