論文の概要: Learning to Format Coq Code Using Language Models
- arxiv url: http://arxiv.org/abs/2006.16743v1
- Date: Thu, 18 Jun 2020 14:46:15 GMT
- ステータス: 処理完了
- システム内更新日: 2022-11-19 14:07:17.181514
- Title: Learning to Format Coq Code Using Language Models
- Title（参考訳）: 言語モデルを用いたCoqコードフォーマットの学習
- Authors: Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
- Abstract要約: Coqコードは、異なる人々やチームによって異なる方法で書かれる傾向があります。
特に、経験の浅いユーザでさえ、標準ライブラリと普通のLtacを使って、頂点を区別することができる。
Coqの美容整形器のようなルールベースのフォーマッターは柔軟性が限られており、所望の規約のごく一部しか取得できない。
- 参考スコア（独自算出の注目度）: 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.
- Abstract（参考訳）: レコード宣言の最後の右括弧は別の行にあるべきだろうか?
書き直し戦術の議論は1つの空間で分離すべきだろうか?
coqコードは、異なる人やチームによって異なる方法で書かれる傾向がある。
Coqの言語と表記の表現性、柔軟性、拡張性は、Coqプロジェクトには様々なコーディングスタイルがあり、しばしば命名とフォーマットに関する規約として明示的に文書化されている。
特に、経験の浅いユーザでさえ、標準ライブラリとプレーンLtacを使って、Mathematical Components (MathComp)ライブラリとSSReflectを使って、慣用的なVernacularと区別することができる。
コーディング規約は理解とメンテナンスには重要ですが、文書化と強制にはコストがかかります。
coqのbeautifierのようなルールベースのフォーマッターは柔軟性が限られており、大規模な検証プロジェクトでは望ましい規約のごく一部しかキャプチャしない。
コーパスにおける正規性を捉えるための自然言語処理(NLP)技術のクラスである言語モデルの応用は、この難題に対する解決策となると信じている。
より具体的には、既存のCoqコードから規則を自動的に学習し、それから適切なコンテキストでユーザに対して慣用的なコードを提案するアプローチは、手動のアプローチや静的解析ツールよりも優れていると考えています。
最初のステップとして、coq 8.10の予備実装でcoqファイルで空間フォーマットを学び提案する初期モデルを概説し、4つのコアプロジェクトから164k行のcoqコードからなるmathcomp 1.9.0に基づくコーパスで評価する。
関連論文リスト
- What can Large Language Models Capture about Code Functional Equivalence? [24.178831487657945]
SeqCoBenchは、コード-LLMがコード関数同値をキャプチャする方法を評価するベンチマークである。
我々は,SeqCoBenchにおける意味論的に等価なプログラムと異なるプログラムのペアを識別できるかどうかを,最先端(Code-)LLMで評価する。
論文 参考訳（メタデータ） (2024-08-20T11:19:06Z) - CatCode: A Comprehensive Evaluation Framework for LLMs On the Mixture of
Code and Text [11.872260531587692]
ChatGPTのような大規模言語モデル(LLM)は、コードとテキストの混在を理解し、生成するのに熟練している。
LLMのコーディング能力を包括的に評価できるtextbfCatCode$という自動評価フレームワークを提案する。
論文 参考訳（メタデータ） (2024-03-04T07:26:07Z) - CodeBERTScore: Evaluating Code Generation with Pretrained Models of Code [75.08995072899594]
コード生成のための評価指標であるCodeBERTScoreを提案する。
CodeBERTScoreは生成されたコードの前に入力された自然言語をエンコードする。
CodeBERTScoreは、既存のすべての指標よりも、人間の嗜好と機能的正しさとの相関性が高いことがわかった。
論文 参考訳（メタデータ） (2023-02-10T22:12:05Z) - DocCoder: Generating Code by Retrieving and Reading Docs [87.88474546826913]
コードマニュアルとドキュメントを明示的に活用するアプローチであるDocCoderを紹介します。
我々のアプローチは一般的に、どんなプログラミング言語にも適用でき、基礎となるニューラルモデルとは無関係です。
論文 参考訳（メタデータ） (2022-07-13T06:47:51Z) - InCoder: A Generative Model for Code Infilling and Synthesis [88.46061996766348]
InCoderは、プログラム合成(左から右への生成)と編集(埋め込み)が可能な統合生成モデルである。
InCoderは、許可されたコードの大きなコーパスからコードファイルを生成するように訓練されている。
私たちのモデルは、ゼロショットコードの埋め込みを直接実行できる最初の生成モデルです。
論文 参考訳（メタデータ） (2022-04-12T16:25:26Z) - LAMNER: Code Comment Generation Using Character Language Model and Named
Entity Recognition [0.7894331610810762]
LANguage Model と Named Entity Recognition (LAMNER) を提案する。
LAMNERは、コード構造を効果的に符号化し、コードトークンの構造的特性をキャプチャできるコードコメント生成装置である。
LAMNERや他のベースラインから生成されたコメントを、一般的な4つのメトリクスを持つ人気のあるJavaデータセットで評価する。
論文 参考訳（メタデータ） (2022-04-05T20:53:06Z) - ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。
我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
論文 参考訳（メタデータ） (2022-03-15T08:25:08Z) - CoSQA: 20,000+ Web Queries for Code Search and Question Answering [63.92224685262063]
CoSQAデータセットには、自然言語クエリとコードのペア用の20,604ラベルが含まれている。
本稿では,クエリコードマッチングを強化するために,CoCLRと呼ばれる対照的な学習手法を提案する。
我々は,CodeXGLUEを同じCodeBERTモデルで評価し,CoSQAのトレーニングにより,コード質問応答の精度が5.1%向上したことを示す。
論文 参考訳（メタデータ） (2021-05-27T15:37:21Z) - Deep Generation of Coq Lemma Names Using Elaborated Terms [35.21093297227429]
我々はCoqプロジェクトのための新しい生成モデルを提案し、補題名を提案する。
マルチインプットニューラルネットワークをベースとした当社のモデルは,コクのレキサートケンからの構文情報と意味情報をレムマ文で活用する最初のモデルです。
以上の結果から,Roosterizeは補題名を提案するベースラインを大幅に上回ることがわかった。
論文 参考訳（メタデータ） (2020-04-16T16:54:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。