論文の概要: 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を用いた検証対応言語の普及に向けた研究課題を述べるとともに,開発者の生産性の向上と,正式な仕様作成やプログラム特性の証明に必要な専門知識のレベルを低下させることにより,今後の作業に向けたアイデアについても論じる。
関連論文リスト
- Optimizing Language Model's Reasoning Abilities with Weak Supervision [48.60598455782159]
弱い教師付きベンチマークであるtextscPuzzleBen について,25,147 の複雑な質問,回答,人為的合理性からなる。
データセットのユニークな側面は、10,000の未注釈の質問を含めることであり、LLMの推論能力を高めるために、より少ないスーパーサイズのデータを活用することができる。
論文 参考訳(メタデータ) (2024-05-07T07:39:15Z) - Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。
証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。
実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
論文 参考訳(メタデータ) (2024-04-18T22:54:08Z) - Can ChatGPT Support Developers? An Empirical Evaluation of Large Language Models for Code Generation [2.93322471069531]
開発者によるChatGPTとの会話から収集したデータセットであるDevGPTにおける会話の実証分析を行った。
この結果から,LLM生成コードを使用する現在の実践は,高レベルな概念を示すか,ドキュメントに例を示すかのどちらかに制限されていることが示唆された。
論文 参考訳(メタデータ) (2024-02-18T20:48:09Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - Context Matters: Data-Efficient Augmentation of Large Language Models
for Scientific Applications [15.893290942177112]
GPT-4のような大規模言語モデル(LLM)に固有の課題について検討する。
一貫性と意味論的に厳密な方法で誤った回答を提示するLLMの能力は、事実の不正確さの検出を複雑にする。
本研究の目的は,このような誤りの理解と軽減を図り,LCMの精度と信頼性の向上に寄与することである。
論文 参考訳(メタデータ) (2023-12-12T08:43:20Z) - Making Large Language Models Better Data Creators [22.0882632635255]
大規模言語モデル(LLM)はNLPの最先端を著しく進歩させた。
ダウンストリームアプリケーションへのデプロイは、コスト、応答性、コントロール、プライバシとセキュリティに関する懸念のため、依然として難しい。
単一フォーマットの例のみを必要とする統一データ生成パイプラインを提案する。
論文 参考訳(メタデータ) (2023-10-31T01:08:34Z) - FactLLaMA: Optimizing Instruction-Following Language Models with
External Knowledge for Automated Fact-Checking [10.046323978189847]
本稿では,命令追従言語モデルと外部エビデンス検索を併用して,ファクトチェック性能を向上させることを提案する。
我々のアプローチは、与えられた入力クレームに関する適切な証拠を検索するために検索エンジンを活用することである。
そして、この証拠を用いて、LLaMAと呼ばれるオープンソースの言語モデルを作成し、入力クレームの正確性をより正確に予測できるようにする。
論文 参考訳(メタデータ) (2023-09-01T04:14:39Z) - SoTaNa: The Open-Source Software Development Assistant [81.86136560157266]
SoTaNaはオープンソースのソフトウェア開発アシスタントだ。
ソフトウェア工学の分野のための高品質な命令ベースのデータを生成する。
オープンソースの基盤モデルであるLLaMAを強化するためにパラメータ効率のよい微調整アプローチを採用している。
論文 参考訳(メタデータ) (2023-08-25T14:56:21Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳(メタデータ) (2023-06-27T17:05:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。