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

要約

形式的保証のあるアルゴリズムを提案する膨大な研究文献があるにもかかわらず、今日のシステムで検証可能なコードの量は依然として最小限です。
この不一致は、コード検証の本質的な難しさ、特に時間のかかる性質と、正式な検証ツールが必要とする証明の詳細の厳密な形式主義に起因します。
しかし、大規模言語モデルにおけるトランスフォーマーの出現は、この課題に対する有望な解決策を提示します。
このポジションペーパーでは、トランスフォーマーは形式的な証明を伴うアルゴリズムを提案する研究論文を読み、これらの証明を検証可能なコードに変換する可能性があると考えています。
私たちはトランスフォーマーを利用して、最初に論文の元のテキストを使用して証明の正式な構造を構築し、次に人間によって省略されることが多い証明の退屈で低レベルの側面を処理します。
私たちは、このアプローチにより正式な検証に対する障壁を大幅に軽減できると主張します。
論文を読んで検証可能なコードを書くという上記のアイデアは、複雑なシステムの検証を自動化するための新しい道を開き、学術研究から正式に検証されたアルゴリズムをよりシームレスに現実世界のソフトウェア システムに移行できる未来を可能にし、それによってコードの信頼性とセキュリティが向上します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google