論文の概要: Dafny as Verification-Aware Intermediate Language for Code Generation

• arxiv url: http://arxiv.org/abs/2501.06283v1
• Date: Fri, 10 Jan 2025 17:23:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-14 14:29:57.235424
• Title: Dafny as Verification-Aware Intermediate Language for Code Generation
• Title（参考訳）: コード生成用中間言語としてのダニー
• Authors: Yue Chen Li, Stefan Zetzsche, Siva Somayyajula,
• Abstract要約: 大規模言語モデル(LLM)は、自然言語プロンプトからソースコードを生成する。 その制限の1つは、生成したコードが正しいようにユーザに提示されているにもかかわらず、時に故障する可能性があることである。 ユーザがLSMをガイドして,まず不透明な中間表現を生成することを,検証対応言語であるDafnyで提案する。 正しいDafnyプログラムはターゲット言語にコンパイルされ、ユーザに返される。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: Using large language models (LLMs) to generate source code from natural language prompts is a popular and promising idea with a wide range of applications. One of its limitations is that the generated code can be faulty at times, often in a subtle way, despite being presented to the user as correct. In this paper, we explore ways in which formal methods can assist with increasing the quality of code generated by an LLM. Instead of emitting code in a target language directly, we propose that the user guides the LLM to first generate an opaque intermediate representation, in the verification-aware language Dafny, that can be automatically validated for correctness against agreed on specifications. The correct Dafny program is then compiled to the target language and returned to the user. All user-system interactions throughout the procedure occur via natural language; Dafny code is never exposed. We describe our current prototype and report on its performance on the HumanEval Python code generation benchmarks.
• Abstract（参考訳）: 自然言語プロンプトからソースコードを生成するために大きな言語モデル(LLM)を使用することは、幅広いアプリケーションで人気があり有望なアイデアである。 その制限の1つは、生成されたコードが時々、しばしば微妙な方法で失敗する可能性があることである。 本稿では,LLMが生成するコードの品質向上に有効な形式的手法を提案する。 対象言語に直接コードを出力する代わりに,ユーザがLSMをガイドしてまず不透明な中間表現を生成することを提案する。 正しいDafnyプログラムはターゲット言語にコンパイルされ、ユーザに返される。 プロシージャ全体のユーザシステム間のインタラクションは、自然言語を介して行われる。 我々は現在のプロトタイプを説明し、HumanEval Pythonコード生成ベンチマークのパフォーマンスについて報告する。

関連論文リスト

• Effective LLM-Driven Code Generation with Pythoness [0.0]
  Pythonessは、大きな言語モデル(LLM)を使用したコード生成のための組み込みドメイン固有言語である。 Pythonessでは、関数やクラス、プログラム全体を記述する際に、開発者は振る舞い仕様のレベルで動作します。 Pythonessは、テストとコード生成の組み合わせをうまく利用して、仕様のみよりも高品質なコードを生成することができることを示す。
  論文  参考訳（メタデータ） (2025-01-03T23:14:46Z)
• Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages [21.18996339478024]
  SPEAC(emphsynthetic programming elicitation and compilation)を紹介する。 SPEACは、より頻繁に、意味的正しさを犠牲にすることなく、構文的に正しいプログラムを生成する。 UCLID5形式検証言語のケーススタディにおいて,SPEACの性能を実証的に評価した。
  論文  参考訳（メタデータ） (2024-06-05T22:16:19Z)
• Decoding at the Speed of Thought: Harnessing Parallel Decoding of Lexical Units for LLMs [57.27982780697922]
  大規模言語モデルは、自然言語の理解と生成において例外的な能力を示した。 しかし、それらの生成速度は、その復号過程の本質的にシーケンシャルな性質によって制限される。 本稿では,データ駆動方式で実装された新しいデコーディング手法であるLexical Unit Decodingを紹介する。
  論文  参考訳（メタデータ） (2024-05-24T04:35:13Z)
• CodeGRAG: Bridging the Gap between Natural Language and Programming Language via Graphical Retrieval Augmented Generation [58.84212778960507]
  我々は,LLMの性能を高めるため,グラフィカル検索拡張コード生成フレームワークであるCodeGRAGを提案する。 CodeGRAGは、制御フローとデータフローに基づいて、コードブロックのグラフィカルなビューを構築し、プログラミング言語と自然言語のギャップを埋める。 ハードメタグラフプロンプト、ソフトプロンプト技術、事前訓練されたGNN専門家の目的の有効性を検証するために、C++言語とピソン言語の両方を含む4つのデータセットで様々な実験と改善が行われた。
  論文  参考訳（メタデータ） (2024-05-03T02:48:55Z)
• Bridging Code Semantic and LLMs: Semantic Chain-of-Thought Prompting for Code Generation [22.219645213202178]
  本稿では,SeCoT というコードの意味情報を抽出する "Semantic Chain-of-Thought" 手法を提案する。 本研究では,SeCoTが最先端の性能を実現し,大規模モデルやコード生成の可能性を大幅に向上させることを示す。
  論文  参考訳（メタデータ） (2023-10-16T05:09:58Z)
• CodeFuse-13B: A Pretrained Multi-lingual Code Large Language Model [58.127534002232096]
  本稿では,オープンソースの事前学習型LLMであるCodeFuse-13Bを紹介する。 英語と中国語の両方のプロンプトによるコード関連のタスク用に特別に設計されている。 CodeFuseは、高品質な事前トレーニングデータセットを利用することで、その効果を達成する。
  論文  参考訳（メタデータ） (2023-10-10T02:38:44Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。 自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。 言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
  論文  参考訳（メタデータ） (2022-08-11T17:41:08Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。 我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2022-03-15T08:25:08Z)
• Incorporating External Knowledge through Pre-training for Natural Language to Code Generation [97.97049697457425]
  オープンドメインコード生成は、自然言語(NL)の意図から汎用プログラミング言語でコードを生成することを目的としている。 オンラインプログラミングQAフォーラムStackOverflowとプログラミング言語APIドキュメントからNL-codeペアを自動的にマイニングする。 評価の結果,2つのソースとデータ拡張と検索ベースデータ再サンプリングを組み合わせることで,コード生成テストベッドCoNaLa上でのBLEUスコアが最大2.2%向上することがわかった。
  論文  参考訳（メタデータ） (2020-04-20T01:45:27Z)

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

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