論文の概要: 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で見ることができる。

関連論文リスト

• CoqPilot, a plugin for LLM-based generation of proofs [0.0]
  CoqPilotは、Coq証明の記述を自動化するために設計されたVS Codeエクステンションである。 プラグインは、Coqファイルの許容戦術でマークされた証明の一部を収集する。 LLMと非機械学習法を組み合わせて、ホールの証明候補を生成する。
  論文  参考訳（メタデータ） (2024-10-25T14:57:29Z)
• CoqPyt: Proof Navigation in Python in the Era of LLMs [5.029445580644576]
  本稿では,Coq証明アシスタントと対話するPythonツールであるCoqPytについて述べる。 CoqPytは、リッチな前提データの抽出など、新しい機能を提供することで、他のCoq関連のツールを改善している。
  論文  参考訳（メタデータ） (2024-05-07T12:50:28Z)
• 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)
• Generation Probabilities Are Not Enough: Uncertainty Highlighting in AI Code Completions [54.55334589363247]
  本研究では,不確実性に関する情報を伝達することで,プログラマがより迅速かつ正確にコードを生成することができるかどうかを検討する。 トークンのハイライトは、編集される可能性が最も高いので、タスクの完了が早くなり、よりターゲットを絞った編集が可能になることがわかりました。
  論文  参考訳（メタデータ） (2023-02-14T18:43:34Z)
• 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)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。