論文の概要: 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) の機能を強調した。 さらに,セレンによる課題が今後の研究で緩和される可能性が示唆された。

関連論文リスト

• AutoPT: How Far Are We from the End2End Automated Web Penetration Testing? [54.65079443902714]
  LLMによって駆動されるPSMの原理に基づく自動浸透試験エージェントであるAutoPTを紹介する。 以上の結果から, AutoPT は GPT-4o ミニモデル上でのベースラインフレームワーク ReAct よりも優れていた。
  論文  参考訳（メタデータ） (2024-11-02T13:24:30Z)
• Towards Automated Penetration Testing: Introducing LLM Benchmark, Analysis, and Improvements [1.4433703131122861]
  大規模言語モデル(LLM)は、サイバーセキュリティなど、さまざまな分野に可能性を示している。 現在、包括的で、オープンで、エンドツーエンドの自動浸透テストベンチマークはありません。 本稿では,LLMを用いた自動貫入試験のための新しいオープンベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-10-22T16:18:41Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Test Oracle Automation in the era of LLMs [52.69509240442899]
  大規模言語モデル(LLM)は、多様なソフトウェアテストタスクに取り組むのに顕著な能力を示した。 本研究の目的は, 各種のオラクル生成時に生じる課題とともに, LLMs によるオラクルの自動化の可能性について検討することである。
  論文  参考訳（メタデータ） (2024-05-21T13:19:10Z)
• 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)
• Anomaly Detection Based on Selection and Weighting in Latent Space [73.01328671569759]
  SWADと呼ばれる新しい選択および重み付けに基づく異常検出フレームワークを提案する。 ベンチマークと実世界のデータセットによる実験は、SWADの有効性と優位性を示している。
  論文  参考訳（メタデータ） (2021-03-08T10:56:38Z)

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

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