論文の概要: Selene: Pioneering Automated Proof in Software Verification
- arxiv url: http://arxiv.org/abs/2401.07663v1
- Date: Mon, 15 Jan 2024 13:08:38 GMT
- ステータス: 処理完了
- システム内更新日: 2024-01-17 17:11:48.912929
- Title: Selene: Pioneering Automated Proof in Software Verification
- Title(参考訳): Selene: ソフトウェア検証における自動証明のパイオニア化
- Authors: Lichen Zhang, Shuai Lu, Nan Duan
- Abstract要約: 我々は,seL4オペレーティングシステムマイクロカーネルの実際の産業レベルのプロジェクトに基づいて構築された,最初のプロジェクトレベルの自動証明ベンチマークであるSeleneを紹介する。
GPT-3.5-turbo や GPT-4 のような先進的な LLM による実験結果は,自動証明生成領域における大規模言語モデル (LLM) の機能を強調した。
- 参考スコア(独自算出の注目度): 69.7891799471749
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Ensuring correctness is a pivotal aspect of software engineering. Among the
various strategies available, software verification offers a definitive
assurance of correctness. Nevertheless, writing verification proofs is
resource-intensive and manpower-consuming, and there is a great need to
automate this process. We introduce Selene in this paper, which is the first
project-level automated proof benchmark constructed based on the real-world
industrial-level project of the seL4 operating system microkernel. Selene
provides a comprehensive framework for end-to-end evaluation and a lightweight
verification environment. Our experimental results with advanced LLMs, such as
GPT-3.5-turbo and GPT-4, highlight the capabilities of large language models
(LLMs) in the domain of automated proof generation. Additionally, our further
proposed augmentations indicate that the challenges presented by Selene can be
mitigated in future research endeavors.
- Abstract(参考訳): 正確性を保証することは、ソフトウェアエンジニアリングの重要な側面である。
利用可能なさまざまな戦略の中で、ソフトウェア検証は正確性を保証する。
それでも、検証証明を書くことはリソース集約的で人的消費であり、このプロセスを自動化する必要がある。
本稿では,SeL4オペレーティングシステムマイクロカーネルの実際の産業レベルプロジェクトに基づいて構築された,プロジェクトレベルの自動検証ベンチマークであるSeleneを紹介する。
Seleneはエンドツーエンド評価のための包括的なフレームワークと軽量な検証環境を提供する。
GPT-3.5-turbo や GPT-4 のような先進的な LLM による実験結果は,自動証明生成領域における大規模言語モデル (LLM) の機能を強調した。
さらに,セレンによる課題が今後の研究で緩和される可能性が示唆された。
関連論文リスト
- DS-Agent: Automated Data Science by Empowering Large Language Models
with Case-Based Reasoning [60.2784156133412]
大規模言語モデル(LLM)エージェントとケースベース推論(CBR)を利用した新しいフレームワークであるDS-Agentを提案する。
開発段階では、DS-AgentはCBRフレームワークに従い、自動イテレーションパイプラインを構築する。
デプロイメントの段階では、DS-Agentは、シンプルなCBRパラダイムで低リソースのデプロイメントステージを実装し、LCMの基本能力に対する需要を大幅に削減する。
論文 参考訳(メタデータ) (2024-02-27T12:26:07Z) - A Preliminary Study on Using Large Language Models in Software
Pentesting [2.0551676463612636]
大規模言語モデル(LLM)は、セキュリティタスクを自動化するための有望な可能性を提供すると考えられている。
ソフトウェアペンテスティングにおけるLLMの使用について検討し,ソースコード中のソフトウェアセキュリティ脆弱性を自動的に識別する作業を行う。
論文 参考訳(メタデータ) (2024-01-30T21:42:59Z) - Towards Generating Executable Metamorphic Relations Using Large Language
Models [49.632090604977364]
大規模言語モデル(LLM)を用いた要件から実行可能なMRを自動的に抽出する手法を提案する。
提案手法の有効性を評価するため,シーメンス・インダストリー・ソフトウェアと共同で質問紙調査を行った。
論文 参考訳(メタデータ) (2024-01-30T13:52:47Z) - Application of LLM Agents in Recruitment: A Novel Framework for Resume
Screening [0.0]
本稿では,新しい大規模言語モデルに基づくエージェント・フレームワークについて紹介する。
我々のフレームワークは、大規模なデータセットから各履歴を効率的に要約し、評価する能力において、異なる。
その結果,自動再試行フレームワークは従来の手作業よりも11倍高速であることがわかった。
論文 参考訳(メタデータ) (2024-01-16T12:30:56Z) - Self-Evaluation Improves Selective Generation in Large Language Models [54.003992911447696]
オープンエンド生成タスクをトークンレベルの予測タスクに再構成する。
我々はLSMに答えを自己評価するように指示する。
自己評価に基づくスコアリング手法をベンチマークする。
論文 参考訳(メタデータ) (2023-12-14T19:09:22Z) - Factcheck-GPT: End-to-End Fine-Grained Document-Level Fact-Checking and
Correction of LLM Output [124.25862294329058]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
ラベル付け手順を高速化し、ラッカーの作業を簡単にするためのアノテーションツールを設計し、構築する。
オープンドメインの文書レベルの事実性ベンチマークを3段階のクレーム,文,文書で構築する。
論文 参考訳(メタデータ) (2023-11-15T14:41:57Z) - LLM4DV: Using Large Language Models for Hardware Test Stimuli Generation [5.905138464855556]
本稿では,大規模言語モデル(LLM)からテスト刺激を抽出するための新しいベンチマークフレームワークを提案する。
LLM4DVと従来の制約ランダムテスト(CRT)を3つのDUTモジュールを用いて比較する。
LLM4DVは、基本的な数学的推論と事前学習された知識を活用する能力を利用して、単純なDUTシナリオを効率的に処理できることを実証した。
論文 参考訳(メタデータ) (2023-10-06T19:02:04Z) - LLM for Test Script Generation and Migration: Challenges, Capabilities,
and Opportunities [8.504639288314063]
テストスクリプト生成はソフトウェアテストの重要なコンポーネントであり、反復的なテストタスクの効率的かつ信頼性の高い自動化を可能にする。
既存の世代のアプローチは、さまざまなデバイス、プラットフォーム、アプリケーション間でテストスクリプトを正確にキャプチャし、再現することの難しさなど、しばしば制限に直面する。
本稿では,モバイルアプリケーションテストスクリプト生成分野における大規模言語モデル(LLM)の適用について検討する。
論文 参考訳(メタデータ) (2023-09-24T07:58:57Z) - Anomaly Detection Based on Selection and Weighting in Latent Space [73.01328671569759]
SWADと呼ばれる新しい選択および重み付けに基づく異常検出フレームワークを提案する。
ベンチマークと実世界のデータセットによる実験は、SWADの有効性と優位性を示している。
論文 参考訳(メタデータ) (2021-03-08T10:56:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。