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

• URL: http://arxiv.org/abs/2501.05252v1
• Date: Thu, 09 Jan 2025 14:03:35 GMT
• Title: From Scientific Texts to Verifiable Code: Automating the Process with Transformers
• Authors: Changjie Wang, Mariano Scazzariello, Marco Chiesa,
• Abstract summary: transformers can read research papers that propose algorithms with formal proofs and translate these proofs into verifiable code. We argue that this approach can significantly reduce the barrier to formal verification.
• Score: 2.536225150399618
• License:
• 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.

Related papers

• Enhancing Code Consistency in AI Research with Large Language Models and Retrieval-Augmented Generation [0.0]
  This paper presents a novel system designed to verify code implementations against the algorithms and methodologies outlined in corresponding research papers. Our system employs Retrieval-Augmented Generation to extract relevant details from both the research papers and code bases, followed by a structured comparison using Large Language Models.
  arXiv  Detail & Related papers  (2025-02-02T00:35:42Z)
• VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
  VEL is a formal verified EL++ reasoner equipped with machine-checkable correctness proofs. Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.
  arXiv  Detail & Related papers  (2024-12-11T19:17:28Z)
• AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement [25.80131224070207]
  We aim to use formal verification to provide mathematical guarantees that the generated code is correct. generating formally verified code with LLMs is hindered by the scarcity of training data and the complexity of formal proofs. We introduce AlphaVerus, a self-improving framework that bootstraps formally verified code generation.
  arXiv  Detail & Related papers  (2024-12-09T03:22:35Z)
• Analogous Alignments: Digital "Formally" meets Analog [0.0]
  This paper focuses on the pragmatic formal verification of a mixed signal Intellectual Property (IP) that has a combination of digital and analog blocks. Digital and Analog Mixed-Signal (AMS) designs, which are fundamentally different in nature, are integrated seamlessly in a formal verification setup.
  arXiv  Detail & Related papers  (2024-09-23T13:38:31Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  Recent Language Models (LMs) have shown impressive capabilities in generating texts with the knowledge internalized in parameters. We propose to verify the output and the knowledge of the knowledge-augmented LMs with a separate verifier. Our results show that the proposed verifier effectively identifies retrieval and generation errors, allowing LMs to provide more factually correct outputs.
  arXiv  Detail & Related papers  (2023-10-19T15:40:00Z)
• FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarios [87.12753459582116]
  A wider range of tasks now face an increasing risk of containing factual errors when handled by generative models. We propose FacTool, a task and domain agnostic framework for detecting factual errors of texts generated by large language models.
  arXiv  Detail & Related papers  (2023-07-25T14:20:51Z)
• A Simple, Yet Effective Approach to Finding Biases in Code Generation [16.094062131137722]
  This work shows that current code generation systems exhibit undesired biases inherited from their large language model backbones. We propose the "block of influence" concept, which enables a modular decomposition and analysis of the coding challenges.
  arXiv  Detail & Related papers  (2022-10-31T15:06:15Z)
• GERE: Generative Evidence Retrieval for Fact Verification [57.78768817972026]
  We propose GERE, the first system that retrieves evidences in a generative fashion. The experimental results on the FEVER dataset show that GERE achieves significant improvements over the state-of-the-art baselines.
  arXiv  Detail & Related papers  (2022-04-12T03:49:35Z)
• Synthetic Disinformation Attacks on Automated Fact Verification Systems [53.011635547834025]
  We explore the sensitivity of automated fact-checkers to synthetic adversarial evidence in two simulated settings. We show that these systems suffer significant performance drops against these attacks. We discuss the growing threat of modern NLG systems as generators of disinformation.
  arXiv  Detail & Related papers  (2022-02-18T19:01:01Z)
• Evidence-Aware Inferential Text Generation with Vector Quantised Variational AutoEncoder [104.25716317141321]
  We propose an approach that automatically finds evidence for an event from a large text corpus, and leverages the evidence to guide the generation of inferential texts. Our approach provides state-of-the-art performance on both Event2Mind and ATOMIC datasets.
  arXiv  Detail & Related papers  (2020-06-15T02:59:52Z)
• Robustness Verification for Transformers [165.25112192811764]
  We develop the first robustness verification algorithm for Transformers. The certified robustness bounds computed by our method are significantly tighter than those by naive Interval Bound propagation. These bounds also shed light on interpreting Transformers as they consistently reflect the importance of different words in sentiment analysis.
  arXiv  Detail & Related papers  (2020-02-16T17:16:31Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.