論文の概要: Selene: Pioneering Automated Proof in Software Verification
- arxiv url: http://arxiv.org/abs/2401.07663v2
- Date: Wed, 5 Jun 2024 08:16:12 GMT
- ステータス: 処理完了
- システム内更新日: 2024-06-07 03:35:00.678191
- 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 の機能を強調した。
- 参考スコア(独自算出の注目度): 62.09555413263788
- 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 operating system microkernel, seL4. Selene provides a comprehensive framework for end-to-end proof generation and a lightweight verification environment. Our experimental results with advanced large language models (LLMs), such as GPT-3.5-turbo and GPT-4, highlight the capabilities of 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 の機能を強調した。
さらに,セレンによる課題が今後の研究で緩和される可能性が示唆された。
関連論文リスト
- Test Oracle Automation in the era of LLMs [52.69509240442899]
大規模言語モデル(LLM)は、多様なソフトウェアテストタスクに取り組むのに顕著な能力を示した。
本研究の目的は, 各種のオラクル生成時に生じる課題とともに, LLMs によるオラクルの自動化の可能性について検討することである。
論文 参考訳(メタデータ) (2024-05-21T13:19:10Z) - Generating Test Scenarios from NL Requirements using Retrieval-Augmented LLMs: An Industrial Study [5.179738379203527]
本稿では,Large Language Models (LLM) を用いたRAG(Retrieval-Augmented Generation) を用いたテストシナリオ生成のための自動アプローチ(RAGTAG)を提案する。
オーストリアポストの2つの産業プロジェクトにおけるRAGTAGの評価を行い,ドイツ語と英語のバイリンガル要件について検討した。
論文 参考訳(メタデータ) (2024-04-19T10:27:40Z) - Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。
仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。
実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
論文 参考訳(メタデータ) (2024-03-31T18:15:49Z) - ChIRAAG: ChatGPT Informed Rapid and Automated Assertion Generation [10.503097140635374]
ChIRAAGはOpenAI GPT4をベースとして、設計の自然言語仕様からSystem Verilog Assertion (SVA)を生成する。
実験では、LSM生成した生のアサーションの27%に誤りがあり、数回の反復で修正された。
以上の結果から,LLMはアサーション生成プロセスにおいて技術者を合理化し,支援し,検証を再構築できることが示唆された。
論文 参考訳(メタデータ) (2024-01-31T12:41:27Z) - 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 [46.26208489175692]
大規模言語モデル(LLM)を用いた要件から実行可能なMRを自動的に抽出する手法を提案する。
提案手法の有効性を評価するため,シーメンス・インダストリー・ソフトウェアと共同で質問紙調査を行った。
論文 参考訳(メタデータ) (2024-01-30T13:52:47Z) - Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳(メタデータ) (2023-11-15T14:41:57Z) - Guiding Large Language Models via Directional Stimulus Prompting [114.84930073977672]
我々は,特定の所望の出力に対して,ブラックボックス大言語モデル(LLM)を導くための新しいフレームワークであるDirectional Stimulus Promptingを紹介する。
LLMを直接調整するのではなく、小さな調整可能なポリシーモデルを用いて各入力インスタンスに対して補助的な指向性刺激プロンプトを生成する。
論文 参考訳(メタデータ) (2023-02-22T17:44:15Z) - Anomaly Detection Based on Selection and Weighting in Latent Space [73.01328671569759]
SWADと呼ばれる新しい選択および重み付けに基づく異常検出フレームワークを提案する。
ベンチマークと実世界のデータセットによる実験は、SWADの有効性と優位性を示している。
論文 参考訳(メタデータ) (2021-03-08T10:56:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。