Deep Generation of Coq Lemma Names Using Elaborated Terms

• URL: http://arxiv.org/abs/2004.07761v2
• Date: Wed, 22 Apr 2020 16:50:17 GMT
• Title: Deep Generation of Coq Lemma Names Using Elaborated Terms
• Authors: Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
• Abstract summary: 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.
• Score: 35.21093297227429
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Coding conventions for naming, spacing, and other essentially stylistic properties are necessary for developers to effectively understand, review, and modify source code in large software projects. Consistent conventions in verification projects based on proof assistants, such as Coq, increase in importance as projects grow in size and scope. While conventions can be documented and enforced manually at high cost, emerging approaches automatically learn and suggest idiomatic names in Java-like languages by applying statistical language models on large code corpora. However, due to its powerful language extension facilities and fusion of type checking and computation, Coq is a challenging target for automated learning techniques. 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 lexer (tokens in lemma statements), parser (syntax trees), and kernel (elaborated terms) for naming; the key insight is that learning from elaborated terms can substantially boost model performance. We implemented our models in a toolchain, dubbed Roosterize, and applied it on a large corpus of code derived from the Mathematical Components family of projects, known for its stringent coding conventions. Our results show that Roosterize substantially outperforms baselines for suggesting lemma names, highlighting the importance of using multi-input models and elaborated terms.

Related papers

• Supporting Cross-language Cross-project Bug Localization Using Pre-trained Language Models [2.5121668584771837]
  Existing techniques often struggle with generalizability and deployment due to their reliance on application-specific data. This paper proposes a novel pre-trained language model (PLM) based technique for bug localization that transcends project and language boundaries.
  arXiv  Detail & Related papers  (2024-07-03T01:09:36Z)
• Analyzing the Performance of Large Language Models on Code Summarization [4.6785446727033335]
  Large language models (LLMs) such as Llama 2 perform very well on tasks that involve both natural language and source code. We show that for the task of code summarization, the performance of these models often depends on the amount of (subword) token overlap between the code and the corresponding natural language descriptions in the dataset.
  arXiv  Detail & Related papers  (2024-04-10T22:42:18Z)
• SparseCoder: Identifier-Aware Sparse Transformer for File-Level Code Summarization [51.67317895094664]
  This paper studies file-level code summarization, which can assist programmers in understanding and maintaining large source code projects. We propose SparseCoder, an identifier-aware sparse transformer for effectively handling long code sequences.
  arXiv  Detail & Related papers  (2024-01-26T09:23:27Z)
• Bridging Code Semantic and LLMs: Semantic Chain-of-Thought Prompting for Code Generation [22.219645213202178]
  This paper proposes the "Semantic Chain-of-Thought" approach to intruduce semantic information of code, named SeCoT. We show that SeCoT can achieves state-of-the-art performance, greatly improving the potential for large models and code generation.
  arXiv  Detail & Related papers  (2023-10-16T05:09:58Z)
• LongCoder: A Long-Range Pre-trained Language Model for Code Completion [56.813974784131624]
  LongCoder employs a sliding window mechanism for self-attention and introduces two types of globally accessible tokens. Bridge tokens are inserted throughout the input sequence to aggregate local information and facilitate global interaction. memory tokens are included to highlight important statements that may be invoked later and need to be memorized.
  arXiv  Detail & Related papers  (2023-06-26T17:59:24Z)
• Multi-lingual Evaluation of Code Generation Models [82.7357812992118]
  We present new benchmarks on evaluation code generation models: MBXP and Multilingual HumanEval, and MathQA-X. These datasets cover over 10 programming languages. We are able to assess the performance of code generation models in a multi-lingual fashion.
  arXiv  Detail & Related papers  (2022-10-26T17:17: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)
• Multilingual Autoregressive Entity Linking [49.35994386221958]
  mGENRE is a sequence-to-sequence system for the Multilingual Entity Linking problem. For a mention in a given language, mGENRE predicts the name of the target entity left-to-right, token-by-token. We show the efficacy of our approach through extensive evaluation including experiments on three popular MEL benchmarks.
  arXiv  Detail & Related papers  (2021-03-23T13:25:55Z)
• Sequence Model Design for Code Completion in the Modern IDE [3.4824234779710452]
  We propose a novel design for predicting top-k next tokens that combines static analysis' ability to enumerate all valid keywords and in-scope identifiers with the ability of a language model to place a probability distribution over them. Our model mixes character-level input representation with token output to represent out-of-vocabulary (OOV) tokens meaningfully and minimize prediction latency.
  arXiv  Detail & Related papers  (2020-04-10T22:40:49Z)

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.