From Scientific Texts to Verifiable Code: Automating the Process with Transformers

TL;DR

This paper explores using transformer-based language models to automatically convert research papers with formal proofs into verifiable code, aiming to bridge the gap between algorithm research and practical implementation.

Contribution

It proposes a novel approach leveraging transformers to interpret formal proofs in research papers and generate verifiable code, reducing manual effort and increasing automation in formal verification.

Findings

Transformers can extract formal proof structures from research texts.

The approach can automate parts of the proof-to-code translation process.

Potential to improve the integration of verified algorithms into real-world systems.

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.