論文の概要: Roosterize: Suggesting Lemma Names for Coq Verification Projects Using
Deep Learning
- arxiv url: http://arxiv.org/abs/2103.01346v1
- Date: Mon, 1 Mar 2021 23:07:44 GMT
- ステータス: 処理完了
- システム内更新日: 2021-03-03 16:09:51.591803
- Title: Roosterize: Suggesting Lemma Names for Coq Verification Projects Using
Deep Learning
- Title(参考訳): Roosterize: ディープラーニングを用いたCoq検証プロジェクトのためのLemmaネームの提案
- Authors: Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric
- Abstract要約: Coqプロジェクトにおける補題名を自動的に提案する、Roosterizeと呼ばれるツールチェーンをデモします。
Roosterizeは、既存のCoqコードで訓練されたニューラルネットワークモデルを利用しており、命名規則の手動仕様を避けている。
評価の結果,roosterizeは補題名を提案するための強力なベースラインを実質的に上回っていることがわかった。
- 参考スコア(独自算出の注目度): 26.226590272852274
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Naming conventions are an important concern in large verification projects
using proof assistants, such as Coq. In particular, lemma names are used by
proof engineers to effectively understand and modify Coq code. However,
providing accurate and informative lemma names is a complex task, which is
currently often carried out manually. Even when lemma naming is automated using
rule-based tools, generated names may fail to adhere to important conventions
not specified explicitly. We demonstrate a toolchain, dubbed Roosterize, which
automatically suggests lemma names in Coq projects. Roosterize leverages a
neural network model trained on existing Coq code, thus avoiding manual
specification of naming conventions. To allow proof engineers to conveniently
access suggestions from Roosterize during Coq project development, we
integrated the toolchain into the popular Visual Studio Code editor. Our
evaluation shows that Roosterize substantially outperforms strong baselines for
suggesting lemma names and is useful in practice. The demo video for Roosterize
can be viewed at: https://youtu.be/HZ5ac7Q14rc.
- Abstract(参考訳): 命名規約は、coqのような証明アシスタントを使用する大規模検証プロジェクトで重要な関心事である。
特に、補題名は証明エンジニアが効果的にCoqコードを理解し、修正するために使用します。
しかし、正確で情報的な補題名を提供することは複雑な作業であり、現在手動で行うことが多い。
規則ベースのツールを使って補題の命名が自動化されたとしても、生成された名前は明示的に指定されていない重要な規約に従わない可能性がある。
Coqプロジェクトにおける補題名を自動的に提案する、Roosterizeと呼ばれるツールチェーンをデモします。
Roosterizeは、既存のCoqコードで訓練されたニューラルネットワークモデルを利用しており、命名規則の手動仕様を避けている。
Coqプロジェクト開発中に証明書エンジニアがRoosterizeから提案に便利にアクセスできるようにするために、ツールチェーンを人気のVisual Studio Codeエディタに統合しました。
評価の結果,Roosterizeは強塩基性に優れており,実際に有用であることが示唆された。
roosterizeのデモビデオは、https://youtu.be/hz5ac7q14rcで見ることができる。
関連論文リスト
- Reproducing, Extending, and Analyzing Naming Experiments [0.23456696459191312]
開発者が名前を選択する方法に関する最近の調査では、異なる開発者が同じオブジェクトに対して与えた名前を収集している。
これにより、これらの名前の多様性と構造の研究が可能となり、名前の作り方に関するモデルの構築が可能となった。
我々はこの研究の様々な部分を3つの独立した実験で再現した。
論文 参考訳(メタデータ) (2024-02-15T15:39:54Z) - Code Reviewer Recommendation Based on a Hypergraph with Multiplex
Relationships [30.74556500021384]
多重関係を持つハイパーグラフを利用する新しいコードレビュアレコメンデーション手法であるMIRRecを提案する。
MIRRecは、プルリクエストと開発者の間で、学位なしのハイパーエッジを使用して、従来のペアワイズ接続を超える高次相関をエンコードする。
MIRRecの有効性を検証するために、GitHubにホストされている10の人気のあるオープンソースプロジェクトからの48,374のプルリクエストからなるデータセットを用いて実験を行った。
論文 参考訳(メタデータ) (2024-01-19T15:25:14Z) - How are We Detecting Inconsistent Method Names? An Empirical Study from
Code Review Perspective [13.585460827586926]
メソッドの適切な命名は、プログラムコードを理解しやすくし、ソフトウェア保守性を高める。
メソッド名の不整合をチェックする自動ツールの開発に多くの研究努力が費やされている。
本研究では,最先端技術が一貫性と一貫性のないメソッド名の検出や推奨にどのように貢献するかを実証研究する。
論文 参考訳(メタデータ) (2023-08-24T10:39:18Z) - CONCORD: Clone-aware Contrastive Learning for Source Code [64.51161487524436]
セルフ教師付き事前トレーニングは、多くのダウンストリームSEタスクに価値のあるジェネリックコード表現を学ぶための牽引役になった。
汎用的な表現学習のために、開発者が日々どのようにコードをコーディングするかは、要因としても不可欠である、と私たちは主張する。
特に,表現空間に良性クローンを近づける自己教師型コントラスト学習戦略であるCONCORDを提案する。
論文 参考訳(メタデータ) (2023-06-05T20:39:08Z) - RefBERT: A Two-Stage Pre-trained Framework for Automatic Rename
Refactoring [57.8069006460087]
本研究では,他のリネーム活動よりも難易度の高い変数名の自動改名について検討する。
変数名に対する名前変更のための2段階事前訓練フレームワークであるRefBERTを提案する。
RefBERTの変数名は既存の手法よりも正確で有意義であることを示す。
論文 参考訳(メタデータ) (2023-05-28T12:29:39Z) - When Counting Meets HMER: Counting-Aware Network for Handwritten
Mathematical Expression Recognition [57.51793420986745]
我々は、手書き数式認識(HMER)のための非従来型ネットワークであるCounting-Aware Network(CAN)を提案する。
シンボルレベルの位置アノテーションを使わずに各シンボルクラスの数を予測できる弱教師付きカウントモジュールを設計する。
HMERのベンチマークデータセットの実験により、エンコーダ・デコーダモデルの予測誤差を修正するために、共同最適化とカウント結果の両方が有用であることが検証された。
論文 参考訳(メタデータ) (2022-07-23T08:39:32Z) - Named Tensor Notation [117.30373263410507]
名前付き軸を持つテンソルの表記法を提案する。
著者、読者、および将来の実装者は、軸の順序を追跡する負担から解放されます。
また、低階テンソル上の操作を高階テンソルに拡張するのも容易である。
論文 参考訳(メタデータ) (2021-02-25T22:21:30Z) - Learning to Format Coq Code Using Language Models [35.21093297227429]
Coqコードは、異なる人々やチームによって異なる方法で書かれる傾向があります。
特に、経験の浅いユーザでさえ、標準ライブラリと普通のLtacを使って、頂点を区別することができる。
Coqの美容整形器のようなルールベースのフォーマッターは柔軟性が限られており、所望の規約のごく一部しか取得できない。
論文 参考訳(メタデータ) (2020-06-18T14:46:15Z) - Deep Generation of Coq Lemma Names Using Elaborated Terms [35.21093297227429]
我々はCoqプロジェクトのための新しい生成モデルを提案し、補題名を提案する。
マルチインプットニューラルネットワークをベースとした当社のモデルは,コクのレキサートケンからの構文情報と意味情報をレムマ文で活用する最初のモデルです。
以上の結果から,Roosterizeは補題名を提案するベースラインを大幅に上回ることがわかった。
論文 参考訳(メタデータ) (2020-04-16T16:54:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。