論文の概要: Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
- arxiv url: http://arxiv.org/abs/2310.01831v2
- Date: Mon, 15 Apr 2024 23:08:37 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-18 01:59:49.446998
- Title: Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?
- Title(参考訳): 大規模言語モデルは自然言語を形式的手法に変換できるか?
- Authors: Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu K. Lahiri,
- Abstract要約: 大きな言語モデル(LLM)は、プログラマの意図にマッチする仕様への自然言語の意図の翻訳を容易にする可能性がある。
本稿では,プログラムアサーションとして表現された,非公式な自然言語形式的メソッドのポストコンディションにLLMを活用する問題であるnl2postcondについて述べる。
- 参考スコア(独自算出の注目度): 17.03841665553565
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Informal natural language that describes code functionality, such as code comments or function documentation, may contain substantial information about a programs intent. However, there is typically no guarantee that a programs implementation and natural language documentation are aligned. In the case of a conflict, leveraging information in code-adjacent natural language has the potential to enhance fault localization, debugging, and code trustworthiness. In practice, however, this information is often underutilized due to the inherent ambiguity of natural language which makes natural language intent challenging to check programmatically. The emergent abilities of Large Language Models (LLMs) have the potential to facilitate the translation of natural language intent to programmatically checkable assertions. However, it is unclear if LLMs can correctly translate informal natural language specifications into formal specifications that match programmer intent. Additionally, it is unclear if such translation could be useful in practice. In this paper, we describe nl2postcond, the problem of leveraging LLMs for transforming informal natural language to formal method postconditions, expressed as program assertions. We introduce and validate metrics to measure and compare different nl2postcond approaches, using the correctness and discriminative power of generated postconditions. We then use qualitative and quantitative methods to assess the quality of nl2postcond postconditions, finding that they are generally correct and able to discriminate incorrect code. Finally, we find that nl2postcond via LLMs has the potential to be helpful in practice; nl2postcond generated postconditions were able to catch 64 real-world historical bugs from Defects4J.
- Abstract(参考訳): コードコメントや関数ドキュメンテーションなどのコード機能を記述するインフォーマル自然言語には、プログラムの意図に関する重要な情報が含まれている可能性がある。
しかし、プログラムの実装と自然言語のドキュメントが一致しているという保証はない。
衝突の場合、コードに隣接した自然言語で情報を活用することは、フォールトローカライゼーション、デバッグ、コードの信頼性を高める可能性がある。
しかし、実際には、自然言語の本来のあいまいさが、自然言語の意図をプログラム的にチェックすることを困難にしているため、この情報は利用されていないことが多い。
大規模言語モデル(LLM)の創発的能力は、プログラムでチェック可能なアサーションへの自然言語意図の翻訳を促進する可能性がある。
しかし、LLMが非公式な自然言語仕様をプログラマの意図に合う形式仕様に正しく翻訳できるかどうかは不明である。
また、そのような翻訳が実際に有用かは定かではない。
本稿では,Nl2postcondについて述べる。これは,プログラムアサーションとして表現された,非公式な自然言語から形式的なメソッドポストコンディションへの変換にLLMを活用する問題である。
生成したポストコンディションの正しさと識別力を用いて,異なるnl2ポストコンディションアプローチを測定・比較するためのメトリクスを導入,検証する。
次に、定性的かつ定量的な手法を用いて、nl2postcond後条件の質を評価し、それらが一般的に正しく、誤ったコードを識別できることを示す。
最後に、LLMによるnl2postcondは、実際に役立つ可能性があることを発見し、nl2postcond生成されたポストコンドは、Defects4Jから64の実際の歴史的バグをキャッチできた。
関連論文リスト
- Assured Automatic Programming via Large Language Models [8.006578501857447]
我々は,その意図に適合するコードを生成しつつ,プログラマの意図を発見することを目的としている。
本研究の目的は,ユーザ意図の理解を深めることによって,プログラム,仕様,テスト間の一貫性を実現することである。
提案手法によって発見された曖昧な意図が,検証可能な自動生成プログラムの割合をいかに高めるかを示す。
論文 参考訳(メタデータ) (2024-10-24T07:29:15Z) - Towards Large Language Model Aided Program Refinement [10.089955747110444]
プログラムの洗練には、正式なハイレベルな仕様文から実行可能なプログラムへの正当性保存の変換が含まれる。
大型言語モデル(LLM)は、非公式な自然言語仕様から自動コード生成を可能にする。
LLM4PRは,形式的プログラム改善手法と非公式なLCMベースの手法を組み合わせたツールである。
論文 参考訳(メタデータ) (2024-06-26T04:29:27Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳(メタデータ) (2024-06-14T06:52:08Z) - 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) - 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) - How Proficient Are Large Language Models in Formal Languages? An In-Depth Insight for Knowledge Base Question Answering [52.86931192259096]
知識ベース質問回答(KBQA)は,知識ベースにおける事実に基づいた自然言語質問への回答を目的としている。
最近の研究は、論理形式生成のための大規模言語モデル(LLM)の機能を活用して性能を向上させる。
論文 参考訳(メタデータ) (2024-01-11T09:27:50Z) - Language Models as Inductive Reasoners [125.99461874008703]
本稿では,帰納的推論のための新しいパラダイム(タスク)を提案し,自然言語の事実から自然言語規則を誘導する。
タスクのための1.2kルールファクトペアを含むデータセットDEERを作成し,ルールと事実を自然言語で記述する。
我々は、事前訓練された言語モデルが自然言語の事実から自然言語規則をいかに誘導できるかを、初めてかつ包括的な分析を行う。
論文 参考訳(メタデータ) (2022-12-21T11:12:14Z) - Python Code Generation by Asking Clarification Questions [57.63906360576212]
本稿では,この課題に対して,より斬新で現実的なセットアップを導入する。
我々は、自然言語記述の過小評価は、明確化を問うことで解決できると仮定する。
我々は、生成した合成明確化質問と回答を含む自然言語記述とコードのペアを含む、CodeClarQAという新しいデータセットを収集し、導入する。
論文 参考訳(メタデータ) (2022-12-19T22:08:36Z) - Transparency Helps Reveal When Language Models Learn Meaning [71.96920839263457]
合成データを用いた体系的な実験により,すべての表現が文脈に依存しない意味を持つ言語では,自己回帰型とマスキング型の両方の言語モデルが,表現間の意味的関係をエミュレートする。
自然言語に目を向けると、特定の現象(参照不透明さ)による実験は、現在の言語モデルが自然言語の意味論をうまく表現していないという証拠を増大させる。
論文 参考訳(メタデータ) (2022-10-14T02:35:19Z) - Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。
自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。
言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
論文 参考訳(メタデータ) (2022-08-11T17:41:08Z) - Code Comment Inconsistency Detection with BERT and Longformer [9.378041196272878]
ソースコードの自然言語記述であるコメントは、ソフトウェア開発者の間で標準的なプラクティスである。
コメントに付随する修正を加えずにコードを変更すると、コメントとコードの間に矛盾が生じます。
本研究では,自然言語推論(NLI)の文脈における不整合を検出するための2つのモデルを提案する。
論文 参考訳(メタデータ) (2022-07-29T02:43:51Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。