論文の概要: Towards AI-Assisted Synthesis of Verified Dafny Methods

• arxiv url: http://arxiv.org/abs/2402.00247v2
• Date: Mon, 10 Jun 2024 20:14:41 GMT
• ステータス: 処理完了
• システム内更新日: 2024-06-12 22:42:29.126988
• Title: Towards AI-Assisted Synthesis of Verified Dafny Methods
• Title（参考訳）: AIによる検証ダニー法の合成に向けて
• Authors: Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, James Noble,
• Abstract要約: 既存の大規模言語モデルでは、検証プログラムの習熟度が著しく低下している。 Dafny検証対応言語における2つの事前学習モデルの習熟度を改善する方法を示す。
• 参考スコア（独自算出の注目度）: 1.0187122752343796
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models show great promise in many domains, including programming. A promise is easy to make but hard to keep, and language models often fail to keep their promises, generating erroneous code. A promising avenue to keep models honest is to incorporate formal verification: generating programs' specifications as well as code so that the code can be proved correct with respect to the specifications. Unfortunately, existing large language models show a severe lack of proficiency in verified programming. In this paper, we demonstrate how to improve two pretrained models' proficiency in the Dafny verification-aware language. Using 178 problems from the MBPP dataset, we prompt two contemporary models (GPT-4 and PaLM-2) to synthesize Dafny methods. We use three different types of prompts: a direct Contextless prompt; a Signature prompt that includes a method signature and test cases, and a Chain of Thought (CoT) prompt that decomposes the problem into steps and includes retrieval augmentation generated example problems and solutions. Our results show that GPT-4 performs better than PaLM-2 on these tasks and that both models perform best with the retrieval augmentation generated CoT prompt. GPT-4 was able to generate verified, human-evaluated, Dafny methods for 58% of the problems, however, GPT-4 managed only 19% of the problems with the Contextless prompt, and even fewer (10%) for the Signature prompt. We are thus able to contribute 153 verified Dafny solutions to MBPP problems, 50 that we wrote manually, and 103 synthesized by GPT-4. Our results demonstrate that the benefits of formal program verification are now within reach of code generating large language models...
• Abstract（参考訳）: 大規模言語モデルは、プログラミングを含む多くの領域で非常に有望である。 約束は簡単ですが、維持するのは難しく、言語モデルは約束を守るのに失敗し、誤ったコードを生成します。 モデルを誠実に保つための有望な方法は、形式的な検証を組み込むことである。プログラムの仕様とコードを生成することで、仕様に関してコードが正しいことを証明できる。 残念ながら、既存の大規模言語モデルは、検証プログラミングの熟練度が著しく低いことを示している。 本稿では,Dafny検証言語における2つの事前学習モデルの習熟度を改善する方法について述べる。 MBPPデータセットから178個の問題を用いて、ダフニー法を合成するために、2つの現代モデル(GPT-4とPaLM-2)を誘導する。 直接コンテキストレスプロンプト、メソッドシグネチャとテストケースを含む署名プロンプト、および問題をステップに分解し、検索拡張生成されたサンプル問題とソリューションを含む思考のチェーンプロンプトの3つの異なるタイプのプロンプトを使用します。 以上の結果から, GPT-4 は PaLM-2 よりも優れた性能を示し, 両モデルとも, CoT プロンプトの検索により高い性能を示した。 GPT-4は58%の精度で検証されたダフニー法を生成できたが、GPT-4はコンテキストレスプロンプトの19%に過ぎず、シグナチャプロンプトの10%も少なかった。 これにより、MBPP問題に153のDafnyソリューション、手書き50、GPT-4で合成された103のソリューションをコントリビュートすることができる。 我々の結果は,プログラム検証の形式的メリットが,大規模言語モデルを生成するコードの範囲内にあることを示している。

関連論文リスト

• Improving Autoformalization using Type Checking [15.58948808529849]
  大規模言語モデルは、自然言語を形式言語に自動翻訳するタスクである、自動形式化の約束を示す。 前回の報告では、Lean 3のCodexを使って達成されたProofNetの公式化ベンチマークのパフォーマンスが16.1%の非公式なステートメントの形式化に成功しただけだった。 解析の結果、これらのモデルの性能は、型チェックを成功させる形式的なステートメントを生成することができないため、大きく制限されていることがわかった。
  論文  参考訳（メタデータ） (2024-06-11T13:01:50Z)
• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
  我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。 我々のデータセットには、約32KのトップレベルF*定義が含まれており、それぞれが型指向プログラムと証明合成の問題を表している。 我々は、AIを用いてプログラムと証明をF*で合成し、有望な結果を得る。
  論文  参考訳（メタデータ） (2024-05-03T00:14:33Z)
• Do Neutral Prompts Produce Insecure Code? FormAI-v2 Dataset: Labelling Vulnerabilities in Code Generated by Large Language Models [3.4887856546295333]
  この研究は、最先端の大規模言語モデル(LLM)の比較分析を提供する。 中立なゼロショットプロンプトを使って単純なCプログラムを書く際に、脆弱性が発生する可能性を分析する。
  論文  参考訳（メタデータ） (2024-04-29T01:24:14Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Leveraging Print Debugging to Improve Code Generation in Large Language Models [63.63160583432348]
  大規模言語モデル(LLM)はコード生成タスクにおいて大きな進歩を遂げた。 しかし、複雑なデータ構造やアルゴリズムによるプログラミング問題に対処する彼らのパフォーマンスは、依然として準最適である。 そこで本稿では,LLM のデバッグを "print debugging" 手法でガイドする,コンテキスト内学習手法を提案する。
  論文  参考訳（メタデータ） (2024-01-10T18:37:59Z)
• Solving Challenging Math Word Problems Using GPT-4 Code Interpreter with Code-based Self-Verification [40.83776920225375]
  OpenAIのGPT-4の最新バージョンは、GPT-4 Code Interpreterと呼ばれ、挑戦的な数学データセットにおいて顕著なパフォーマンスを示している。 新規かつ効果的なUlinecode-based ulineself-ulineverification(CSV)を提案する。 我々はMATHデータセット textbf (53.9% $to 84.3%) で印象的なゼロショット精度を達成した。
  論文  参考訳（メタデータ） (2023-08-15T17:58:45Z)
• FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarios [87.12753459582116]
  より広い範囲のタスクは、生成モデルによって処理されると、事実エラーを含むリスクが増大する。 大規模言語モデルにより生成されたテキストの事実誤りを検出するためのタスクおよびドメインに依存しないフレームワークであるFacToolを提案する。
  論文  参考訳（メタデータ） (2023-07-25T14:20:51Z)
• Teaching Large Language Models to Self-Debug [62.424077000154945]
  大規模言語モデル(LLM)は、コード生成において素晴らしいパフォーマンスを達成した。 本稿では,大規模言語モデルで予測プログラムを数発のデモでデバッグする自己デバッグを提案する。
  論文  参考訳（メタデータ） (2023-04-11T10:43:43Z)
• Ask Me Anything: A simple strategy for prompting language models [24.294416731247427]
  大規模言語モデル(LLM)は、単に自然言語のプロンプトを与えられただけである。 そこで本研究では,質問応答(QA)のプロンプトが,モデル出力を制限するプロンプトよりも優れていることを示す。 収集したプロンプトを適用して、入力の真のラベルに対していくつかのノイズの多い投票を行う。 プロンプトは、非常に異なる精度と複雑な依存関係を持つことができる。
  論文  参考訳（メタデータ） (2022-10-05T17:59:45Z)
• Finetuned Language Models Are Zero-Shot Learners [67.70352207685558]
  命令チューニングは、目に見えないタスクにおけるゼロショット性能を向上することを示す。 137Bパラメータを事前訓練した言語モデルと、自然言語の命令テンプレートを介して言語化された60以上のNLPタスクにチューニングする。 FLANと呼ばれるこの命令調整モデルについて、未知のタスクタイプで評価する。
  論文  参考訳（メタデータ） (2021-09-03T17:55:52Z)
• TuringAdvice: A Generative and Dynamic Evaluation of Language Use [90.3029315711237]
  言語理解モデルのための新しい課題タスクとデータセットであるTuringAdviceを提案する。 現実の人が現在直面している記述された状況を考えると、モデルは自然言語で有益なアドバイスを生成する必要がある。 実証的な結果は、今日のモデルがTuringAdviceで苦労していることを示している。
  論文  参考訳（メタデータ） (2020-04-07T18:00:03Z)

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

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