論文の概要: Towards Large Language Model Aided Program Refinement

• arxiv url: http://arxiv.org/abs/2406.18616v1
• Date: Wed, 26 Jun 2024 04:29:27 GMT
• ステータス: 処理完了
• システム内更新日: 2024-06-28 18:17:19.705525
• Title: Towards Large Language Model Aided Program Refinement
• Title（参考訳）: プログラムのリファインメントを支援する大規模言語モデルに向けて
• Authors: Yufan Cai, Zhe Hou, Xiaokun Luan, David Miguel Sanan Baena, Yun Lin, Jun Sun, Jin Song Dong,
• Abstract要約: プログラムの洗練には、正式なハイレベルな仕様文から実行可能なプログラムへの正当性保存の変換が含まれる。 大型言語モデル(LLM)は、非公式な自然言語仕様から自動コード生成を可能にする。 LLM4PRは,形式的プログラム改善手法と非公式なLCMベースの手法を組み合わせたツールである。
• 参考スコア（独自算出の注目度）: 10.089955747110444
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Program refinement involves correctness-preserving transformations from formal high-level specification statements into executable programs. Traditional verification tool support for program refinement is highly interactive and lacks automation. On the other hand, the emergence of large language models (LLMs) enables automatic code generations from informal natural language specifications. However, code generated by LLMs is often unreliable. Moreover, the opaque procedure from specification to code provided by LLM is an uncontrolled black box. We propose LLM4PR, a tool that combines formal program refinement techniques with informal LLM-based methods to (1) transform the specification to preconditions and postconditions, (2) automatically build prompts based on refinement calculus, (3) interact with LLM to generate code, and finally, (4) verify that the generated code satisfies the conditions of refinement calculus, thus guaranteeing the correctness of the code. We have implemented our tool using GPT4, Coq, and Coqhammer, and evaluated it on the HumanEval and EvalPlus datasets.
• Abstract（参考訳）: プログラムの洗練には、正式なハイレベルな仕様文から実行可能なプログラムへの正当性保存の変換が含まれる。 プログラムリファインメントに対する従来の検証ツールのサポートは対話性が高く、自動化が欠如している。 一方、大規模言語モデル(LLM)の出現は、非公式な自然言語仕様から自動コード生成を可能にする。 しかし、LLMによって生成されたコードは、しばしば信頼できない。 さらに、LCMが提供する仕様からコードへの不透明な手続きは、制御されていないブラックボックスである。 LLM4PR は,(1) 仕様を事前条件と後条件に変換し,(2) 修正計算に基づいてプロンプトを自動構築し,(3) コード生成のために LLM と対話し,(4) 生成したコードが修正計算の条件を満たすことを検証し,その正確性を保証するツールである。 我々は、GPT4、Coq、Coqhammerを使用してツールを実装し、HumanEvalおよびEvalPlusデータセットで評価した。

関連論文リスト

• Crystal: Illuminating LLM Abilities on Language and Code [58.5467653736537]
  本稿では,自然言語と符号化機能の統合性を高めるための事前学習戦略を提案する。 結果のモデルであるCrystalは、両方のドメインで顕著な能力を示します。
  論文  参考訳（メタデータ） (2024-11-06T10:28:46Z)
• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
  トレーニングデータを自動的に生成する最初のスケーラブルで信頼性の高いAutoIFを導入する。 AutoIFは命令追従データ品質の検証をコード検証に変換する。
  論文  参考訳（メタデータ） (2024-06-19T13:29:53Z)
• 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)
• SpecTra: Enhancing the Code Translation Ability of Language Models by Generating Multi-Modal Specifications [17.60108067953814]
  大規模言語モデル(LLM)は、コード翻訳の自動化作業にますます利用されている。 本稿では,新しい自己整合性フィルタを用いて,まず高品質な仕様を生成するマルチステージアプローチであるSpecTraを提案する。
  論文  参考訳（メタデータ） (2024-05-28T20:48:30Z)
• CodeIP: A Grammar-Guided Multi-Bit Watermark for Large Language Models of Code [56.019447113206006]
  大規模言語モデル(LLM)はコード生成において顕著な進歩を遂げた。 CodeIPは、新しいマルチビット透かし技術で、出所の詳細を保存するために追加情報を埋め込む。 5つのプログラミング言語にまたがる実世界のデータセットで実施された実験は、CodeIPの有効性を実証している。
  論文  参考訳（メタデータ） (2024-04-24T04:25:04Z)
• Grounding Data Science Code Generation with Input-Output Specifications [32.07033683677839]
  大規模言語モデル(LLM)は、最近、自然言語プロンプトからコードを生成する驚くべき能力を示した。 LLMは出力をNLプロンプトとI/O仕様の両方と整合させることが困難である。 I/O 仕様に対する LLM の微調整のための新しい手法である GIFT4Code を提案する。
  論文  参考訳（メタデータ） (2024-02-12T21:32:49Z)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  大型言語モデル(LLM)は、自然言語と形式言語(コード)の組み合わせに基づいて訓練される コードは、標準構文、論理一貫性、抽象化、モジュール性を備えた高レベルの目標を実行可能なステップに変換する。
  論文  参考訳（メタデータ） (2024-01-01T16:51:20Z)
• Function-constrained Program Synthesis [12.55507214959886]
  大規模言語モデル(LLM)は、開発環境で利用可能なすべてのコードを描画することで、リアルタイムでコードを生成することができる。 現在のシステムには効果的なリカバリ方法が欠如しており、ユーザーは十分な解に到達するまで、修正されたプロンプトでモデルを反復的に再起動せざるを得ない。 提案手法は,コード生成を明示的な関数集合に制約し,自動生成されたサブ関数を通じて失敗した試行からのリカバリを可能にする。
  論文  参考訳（メタデータ） (2023-11-27T02:55:34Z)
• Test-Case-Driven Programming Understanding in Large Language Models for Better Code Generation [15.166827643436346]
  muFiXは、大きな言語モデル(LLM)のコード生成性能を改善する新しいプロンプト技術である。 まず、テストケース分析を利用して仕様の理解を得、自己改善プロセスを可能にする。 muFiXはさらに、提供された理解と実際の理解の間のギャップを減らす方向に向けた仕様理解を修正している。
  論文  参考訳（メタデータ） (2023-09-28T02:58:07Z)
• LLM-Pruner: On the Structural Pruning of Large Language Models [65.02607075556742]
  大規模言語モデル(LLM)は、言語理解と生成において顕著な能力を示している。 タスク非依存であり、元のトレーニングデータセットへの依存を最小限に抑えるという2つの制約の範囲内でLLMの圧縮に取り組む。 LLM-Prunerという名前のこの手法は、非臨界結合構造を選択的に除去する構造プルーニングを採用する。
  論文  参考訳（メタデータ） (2023-05-19T12:10:53Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  本稿では,プログラムの実行結果の検証を学習することで,言語からコードへの生成を改善するシンプルな手法であるLEVERを提案する。 具体的には、LLMからサンプリングされたプログラムが、自然言語入力、プログラム自体とその実行結果に基づいて正しいか否かを判定するために、検証者を訓練する。 LEVER はベースコード LLMs (4.6% から 10.9% まで) を継続的に改善し、それらすべてに対して新しい最先端の結果を得る。
  論文  参考訳（メタデータ） (2023-02-16T18:23:22Z)

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

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