Learning to Format Coq Code Using Language Models

• URL: http://arxiv.org/abs/2006.16743v1
• Date: Thu, 18 Jun 2020 14:46:15 GMT
• Title: Learning to Format Coq Code Using Language Models
• Authors: Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
• Abstract summary: Coq code tends to be written in distinct manners by different people and teams. In particular, even inexperienced users can distinguish vernacular using the standard library and plain Ltac. Rule-based formatters, such as Coq's beautifier, have limited flexibility and only capture small fractions of desired conventions.
• Score: 35.21093297227429
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Should the final right bracket in a record declaration be on a separate line? Should arguments to the rewrite tactic be separated by a single space? Coq code tends to be written in distinct manners by different people and teams. The expressiveness, flexibility, and extensibility of Coq's languages and notations means that Coq projects have a wide variety of recognizable coding styles, sometimes explicitly documented as conventions on naming and formatting. In particular, even inexperienced users can distinguish vernacular using the standard library and plain Ltac from idiomatic vernacular using the Mathematical Components (MathComp) library and SSReflect. While coding conventions are important for comprehension and maintenance, they are costly to document and enforce. Rule-based formatters, such as Coq's beautifier, have limited flexibility and only capture small fractions of desired conventions in large verification projects. We believe that application of language models - a class of Natural Language Processing (NLP) techniques for capturing regularities in corpora - can provide a solution to this conundrum. More specifically, we believe that an approach based on automatically learning conventions from existing Coq code, and then suggesting idiomatic code to users in the proper context, can be superior to manual approaches and static analysis tools - both in terms of effort and results. As a first step, we here outline initial models to learn and suggest space formatting in Coq files, with a preliminary implementation for Coq 8.10, and evaluated on a corpus based on MathComp 1.9.0 which comprises 164k lines of Coq code from four core projects.

Related papers

• What can Large Language Models Capture about Code Functional Equivalence? [24.178831487657945]
  We introduce SeqCoBench, a benchmark for assessing how Code-LLMs can capture code functional equivalence. We conduct evaluations on state-of-the-art (Code-)LLMs to see if they can discern semantically equivalent or different pairs of programs in SeqCoBench.
  arXiv  Detail & Related papers  (2024-08-20T11:19:06Z)
• CatCode: A Comprehensive Evaluation Framework for LLMs On the Mixture of Code and Text [11.872260531587692]
  Large language models (LLMs) such as ChatGPT are increasingly proficient in understanding and generating a mixture of code and text. We present an automatic evaluation framework called $textbfCatCode$ that can comprehensively assess the coding abilities of LLMs.
  arXiv  Detail & Related papers  (2024-03-04T07:26:07Z)
• CodeBERTScore: Evaluating Code Generation with Pretrained Models of Code [75.08995072899594]
  We propose CodeBERTScore: an evaluation metric for code generation. CodeBERTScore encodes the natural language input preceding the generated code. We find that CodeBERTScore achieves a higher correlation with human preference and with functional correctness than all existing metrics.
  arXiv  Detail & Related papers  (2023-02-10T22:12:05Z)
• DocCoder: Generating Code by Retrieving and Reading Docs [87.88474546826913]
  We introduce DocCoder, an approach that explicitly leverages code manuals and documentation. Our approach is general, can be applied to any programming language, and is agnostic to the underlying neural model.
  arXiv  Detail & Related papers  (2022-07-13T06:47:51Z)
• InCoder: A Generative Model for Code Infilling and Synthesis [88.46061996766348]
  We introduce InCoder, a unified generative model that can perform program synthesis (via left-to-right generation) and editing (via infilling) InCoder is trained to generate code files from a large corpus of permissively licensed code. Our model is the first generative model that is able to directly perform zero-shot code infilling.
  arXiv  Detail & Related papers  (2022-04-12T16:25:26Z)
• LAMNER: Code Comment Generation Using Character Language Model and Named Entity Recognition [0.7894331610810762]
  We present LAnguage Model and Named Entity Recognition (LAMNER) LAMNER is a code comment generator capable of encoding code constructs effectively and capturing the structural property of a code token. We evaluate the generated comments from LAMNER and other baselines on a popular Java dataset with four commonly used metrics.
  arXiv  Detail & Related papers  (2022-04-05T20:53:06Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  We propose a retrieval-augmented code completion framework, leveraging both lexical copying and referring to code with similar semantics by retrieval. We evaluate our approach in the code completion task in Python and Java programming languages, achieving a state-of-the-art performance on CodeXGLUE benchmark.
  arXiv  Detail & Related papers  (2022-03-15T08:25:08Z)
• CoSQA: 20,000+ Web Queries for Code Search and Question Answering [63.92224685262063]
  CoSQA dataset includes 20,604 labels for pairs of natural language queries and codes. We introduce a contrastive learning method dubbed CoCLR to enhance query-code matching. We show that evaluated on CodeXGLUE with the same CodeBERT model, training on CoSQA improves the accuracy of code question answering by 5.1%.
  arXiv  Detail & Related papers  (2021-05-27T15:37:21Z)
• Deep Generation of Coq Lemma Names Using Elaborated Terms [35.21093297227429]
  We present novel generation models for learning and suggesting lemma names for Coq projects. Our models, based on multi-input neural networks, are the first to leverage syntactic and semantic information from Coq's lexertokens in lemma statements. Our results show that Roosterize substantially outperforms baselines for suggesting lemma names.
  arXiv  Detail & Related papers  (2020-04-16T16:54:21Z)

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.