論文の概要: FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware

• arxiv url: http://arxiv.org/abs/2410.23299v1
• Date: Tue, 15 Oct 2024 21:48:57 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-11-03 08:19:31.573882
• Title: FVEval: Understanding Language Model Capabilities in Formal Verification of Digital Hardware
• Title（参考訳）: FVEval: デジタルハードウェアの形式検証における言語モデル能力の理解
• Authors: Minwoo Kang, Mingjie Liu, Ghaith Bany Hamad, Syed Suhaib, Haoxing Ren,
• Abstract要約: FVEvalは,形式的検証(FV)に関わるタスクにおいて,大規模言語モデル(LLM)のパフォーマンスを特徴付ける最初の総合ベンチマークである。 ベンチマークは3つのサブタスクで構成され、異なるレベルでLLM能力を測定する。 本稿では,FVに整合した合成例を生成するための,専門家による検証手法と手法のコレクションについて述べる。
• 参考スコア（独自算出の注目度）: 4.480157114854711
• License:
• Abstract: The remarkable reasoning and code generation capabilities of large language models (LLMs) have spurred significant interest in applying LLMs to enable task automation in digital chip design. In particular, recent work has investigated early ideas of applying these models to formal verification (FV), an approach to verifying hardware implementations that can provide strong guarantees of confidence but demands significant amounts of human effort. While the value of LLM-driven automation is evident, our understanding of model performance, however, has been hindered by the lack of holistic evaluation. In response, we present FVEval, the first comprehensive benchmark and evaluation framework for characterizing LLM performance in tasks pertaining to FV. The benchmark consists of three sub-tasks that measure LLM capabilities at different levels: from the generation of SystemVerilog assertions (SVAs) given natural language descriptions to reasoning about the design RTL and suggesting assertions directly without additional human input. As test instances, we present both collections of expert-written verification collateral and methodologies to scalably generate synthetic examples aligned with industrial FV workflows. A wide range of existing LLMs, both proprietary and open-source, are evaluated against FVEval, based on which we investigate where today's LLMs stand and how we might further enable their application toward improving productivity in digital FV. Our benchmark and evaluation code is available at \url{https://github.com/NVlabs/FVEval}.
• Abstract（参考訳）: 大型言語モデル(LLM)の顕著な推論とコード生成能力は、デジタルチップ設計におけるタスク自動化の実現にLLMを適用することに大きな関心を惹き付けている。 特に最近の研究は、これらのモデルをフォーマルな検証(FV)に適用するという初期のアイデアを調査している。 LLMによる自動化の価値は明らかだが、モデル性能に対する理解は、全体的な評価の欠如によって妨げられている。 そこで本研究では,FVに関連するタスクにおいてLLM性能を特徴付けるための,初の総合的なベンチマークおよび評価フレームワークであるFVEvalを提案する。 ベンチマークは3つのサブタスクから構成されており、SystemVerilogのアサーション(SVAs)の生成から、設計RTLに関する推論や、追加の人間の入力なしにアサーションを直接提案に至るまで、さまざまなレベルでLLM能力を測定する。 テスト事例として、専門家による検証の検証と、産業用FVワークフローに整合した合成例を巧みに生成する手法の両方を提示する。 既存のLLMはプロプライエタリでもオープンソースでも、FVEvalに対して幅広い評価がなされており、今日のLLMの立ち位置と、デジタルFVにおける生産性向上へのさらなる応用方法について検討している。 我々のベンチマークと評価コードは \url{https://github.com/NVlabs/FVEval} で公開されている。

関連論文リスト

• AutoBench-V: Can Large Vision-Language Models Benchmark Themselves? [55.14033256706175]
  視覚・言語情報の統合を促進するためには,LVLM(Large Vision-Language Models)が不可欠である。 本稿では,需要評価のための自動フレームワークであるAutoBench-Vを紹介する。 5つの要求されたユーザ入力にまたがる7つのLVLMの広範な評価を通じて、このフレームワークの有効性と信頼性を示す。
  論文  参考訳（メタデータ） (2024-10-28T17:55:08Z)
• VulnLLMEval: A Framework for Evaluating Large Language Models in Software Vulnerability Detection and Patching [0.9208007322096533]
  大きな言語モデル(LLM)は、コード翻訳のようなタスクにおいて有望であることを示している。 本稿では,C コードの脆弱性を特定し,パッチする際の LLM の性能を評価するためのフレームワーク VulnLLMEval を紹介する。 私たちの研究には、Linuxカーネルから抽出された307の現実世界の脆弱性が含まれている。
  論文  参考訳（メタデータ） (2024-09-16T22:00:20Z)
• LLM4VV: Exploring LLM-as-a-Judge for Validation and Verification Testsuites [6.796136787585992]
  大規模言語モデル(LLM)は進化し、ソフトウェア開発のランドスケープに大きな革命をもたらしています。 本稿では,ディレクティブプログラミングモデルのコンパイラ実装を評価するために使用されるテストの判定について考察する。
  論文  参考訳（メタデータ） (2024-08-21T15:54:17Z)
• Q*: Improving Multi-step Reasoning for LLMs with Deliberative Planning [53.6472920229013]
  大規模言語モデル(LLM)は多くの自然言語タスクにおいて印象的な能力を示している。 LLMは多段階推論を行う際にエラー、幻覚、矛盾する文を生成する傾向がある。 本稿では,LLMの復号化過程を検討計画で導くためのフレームワークであるQ*を紹介する。
  論文  参考訳（メタデータ） (2024-06-20T13:08:09Z)
• An Empirical Study of Automated Vulnerability Localization with Large Language Models [21.84971967029474]
  大規模言語モデル(LLM)は、様々な領域において可能性を示しているが、脆弱性のローカライゼーションにおけるその有効性は未解明のままである。 本調査では,ChatGPTや各種オープンソースモデルなど,コード解析に適した10以上のLLMを対象とする。 ゼロショット学習,ワンショット学習,識別的微調整,生成的微調整の4つのパラダイムを用いて,これらのLCMの有効性を検討する。
  論文  参考訳（メタデータ） (2024-03-30T08:42:10Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。 このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。 LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
  論文  参考訳（メタデータ） (2023-11-29T08:29:54Z)
• SEED-Bench-2: Benchmarking Multimodal Large Language Models [67.28089415198338]
  MLLM(Multimodal large language model)は、最近、テキストだけでなく、インターリーブされたマルチモーダル入力の画像を生成できることを実証した。 SEED-Bench-2は、正確な人間のアノテーションを持つ24Kの多重選択質問で構成されており、27次元にまたがっている。 我々は,23個の著名なオープンソースMLLMの性能を評価し,貴重な観察結果を要約した。
  論文  参考訳（メタデータ） (2023-11-28T05:53:55Z)
• ReForm-Eval: Evaluating Large Vision Language Models via Unified Re-Formulation of Task-Oriented Benchmarks [76.25209974199274]
  大規模視覚言語モデル(LVLM)は、視覚信号を知覚し、視覚的根拠を持つ推論を行う驚くべき能力を示す。 当社のベンチマークおよび評価フレームワークは,LVLMの開発を進めるための基盤としてオープンソース化される予定である。
  論文  参考訳（メタデータ） (2023-10-04T04:07:37Z)
• Measuring and Improving Chain-of-Thought Reasoning in Vision-Language Models [61.28463542324576]
  視覚言語モデル(VLM)は近年,人間のような出力を生成できる視覚アシスタントとして,強力な有効性を示している。 我々は、既存の最先端のVLMを評価し、最高の性能モデルでさえ、強力な視覚的推論能力と一貫性を示すことができないことを発見した。 本稿では,VLMの推論性能と一貫性の向上を目的とした2段階トレーニングフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-08T17:49:44Z)

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

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