論文の概要: Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models

• arxiv url: http://arxiv.org/abs/2412.10483v1
• Date: Fri, 13 Dec 2024 10:36:18 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-17 14:02:22.172835
• Title: Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models
• Title（参考訳）: 大規模言語モデルを用いた複雑プログラムの自動ループ不変生成の実現
• Authors: Ruibang Liu, Guoqiang Li, Minyu Chen, Ling-I Wu, Jingyu Ke,
• Abstract要約: ACInvは、自動複雑プログラムループ不変生成ツールである。 静的解析とLLM(Large Language Models)を組み合わせることで、適切なループ不変量を生成する。 我々はACInvの実験を行い、ACInvはデータ構造を持つデータセットにおいて、以前のツールよりも優れていたことを示した。
• 参考スコア（独自算出の注目度）: 2.243213786359577
• License:
• Abstract: Automated program verification has always been an important component of building trustworthy software. While the analysis of real-world programs remains a theoretical challenge, the automation of loop invariant analysis has effectively resolved the problem. However, real-world programs that often mix complex data structures and control flows pose challenges to traditional loop invariant generation tools. To enhance the applicability of invariant generation techniques, we proposed ACInv, an Automated Complex program loop Invariant generation tool, which combines static analysis with Large Language Models (LLMs) to generate the proper loop invariants. We utilize static analysis to extract the necessary information for each loop and embed it into prompts for the LLM to generate invariants for each loop. Subsequently, we employ an LLM-based evaluator to assess the generated invariants, refining them by either strengthening, weakening, or rejecting them based on their correctness, ultimately obtaining enhanced invariants. We conducted experiments on ACInv, which showed that ACInv outperformed previous tools on data sets with data structures, and maintained similar performance to the state-of-the-art tool AutoSpec on numerical programs without data structures. For the total data set, ACInv can solve 21% more examples than AutoSpec and can generate reference data structure templates.
• Abstract（参考訳）: プログラムの自動検証は、信頼できるソフトウェアを構築する上で、常に重要なコンポーネントである。 実世界のプログラムの分析は理論的な課題であるが、ループ不変解析の自動化はこの問題を効果的に解決した。 しかし、複雑なデータ構造と制御フローを混在させる現実世界のプログラムは、従来のループ不変生成ツールに課題をもたらす。 そこで我々は,自動複雑プログラムループ不変生成ツールACInvを提案し,静的解析をLLM(Large Language Models)と組み合わせ,適切なループ不変を生成する。 静的解析を用いて各ループに必要な情報を抽出し、LLMが各ループの不変量を生成するプロンプトに埋め込む。 その後、LLMに基づく評価器を用いて、生成した不変量を評価し、それらの正しさに基づいてそれらを強化、弱化、あるいは拒絶することにより精製し、最終的に強化された不変量を得る。 我々はACInvの実験を行い、ACInvはデータ構造を持つデータセット上で過去のツールよりも優れており、データ構造を持たない数値プログラム上での最先端ツールAutoSpecと類似した性能を維持した。 データセット全体について、ACInvはAutoSpecよりも21%多くのサンプルを解決し、参照データ構造テンプレートを生成することができる。

関連論文リスト

• An Empirical Study on Self-correcting Large Language Models for Data Science Code Generation [1.335664823620186]
  大規模言語モデル(LLM)は最近、ソフトウェア工学のタスクに多くの応用を進歩させた。 CoT-SelfEvolveは、自己修正プロセスを通じて、反復的かつ自動的にコードを洗練する。
  論文  参考訳（メタデータ） (2024-08-28T09:19:09Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• Planning, Creation, Usage: Benchmarking LLMs for Comprehensive Tool Utilization in Real-World Complex Scenarios [93.68764280953624]
  UltraToolは、ツール利用におけるLarge Language Modelsの能力を改善し評価するために設計された、新しいベンチマークである。 現実の複雑さを強調し、効果的な問題解決のために正確で多段階の計画を必要とする。 UltraToolの重要な特徴は、ツールの使用前に発生する自然言語による計画の独立した評価である。
  論文  参考訳（メタデータ） (2024-01-30T16:52:56Z)
• AutoAct: Automatic Agent Learning from Scratch for QA via Self-Planning [54.47116888545878]
  AutoActはQAのための自動エージェント学習フレームワークである。 大規模アノテートデータやクローズドソースモデルからの合成計画軌道は依存していない。
  論文  参考訳（メタデータ） (2024-01-10T16:57:24Z)
• Finding Inductive Loop Invariants using Large Language Models [14.846222005558666]
  帰納ループ不変量を見つけることは決定不可能な問題である。 実用化に向けた長い研究の歴史にもかかわらず、解決された問題には程遠い。 本稿では,新たなソリューションを提供する上での大規模言語モデルの有用性について検討する。
  論文  参考訳（メタデータ） (2023-11-14T06:58:09Z)
• Time-LLM: Time Series Forecasting by Reprogramming Large Language Models [110.20279343734548]
  時系列予測は多くの実世界の力学系において重要な意味を持つ。 時系列予測のための大規模言語モデルを再利用するための再プログラミングフレームワークであるTime-LLMを提案する。 Time-LLMは、最先端の特殊な予測モデルよりも優れた、強力な時系列学習者である。
  論文  参考訳（メタデータ） (2023-10-03T01:31:25Z)
• Transformers as Statisticians: Provable In-Context Learning with In-Context Algorithm Selection [88.23337313766353]
  この研究はまず、変換器がICLを実行するための包括的な統計理論を提供する。 コンテクストにおいて、トランスフォーマーは、幅広い種類の標準機械学習アルゴリズムを実装可能であることを示す。 エンフィングル変換器は、異なるベースICLアルゴリズムを適応的に選択することができる。
  論文  参考訳（メタデータ） (2023-06-07T17:59:31Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)
• TSGM: A Flexible Framework for Generative Modeling of Synthetic Time Series [61.436361263605114]
  時系列データは、研究者と産業組織間のデータの共有を妨げるため、しばしば不足または非常に敏感である。 本稿では,合成時系列の生成モデリングのためのオープンソースフレームワークである時系列生成モデリング(TSGM)を紹介する。
  論文  参考訳（メタデータ） (2023-05-19T10:11:21Z)
• Modelling Concurrency Bugs Using Machine Learning [0.0]
  このプロジェクトは、一般的な機械学習アプローチと最近の機械学習アプローチを比較することを目的としている。 我々は、実生活(同時)プログラムをシミュレートする範囲で生成する合成データセットを定義する。 各種機械学習モデルモデルの基本的な限界に関する仮説を定式化する。
  論文  参考訳（メタデータ） (2023-05-08T17:30:24Z)
• Synthetic Datasets for Neural Program Synthesis [66.20924952964117]
  本稿では,プログラムと仕様の両方で合成データ分布のバイアスを制御し,評価するための新しい手法を提案する。 そこで我々は,Karel DSLと小さなCalculator DSLを用いて,これらの分布上でのディープネットワークのトレーニングにより,分散一般化性能が向上することが実証された。
  論文  参考訳（メタデータ） (2019-12-27T21:28:10Z)

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

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