論文の概要: Leveraging Large Language Models to Boost Dafny's Developers Productivity

• arxiv url: http://arxiv.org/abs/2401.00963v1
• Date: Mon, 1 Jan 2024 21:58:13 GMT
• ステータス: 処理完了
• システム内更新日: 2024-01-03 15:12:39.999962
• Title: Leveraging Large Language Models to Boost Dafny's Developers Productivity
• Title（参考訳）: Dafnyの開発者生産性を高めるために大規模言語モデルを活用する
• Authors: \'Alvaro Silva, Alexandra Mendes, Jo\~ao F. Ferreira
• Abstract要約: 本稿では、Dafny開発者の生産性を高めるために、LLM(Large Language Models)を活用することを提案する。 新しいDafnyプラグインは、Dafnyが発見および使用できない関連する補題の提案を生成する。 自動的に証明できない補題に対して、プラグインはまた、付随する計算的証明を提供しようとする。
• 参考スコア（独自算出の注目度）: 49.64902130083662
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-aware languages, such as Dafny, has increased considerably in the last decade, these are still not widely adopted. Often the cost of using such languages is too high, due to the level of expertise required from the developers and challenges that they often face when trying to prove a program correct. Even though Dafny automates a lot of the verification process, sometimes there are steps that are too complex for Dafny to perform on its own. One such case is that of missing lemmas, i.e. Dafny is unable to prove a result without being given further help in the form of a theorem that can assist it in the proof of the step. In this paper, we describe preliminary work on a new Dafny plugin that leverages LLMs to assist developers by generating suggestions for relevant lemmas that Dafny is unable to discover and use. Moreover, for the lemmas that cannot be proved automatically, the plugin also attempts to provide accompanying calculational proofs. We also discuss ideas for future work by describing a research agenda on using LLMs to increase the adoption of verification-aware languages in general, by increasing developers productivity and by reducing the level of expertise required for crafting formal specifications and proving program properties.
• Abstract（参考訳）: 本稿では,Dafny開発者の生産性を高めるためにLLM(Large Language Models)を活用することを提案する。 Dafnyのような検証対応言語の使用は過去10年間で大幅に増加したが、まだ広く採用されていない。 このような言語を使うことのコストが高すぎるのは、開発者に必要な専門知識のレベルと、プログラムを正しく証明しようとするときにしばしば直面する課題のためです。 Dafnyは検証プロセスの多くを自動化するが、時にはDafnyが単独で実行するには複雑すぎるステップもある。 そのような場合の1つは、補題の欠如、すなわちダフニーは、ステップの証明においてそれを助けることができる定理の形で、さらなる助けを与えることなく結果を証明できないことである。 本稿では,新しいdafnyプラグインの予備的な開発について述べる。llmを利用して,dafnyが発見・使用できない関連する補題の提案を生成することで,開発者を支援する。 さらに、自動で証明できない補題に対して、プラグインは付随する計算的証明を提供しようとしている。 また,LCMを用いた検証対応言語の普及に向けた研究課題を述べるとともに,開発者の生産性の向上と,正式な仕様作成やプログラム特性の証明に必要な専門知識のレベルを低下させることにより,今後の作業に向けたアイデアについても論じる。

関連論文リスト

• Large Language Models Can Self-Improve in Long-context Reasoning [100.52886241070907]
  大規模言語モデル(LLM)は、長いコンテキストの処理においてかなりの進歩を遂げているが、それでも長いコンテキストの推論に苦慮している。 我々はこの目的のために特別に設計されたアプローチである我々の提案する。 人類の専門家や 先進的なモデルによるデータに依存する 従来のアプローチと比べて 優れたパフォーマンスを達成しています
  論文  参考訳（メタデータ） (2024-11-12T19:53:00Z)
• SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
  本稿では,コードに基づく批判モデルを用いて,質問コードデータ構築,品質管理,補完的評価などのステップをガイドする新しいパラダイムを提案する。 英語と中国語におけるドメイン内ベンチマークとドメイン外ベンチマークの両方の実験は、提案したパラダイムの有効性を実証している。
  論文  参考訳（メタデータ） (2024-08-28T06:33:03Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• Laurel: Generating Dafny Assertions Using Large Language Models [2.6942525604796366]
  本稿では,大規模な言語モデル(LLM)を用いて,Dafnyプログラムのヘルパーアサーションを自動的に生成するツールであるLaurillを提案する。 Laurelは数回の試行で、必要なヘルパーアサーションの50%以上を生成することができる。
  論文  参考訳（メタデータ） (2024-05-27T03:26:01Z)
• Prompting-based Synthetic Data Generation for Few-Shot Question Answering [23.97949073816028]
  大規模言語モデルを用いることで,複数データセットにおける質問応答性能が向上することを示す。 言語モデルには、一般的な事前学習/微調整スキームを超えて使える貴重なタスク非依存の知識が含まれていることを示唆する。
  論文  参考訳（メタデータ） (2024-05-15T13:36:43Z)
• Optimizing Language Model's Reasoning Abilities with Weak Supervision [48.60598455782159]
  弱い教師付きベンチマークであるtextscPuzzleBen について,25,147 の複雑な質問,回答,人為的合理性からなる。 データセットのユニークな側面は、10,000の未注釈の質問を含めることであり、LLMの推論能力を高めるために、より少ないスーパーサイズのデータを活用することができる。
  論文  参考訳（メタデータ） (2024-05-07T07:39:15Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• FactLLaMA: Optimizing Instruction-Following Language Models with External Knowledge for Automated Fact-Checking [10.046323978189847]
  本稿では,命令追従言語モデルと外部エビデンス検索を併用して,ファクトチェック性能を向上させることを提案する。 我々のアプローチは、与えられた入力クレームに関する適切な証拠を検索するために検索エンジンを活用することである。 そして、この証拠を用いて、LLaMAと呼ばれるオープンソースの言語モデルを作成し、入力クレームの正確性をより正確に予測できるようにする。
  論文  参考訳（メタデータ） (2023-09-01T04:14:39Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)

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

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