From Scientific Texts to Verifiable Code: Automating the Process with Transformers
Changjie Wang, Mariano Scazzariello, Marco Chiesa
TL;DR
The paper tackles the challenge of converting research-proposed algorithms with formal guarantees into verifiable code, a task hindered by the heavy, low-level nature of formal verification. It proposes a two-stage, transformer-assisted pipeline: first translate human proofs into high-level verification code skeletons, then autonomously generate the necessary low-level proofs, leveraging the strengths of modern LLMs. A prototype system, Prometheus, demonstrates this approach on graph-theoretic lemmas, achieving superior success rates over zero-shot baselines by separating skeleton creation from low-level proof synthesis. If scalable, this method could automate verification for decades of scholarly work, enhancing software reliability and security, though challenges remain in automated specification generation and full automation of complex proofs.
Abstract
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.