論文の概要: Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages

• arxiv url: http://arxiv.org/abs/2406.09757v2
• Date: Tue, 15 Oct 2024 21:44:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-17 13:40:00.214863
• Title: Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages
• Title（参考訳）: 検証対応言語におけるLLM駆動型ユーザインテント形式化の評価
• Authors: Shuvendu K. Lahiri,
• Abstract要約: 本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
• 参考スコア（独自算出の注目度）: 6.0608817611709735
• License:
• Abstract: Verification-aware programming languages such as Dafny and F* provide means to formally specify and prove properties of a program. Although the problem of checking an implementation against a specification can be defined mechanically, there is no algorithmic way of ensuring the correctness of the {\it user-intent formalization for programs}, expressed as a formal specification. This is because intent or requirement is expressed {\it informally} in natural language and the specification is a formal artefact. Despite, the advent of large language models (LLMs) has made tremendous strides bridging the gap between informal intent and formal program implementations recently, driven in large parts by benchmarks and automated metrics for evaluation. Recent work has proposed a framework for evaluating the {\it user-intent formalization} problem for mainstream programming languages~\cite{endres-fse24}. However, such an approach does not readily extend to verification-aware languages that support rich specifications (using quantifiers and ghost variables) that cannot be evaluated through dynamic execution. Previous work also required generating program mutants using LLMs to create the benchmark. We advocate an alternate, perhaps simpler approach of {\it symbolically testing specifications} to provide an intuitive metric for evaluating the quality of specifications for verification-aware languages. We demonstrate that our automated metric agrees closely on a human-labeled dataset of Dafny specifications for the popular MBPP code-generation benchmark, yet demonstrates cases where the human labeling is not perfect. We also outline formal verification challenges that need to be addressed to apply the technique more widely. We believe our work provides a stepping stone to enable the establishment of a benchmark and research agenda for the problem of user-intent formalization for programs.
• Abstract（参考訳）: DafnyやF*のような検証可能なプログラミング言語は、プログラムの特性を正式に指定し、証明する手段を提供する。 仕様書に対して実装をチェックする問題は機械的に定義できるが、形式的な仕様として表されるプログラムのユーザ意図的な形式化の正確性を保証するアルゴリズム的な方法はない。 これは、意図や要求が自然言語で非公式に表現され、仕様は形式的な成果物であるからである。 にもかかわらず、大規模言語モデル(LLM)の出現は、最近、非公式な意図と形式的なプログラム実装のギャップを埋め、ベンチマークと評価のための自動メトリクスによって、大きな部分で推進されている。 近年の研究では、メインストリームプログラミング言語の「it user-intent formalization」問題を評価するためのフレームワークが提案されている。 しかし、このようなアプローチは、動的実行では評価できないリッチな仕様(量化子とゴースト変数)をサポートする検証対応言語に、容易には適用できない。 以前の作業では、ベンチマークを作成するためにLSMを使用してプログラムミュータントを生成する必要があった。 我々は、検証対応言語における仕様の品質を評価するための直感的な指標を提供するために、仕様を象徴的にテストする代替的、おそらくより単純なアプローチを提唱する。 我々は,MBPPコード生成ベンチマークにおけるDafny仕様の人間ラベル付きデータセットに,我々の自動測定値が密接に一致することを実証するが,人間のラベル付けが完璧でないケースを実証する。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。 我々は,プログラムのユーザインテリジェントな形式化の問題に対して,ベンチマークと研究アジェンダの確立を可能にするための一歩として,我々の研究を信じている。

関連論文リスト

• An Agile Formal Specification Language Design Based on K Framework [11.042686307366818]
  本稿では,アジャイル形式仕様言語(ASL)を紹介する。 ASLの設計にはアジャイル設計の原則が組み込まれており、形式仕様の記述をシンプルに、より効率的に、スケーラブルにする。 ASLを検証のために実行可能なK形式仕様言語に変換することのできる仕様翻訳アルゴリズムが開発された。
  論文  参考訳（メタデータ） (2024-04-29T09:00:50Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。 NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
  論文  参考訳（メタデータ） (2024-04-23T01:46:32Z)
• An Empirical Evaluation of Pre-trained Large Language Models for Repairing Declarative Formal Specifications [5.395614997568524]
  本稿では,アロイの宣言的仕様を修復するためのLarge Language Models (LLMs) の能力について,体系的に検討する。 本稿では, 補修エージェントとプロンプトエージェントを組み合わせた, 二重エージェントLLMフレームワークを統合した新しい補修パイプラインを提案する。 本研究は, LLM, 特に GPT-4 変種が, 実行時およびトークン使用率の限界が増大しているにもかかわらず, 修復効率において既存の技術よりも優れていたことを明らかにした。
  論文  参考訳（メタデータ） (2024-04-17T03:46:38Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。 このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。 LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
  論文  参考訳（メタデータ） (2023-11-29T08:29:54Z)
• Quantifying Language Models' Sensitivity to Spurious Features in Prompt Design or: How I learned to start worrying about prompt formatting [68.19544657508509]
  言語モデル(LLM)は、言語技術の基本コンポーネントとして採用されている。 いくつかの広く使われているオープンソースLLMは、数ショット設定でプロンプトフォーマットの微妙な変更に対して非常に敏感であることがわかった。 本稿では,与えられたタスクに対して有効なプロンプトフォーマットのサンプルセットを迅速に評価するアルゴリズムを提案し,モデル重み付けにアクセスせずに期待性能の間隔を報告する。
  論文  参考訳（メタデータ） (2023-10-17T15:03:30Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [3.1143846686797314]
  大規模言語モデル(LLM)を適用するためのフレームワークであるnl2specは、構造化されていない自然言語から正式な仕様を導出する。 本稿では,自然言語におけるシステム要求のあいまいさを検知し,解決する新たな手法を提案する。 ユーザは、これらのサブ翻訳を反復的に追加、削除、編集して、不正なフォーマル化を修正する。
  論文  参考訳（メタデータ） (2023-03-08T20:08:53Z)
• ROSCOE: A Suite of Metrics for Scoring Step-by-Step Reasoning [63.77667876176978]
  大規模言語モデルでは、最終回答を正当化するためにステップバイステップの推論を生成するように促された場合、ダウンストリームタスクの解釈可能性が改善されている。 これらの推論ステップは、モデルの解釈可能性と検証を大幅に改善するが、客観的にそれらの正確性を研究することは困難である。 本稿では、従来のテキスト生成評価指標を改善し拡張する、解釈可能な教師なし自動スコアのスイートであるROSを提案する。
  論文  参考訳（メタデータ） (2022-12-15T15:52:39Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。 自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。 言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
  論文  参考訳（メタデータ） (2022-08-11T17:41:08Z)
• Automatic Extraction of Rules Governing Morphological Agreement [103.78033184221373]
  原文から第一パス文法仕様を抽出する自動フレームワークを開発する。 我々は、世界の多くの言語の文法の中核にあるモルフォシンタクティックな現象である合意を記述する規則の抽出に焦点をあてる。 我々のフレームワークはUniversal Dependenciesプロジェクトに含まれるすべての言語に適用され、有望な結果が得られます。
  論文  参考訳（メタデータ） (2020-10-02T18:31:45Z)

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

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