論文の概要: Deep Generation of Coq Lemma Names Using Elaborated Terms
- arxiv url: http://arxiv.org/abs/2004.07761v2
- Date: Wed, 22 Apr 2020 16:50:17 GMT
- ステータス: 処理完了
- システム内更新日: 2022-12-12 22:05:13.682312
- Title: Deep Generation of Coq Lemma Names Using Elaborated Terms
- Title（参考訳）: 共同用語を用いたCoq Lemmaの名前の深部生成
- Authors: Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
- Abstract要約: 我々はCoqプロジェクトのための新しい生成モデルを提案し、補題名を提案する。
マルチインプットニューラルネットワークをベースとした当社のモデルは,コクのレキサートケンからの構文情報と意味情報をレムマ文で活用する最初のモデルです。
以上の結果から,Roosterizeは補題名を提案するベースラインを大幅に上回ることがわかった。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: 命名、スペーシング、その他の本質的にスタイル的特性のコーディング規約は、開発者が大規模ソフトウェアプロジェクトでソースコードを効果的に理解し、レビューし、修正するために必要である。
coqのような証明アシスタントに基づいた検証プロジェクトの一貫した規約は、プロジェクトのサイズとスコープが大きくなるにつれて重要性が増す。
規約は高コストで文書化と強制が可能だが、新しいアプローチでは大きなコードコーパスに統計的言語モデルを適用することで、javaライクな言語で慣用的な名前を自動的に学習し提案する。
しかし、その強力な言語拡張機能と型チェックと計算の融合により、Coqは自動学習技術の挑戦的なターゲットとなっている。
我々はCoqプロジェクトのための新しい生成モデルを提案し、補題名を提案する。
当社のモデルは、マルチインプットニューラルネットワークを基盤として、coqのlexer(lemma文のトケン)、parser(シンタックスツリー)、kernel(詳細用語)から構文と意味情報を最初に活用したモデルです。
我々はroosterizeというツールチェーンでモデルを実装し、その厳密なコーディング規約で知られている数学的なコンポーネントファミリから派生したコードの大規模なコーパスに適用しました。
以上の結果から,Roosterizeは,マルチインプットモデルと精巧な用語の使用の重要性を強調し,補題名を提案するベースラインを大幅に上回ることを示す。
関連論文リスト
- Supporting Cross-language Cross-project Bug Localization Using Pre-trained Language Models [2.5121668584771837]
既存のテクニックは、アプリケーション固有のデータに依存しているため、一般化性とデプロイメントに苦労することが多い。
本稿では,プロジェクトと言語の境界を超越したバグローカライゼーションのための,PLMに基づく新しい言語モデルを提案する。
論文 参考訳（メタデータ） (2024-07-03T01:09:36Z) - Analyzing the Performance of Large Language Models on Code Summarization [4.6785446727033335]
Llama 2のような大規模言語モデル(LLM)は、自然言語とソースコードの両方を含むタスクで非常によく機能する。
コード要約のタスクにおいて、これらのモデルの性能は、コードとデータセットの対応する自然言語記述との間の重複する(サブワード)トークンの量に依存することがよく示される。
論文 参考訳（メタデータ） (2024-04-10T22:42:18Z) - SparseCoder: Identifier-Aware Sparse Transformer for File-Level Code
Summarization [51.67317895094664]
本稿では,大規模なソースコードプロジェクトの理解と維持を支援するファイルレベルのコード要約について検討する。
長いコードシーケンスを効果的に処理するための識別子対応スパース変換器であるSparseCoderを提案する。
論文 参考訳（メタデータ） (2024-01-26T09:23:27Z) - Bridging Code Semantic and LLMs: Semantic Chain-of-Thought Prompting for
Code Generation [22.219645213202178]
本稿では,SeCoT というコードの意味情報を抽出する "Semantic Chain-of-Thought" 手法を提案する。
本研究では,SeCoTが最先端の性能を実現し,大規模モデルやコード生成の可能性を大幅に向上させることを示す。
論文 参考訳（メタデータ） (2023-10-16T05:09:58Z) - LongCoder: A Long-Range Pre-trained Language Model for Code Completion [56.813974784131624]
LongCoderは自己アテンションにスライディングウィンドウ機構を採用し、グローバルアクセス可能なトークンを2種類導入している。
ブリッジトークンは入力シーケンス全体を通して挿入され、ローカル情報を集約し、グローバルな相互作用を促進する。
メモリトークンは、後で呼び出され、記憶する必要がある重要なステートメントをハイライトするために含まれます。
論文 参考訳（メタデータ） (2023-06-26T17:59:24Z) - Multi-lingual Evaluation of Code Generation Models [82.7357812992118]
本稿では,MBXPとMultilingual HumanEval,MathQA-Xという,評価コード生成モデルに関する新しいベンチマークを提案する。
これらのデータセットは10以上のプログラミング言語をカバーする。
コード生成モデルの性能を多言語で評価することができる。
論文 参考訳（メタデータ） (2022-10-26T17:17:06Z) - ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。
我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
論文 参考訳（メタデータ） (2022-03-15T08:25:08Z) - Multilingual Autoregressive Entity Linking [49.35994386221958]
mGENREはMultilingual Entity Linking問題のためのシーケンス対シーケンスシステムである。
与えられた言語で言及すると、mGENREはターゲットエンティティの名前を左から右へ、トークンごとに予測します。
提案手法の有効性を3つのMELベンチマーク実験を含む広範囲な評価により示す。
論文 参考訳（メタデータ） (2021-03-23T13:25:55Z) - Sequence Model Design for Code Completion in the Modern IDE [3.4824234779710452]
本稿では,すべての有効なキーワードとスコープ内識別子を列挙する静的解析能力と,それらの上に確率分布を配置する言語モデルの能力を組み合わせた,トップk次トークンの予測手法を提案する。
我々のモデルは,文字レベルの入力表現とトークン出力を混合し,語彙外トークン(OOV)を有意に表現し,予測遅延を最小化する。
論文 参考訳（メタデータ） (2020-04-10T22:40:49Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。