論文の概要: Towards AI-Assisted Synthesis of Verified Dafny Methods
- arxiv url: http://arxiv.org/abs/2402.00247v1
- Date: Thu, 1 Feb 2024 00:07:23 GMT
- ステータス: 処理完了
- システム内更新日: 2024-02-02 17:00:51.753771
- 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つの事前学習モデルの習熟度を改善する方法を示す。
直接コンテキストレスプロンプト、メソッドとテストケースのシグネチャを含む第2のプロンプト、問題をステップに分解する第3のプロンプトの3つの異なるタイプのプロンプトを使用します。
第3のプロンプトでは、GPT-4は58%のケースで検証された(そして評価された)ダフニー法を生成でき、第1のプロンプトは19%のケースで検証された手法を生成できた。
- 参考スコア（独自算出の注目度）: 1.1128699769026908
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large stochastic 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 when applied to programming,
generating erroneous code. One promising avenue to keep models honest is to
have them generate code in a language that supports formal verification: if and
when that is adopted, the model would provide proof along with the code, and
that proof would be automatically verified. Unfortunately, existing large
language models show a severe lack of proficiency in verified programming
languages. In this paper we demonstrate how to improve two pretrained models'
proficiency in the Dafny verified programming language. Using 178 programming
problems from the MBPP dataset, we prompt two contemporary models (GPT-4 and
PaLM-2) to generate methods in Dafny. We use three different types of prompts:
a direct contextless prompt, a second one that includes a signature of the
method and test cases, and a third one that decomposes the problem into steps
and includes dynamically chosen similar examples. Our results show that GPT-4
is better than PaLM-2, but that, in both models, the third prompt greatly
improves the success of the generation task for the direct prompt. With the
third prompt, GPT-4 was able to generate verified (and human-evaluated) Dafny
methods in 58% of the cases, while the first prompt generated verified (and
human-evaluated) methods in only 19% of the cases. Surprisingly, the second
prompt had the worst performance, with only 10%. One tangible contribution of
our work is a collection of 153 MBPP problems that are implemented and formally
verified in Dafny, 50 of which were written by us and 103 were automatically
synthesized by GPT-4. Additionally, our results demonstrate that the benefits
of formal program verification (proof of correctness) are now within reach...
- Abstract（参考訳）: 大きな確率言語モデルは、プログラミングを含む多くの領域で大きな期待を示します。
約束は簡単にできるが、維持は困難であり、言語モデルはしばしば、プログラミングに適用して誤ったコードを生成するときに約束を守らない。
モデルを正直に保つための有望な方法の1つは、形式的な検証をサポートする言語でコードを生成することである。
残念なことに、既存の大規模言語モデルは、検証済みプログラミング言語の熟練度が極めて低いことを示している。
本稿では,dafny検証プログラム言語における2つの事前学習モデルの習熟度を改善する方法について述べる。
MBPPデータセットから178のプログラミング問題を用いて、2つの現代モデル(GPT-4とPaLM-2)をダフニーで生成する。
直接コンテキストレスプロンプト、メソッドとテストケースのシグネチャを含む第2のプロンプト、問題をステップに分解し動的に選択された同様の例を含む第3のプロンプトの3つの異なるタイプのプロンプトを使用します。
その結果, GPT-4 は PaLM-2 よりも優れていることがわかったが, どちらのモデルにおいても, 3番目のプロンプトは直接プロンプト生成タスクの成功を大幅に改善する。
第3のプロンプトにより、gpt-4は58%のケースで検証済み(かつ評価済み)dafny法を生成でき、第1のプロンプトは19%のケースで検証済み(かつ評価済み)なdafny法を生成できた。
驚いたことに、第2のプロンプトはパフォーマンスが悪く、10%しかなかった。
本研究の顕著な貢献の一つは,Dafnyで実装および正式に検証された153MBPP問題の集合であり,そのうち50は私たちによって書かれ,103は自動的にGPT-4によって合成された。
さらに,形式的プログラム検証(正しさの証明)の利点が限界に達していることを実証した。
関連論文リスト
- Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarsity [0.5370906227996627]
本稿では,プロジェクトレベルの証明指向プログラミングのための合成データ拡張について,生成と修復の両面について紹介する。
本手法は,その言語の習熟度に関する基礎的証明指向プログラミング問題を合成することにより,データの不足に対処する。
我々は,プロジェクトレベルでの証明指向プログラミングにおいて,GPT-4oよりも優れた性能を示すモデルとして,細調整した14BパラメータモデルPoPilotを提案する。
論文 参考訳（メタデータ） (2025-02-17T15:24:11Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
本稿では,オープンソースの大規模言語モデル(LLM)であるGoedel-Proverを紹介する。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。
このデータセットには、Windows、Linux、Python、Firefoxなど、プロダクションシステムで使用されるソフトウェアが含まれている。
我々は,AIを用いてプログラムとその証明をF*で合成し,有望な結果を得る。
論文 参考訳（メタデータ） (2024-05-03T00:14:33Z) - 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) - Prompt Engineering or Fine-Tuning: An Empirical Assessment of LLMs for Code [7.760653867600283]
我々は,基本的なプロンプト,コンテキスト内学習,タスク固有のプロンプトという3つのプロンプト技術戦略を用いて,GPT-4を評価する。
コード要約、生成、翻訳という3つのコード関連タスクに関する17の微調整モデルと比較する。
論文 参考訳（メタデータ） (2023-10-11T00:21:00Z) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。