論文の概要: ClassInvGen: Class Invariant Synthesis using Large Language Models
- arxiv url: http://arxiv.org/abs/2502.18917v1
- Date: Wed, 26 Feb 2025 08:10:57 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-02-27 14:58:11.868571
- Title: ClassInvGen: Class Invariant Synthesis using Large Language Models
- Title（参考訳）: ClassInvGen:大規模言語モデルを用いたクラス不変合成
- Authors: Chuyue Sun, Viraj Agashe, Saikat Chakraborty, Jubi Taneja, Clark Barrett, David Dill, Xiaokang Qiu, Shuvendu K. Lahiri,
- Abstract要約: ClassInvGenは実行可能なクラス不変量とテスト入力を共同生成するメソッドである。
ClassInvGenは、(コードから)仕様を生成するために純粋なLCMベースの技術より優れていることを示す。
また、広く使われている高積分C++内のいくつかのクラスについてケーススタディを行い、実世界のコードに適用可能であることを示す。
- 参考スコア（独自算出の注目度）: 11.374431160444676
- License:
- Abstract: Formal program specifications in the form of preconditions, postconditions, and class invariants have several benefits for the construction and maintenance of programs. They not only aid in program understanding due to their unambiguous semantics but can also be enforced dynamically (or even statically when the language supports a formal verifier). However, synthesizing high-quality specifications in an underlying programming language is limited by the expressivity of the specifications or the need to express them in a declarative manner. Prior work has demonstrated the potential of large language models (LLMs) for synthesizing high-quality method pre/postconditions for Python and Java, but does not consider class invariants. In this work, we describe ClassInvGen, a method for co-generating executable class invariants and test inputs to produce high-quality class invariants for a mainstream language such as C++, leveraging LLMs' ability to synthesize pure functions. We show that ClassInvGen outperforms a pure LLM-based technique to generate specifications (from code) as well as prior data-driven invariant inference techniques such as Daikon. We contribute a benchmark of standard C++ data structures along with a harness that can help measure both the correctness and completeness of generated specifications using tests and mutants. We also demonstrate its applicability to real-world code by performing a case study on several classes within a widely used and high-integrity C++ codebase.
- Abstract（参考訳）: プレコンディション、ポストコンディション、クラス不変の形式的なプログラム仕様は、プログラムの構築とメンテナンスにいくつかの利点がある。
これらは、曖昧な意味からプログラム理解を助けるだけでなく、動的に強制することもできる(あるいは、言語が形式的検証をサポートするときさえも静的に)。
しかし、基礎となるプログラミング言語で高品質な仕様を合成することは、仕様の表現力や宣言的な表現の必要性によって制限される。
これまでの研究は、PythonとJavaの高品質なメソッドプレ/ポスト条件を合成するための大きな言語モデル(LLM)の可能性を示してきたが、クラス不変性は考慮していない。
本稿では,C++ などの主流言語に対して,LLM が純粋関数を合成する能力を活用して高品質なクラス不変量を生成するために,実行可能クラス不変量とテスト入力を共同生成する手法である ClassInvGen について述べる。
そこで本研究では,ClassInvGenの仕様生成技術(コードから)と,ダイコンなどの従来のデータ駆動型不変推論技術に優れた性能を示す。
我々は、テストとミュータントを使用して生成された仕様の正確性と完全性を測定するのに役立つハーネスとともに、標準C++データ構造のベンチマークに貢献する。
また、広く使われている高統合性C++コードベース内のいくつかのクラスについてケーススタディを行い、実世界のコードに適用可能であることを実証した。
関連論文リスト
- Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
形式言語理論は、特に認識者に関するものである。
代わりに、非公式な意味でのみ類似したプロキシタスクを使用するのが一般的である。
ニューラルネットワークを文字列のバイナリ分類器として直接訓練し評価することで、このミスマッチを補正する。
論文 参考訳（メタデータ） (2024-11-11T16:33:25Z) - 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) - Decoding at the Speed of Thought: Harnessing Parallel Decoding of Lexical Units for LLMs [57.27982780697922]
大規模言語モデルは、自然言語の理解と生成において例外的な能力を示した。
しかし、それらの生成速度は、その復号過程の本質的にシーケンシャルな性質によって制限される。
本稿では,データ駆動方式で実装された新しいデコーディング手法であるLexical Unit Decodingを紹介する。
論文 参考訳（メタデータ） (2024-05-24T04:35:13Z) - 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers [5.102523342662388]
3DGenは、AIエージェントを使用して、混合非公式入力を3Dと呼ばれる言語でフォーマット仕様に変換するフレームワークである。
3DGenはテストスイートに準拠した3D仕様を生成する。
論文 参考訳（メタデータ） (2024-04-16T07:53:28Z) - Python Code Generation by Asking Clarification Questions [57.63906360576212]
本稿では,この課題に対して,より斬新で現実的なセットアップを導入する。
我々は、自然言語記述の過小評価は、明確化を問うことで解決できると仮定する。
我々は、生成した合成明確化質問と回答を含む自然言語記述とコードのペアを含む、CodeClarQAという新しいデータセットを収集し、導入する。
論文 参考訳（メタデータ） (2022-12-19T22:08:36Z) - Benchmarking Language Models for Code Syntax Understanding [79.11525961219591]
事前学習された言語モデルは、自然言語処理とプログラム理解の両方において素晴らしい性能を示している。
本研究では,プログラムの構文構造を特定するための,最先端の事前訓練モデルの最初の徹底的なベンチマークを行う。
この結果から,既存のプログラミング言語の事前学習手法の限界が指摘され,構文構造をモデル化することの重要性が示唆された。
論文 参考訳（メタデータ） (2022-10-26T04:47:18Z) - BenchCLAMP: A Benchmark for Evaluating Language Models on Syntactic and
Semantic Parsing [55.058258437125524]
本稿では,制約付きLanguage Model Parsingを評価するベンチマークであるBenchCLAMPを紹介する。
APIを通じてのみ利用可能な2つのGPT-3変種を含む8つの言語モデルをベンチマークする。
実験により,エンコーダ-デコーダ事前学習言語モデルでは,モデル出力が有効であると制約された場合に,構文解析や意味解析の最先端手法を超えることができることがわかった。
論文 参考訳（メタデータ） (2022-06-21T18:34:11Z) - OrdinalCLIP: Learning Rank Prompts for Language-Guided Ordinal
Regression [94.28253749970534]
我々は、リッチなセマンティックCLIP潜在空間からランクの概念を学ぶことを提案する。
OrdinalCLIPは学習可能なコンテキストトークンと学習可能なランク埋め込みで構成されている。
実験結果から,本パラダイムは一般順序回帰タスクにおける競合性能を達成できることが示唆された。
論文 参考訳（メタデータ） (2022-06-06T03:54:53Z) - Synchromesh: Reliable code generation from pre-trained language models [38.15391794443022]
コード生成のための事前学習モデルの信頼性を大幅に向上するフレームワークであるSynchromeshを提案する。
まず、TST(Target similarity Tuning)を使用して、トレーニングバンクから、セマンティックなサンプル選択の新しい方法を使用して、数ショットのサンプルを検索する。
次に、Synchromeshはサンプルをトレーニング済みの言語モデルに供給し、対象言語の有効なプログラムセットに出力を制約する一般的なフレームワークであるConstrained Semantic Decoding (CSD)を使用してプログラムをサンプリングする。
論文 参考訳（メタデータ） (2022-01-26T22:57:44Z) - Code Building Genetic Programming [0.0]
我々は、コード構築遺伝プログラミング(CBGP)を、これを実現するためのフレームワークとして紹介する。
CBGPは、ホスト言語のソースコードに実行または変換できる計算グラフを生成する。
論文 参考訳（メタデータ） (2020-08-09T04:33:04Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。