論文の概要: Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK

• arxiv url: http://arxiv.org/abs/2502.07728v1
• Date: Tue, 11 Feb 2025 17:42:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-12 14:10:26.127350
• Title: Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK
• Title（参考訳）: Ada/SPARKを用いたソフトウェア検証におけるLCM生成コードの検証
• Authors: Marcos Cramer, Lucian McIntyre,
• Abstract要約: 大規模言語モデル(LLM)は、顕著なコード生成能力を示しているが、生成されたコードの正確性は本質的に信頼できない。 本稿では,ALM生成コードの信頼性を確保するために,形式的ソフトウェア検証,特にAdaのSPARKフレームワークを使用することの実現可能性について検討する。 本稿では,既存のプログラムのSPARKアノテーションを生成するためにLLMを利用するツールであるMarmaraganについて述べる。
• 参考スコア（独自算出の注目度）: 0.4143603294943439
• License:
• Abstract: Large language models (LLMs) have demonstrated remarkable code generation capabilities, but the correctness of the generated code cannot be inherently trusted. This paper explores the feasibility of using formal software verification, specifically the SPARK framework for Ada, to ensure the reliability of LLM-generated code. We present Marmaragan, a tool that leverages an LLM in order to generate SPARK annotations for existing programs, enabling formal verification of the code. The tool is benchmarked on a curated set of SPARK programs, with annotations selectively removed to test specific capabilities. The performance of Marmaragan with GPT-4o on the benchmark is promising, with correct annotations having been generated for 50.7% of the benchmark cases. The results establish a foundation for future work on combining the power of LLMs with the reliability of formal software verification.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、顕著なコード生成能力を示しているが、生成されたコードの正確性は本質的に信頼できない。 本稿では,ALM生成コードの信頼性を確保するために,形式的ソフトウェア検証,特にAdaのSPARKフレームワークを使用することの実現可能性について検討する。 本稿では,既存のプログラムのSPARKアノテーションを生成するためにLLMを利用するツールであるMarmaraganについて述べる。 このツールはSPARKプログラムのキュレートされたセットでベンチマークされており、特定の機能をテストするためにアノテーションを選択的に削除している。 GPT-4oのベンチマークでのマーマラガンのパフォーマンスは有望であり、ベンチマークケースの50.7%で正しいアノテーションが生成されている。 その結果,LSMのパワーと形式的ソフトウェア検証の信頼性の両立に向けた今後の研究の基盤が確立された。

関連論文リスト

• Automatic Generation of Benchmarks and Reliable LLM Judgment for Code Tasks [0.8274693573069442]
  この研究は、自動生成されたベンチマークを利用して、LaaJの実装を生成および評価する方法論を導入する。 ベンチマークは、LaaJの開発と検証と、LaaJを使用してLLMコード関連ソリューションの検証とテストの両方に使用される。 私たちのアプローチは、高品質なコードタスクソリューションの作成を可能にします。
  論文  参考訳（メタデータ） (2024-10-28T14:34:36Z)
• FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware [4.480157114854711]
  FVEvalは,形式的検証(FV)に関わるタスクにおいて,大規模言語モデル(LLM)のパフォーマンスを特徴付ける最初の総合ベンチマークである。 ベンチマークは3つのサブタスクで構成され、異なるレベルでLLM能力を測定する。 本稿では,FVに整合した合成例を生成するための,専門家による検証手法と手法のコレクションについて述べる。
  論文  参考訳（メタデータ） (2024-10-15T21:48:57Z)
• LLM4VV: Exploring LLM-as-a-Judge for Validation and Verification Testsuites [6.796136787585992]
  大規模言語モデル(LLM)は進化し、ソフトウェア開発のランドスケープに大きな革命をもたらしています。 本稿では,ディレクティブプログラミングモデルのコンパイラ実装を評価するために使用されるテストの判定について考察する。
  論文  参考訳（メタデータ） (2024-08-21T15:54:17Z)
• Exploring Automatic Cryptographic API Misuse Detection in the Era of LLMs [60.32717556756674]
  本稿では,暗号誤用の検出において,大規模言語モデルを評価するための体系的評価フレームワークを提案する。 11,940個のLCM生成レポートを詳細に分析したところ、LSMに固有の不安定性は、報告の半数以上が偽陽性になる可能性があることがわかった。 最適化されたアプローチは、従来の手法を超え、確立されたベンチマークでこれまで知られていなかった誤用を明らかにすることで、90%近い顕著な検出率を達成する。
  論文  参考訳（メタデータ） (2024-07-23T15:31:26Z)
• Towards Large Language Model Aided Program Refinement [10.089955747110444]
  プログラムの洗練には、正式なハイレベルな仕様文から実行可能なプログラムへの正当性保存の変換が含まれる。 大型言語モデル(LLM)は、非公式な自然言語仕様から自動コード生成を可能にする。 LLM4PRは,形式的プログラム改善手法と非公式なLCMベースの手法を組み合わせたツールである。
  論文  参考訳（メタデータ） (2024-06-26T04:29:27Z)
• Cycles of Thought: Measuring LLM Confidence through Stable Explanations [53.15438489398938]
  大規模言語モデル(LLM)は、様々なベンチマークで人間レベルの精度に到達し、さらに超えることができるが、不正確な応答における過度な自信は、依然として十分に文書化された障害モードである。 本稿では,LLMの不確実性を測定するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-06-05T16:35:30Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
  大規模言語モデル(LLM)は、知識探索タスクにおける高い性能のため、知識ベースとして扱われてきた。 LLMが実際に正しい答えを連続的に生成する能力をどのように評価するか。 LLMの信頼性を直接測定するための新しい指標であるMOdel kNowledge relIabiliTy score (MONITOR)を提案する。
  論文  参考訳（メタデータ） (2023-10-15T12:40:30Z)
• LLMRec: Benchmarking Large Language Models on Recommendation Task [54.48899723591296]
  推奨領域におけるLarge Language Models (LLMs) の適用について, 十分に検討されていない。 我々は、評価予測、シーケンシャルレコメンデーション、直接レコメンデーション、説明生成、レビュー要約を含む5つのレコメンデーションタスクにおいて、市販のLLMをベンチマークする。 ベンチマークの結果,LLMは逐次的・直接的推薦といった精度に基づくタスクにおいて適度な熟練度しか示さないことがわかった。
  論文  参考訳（メタデータ） (2023-08-23T16:32:54Z)
• The potential of LLMs for coding with low-resource and domain-specific programming languages [0.0]
  本研究は,オープンソースソフトウェアGreetlのハンスル(Hansl)という,econometricスクリプティング言語に焦点を当てたものである。 この結果から, LLMはグレタブルコードの記述, 理解, 改善, 文書化に有用なツールであることが示唆された。
  論文  参考訳（メタデータ） (2023-07-24T17:17:13Z)
• 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)

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

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