Fugu-MT 論文翻訳(概要): LF-checker: Machine Learning Acceleration of Bounded Model Checking for Concurrency Verification (Competition Contribution)

論文の概要: LF-checker: Machine Learning Acceleration of Bounded Model Checking for Concurrency Verification (Competition Contribution)

arxiv url: http://arxiv.org/abs/2301.09142v1
Date: Sun, 22 Jan 2023 15:46:57 GMT
ステータス: 処理完了
システム内更新日: 2023-01-24 14:45:54.409091
Title: LF-checker: Machine Learning Acceleration of Bounded Model Checking for Concurrency Verification (Competition Contribution)
Title（参考訳）: lf-checker: 並行性検証のための境界モデルチェックの機械学習アクセラレーション(競合貢献)
Authors: Tong Wu and Edoardo Manino and Fatimah Aljaafari and Pavlos Petoumenos and Lucas C. Cordeiro
Abstract要約: 機械学習に基づくメタ検証ツールLF-checkerを記述・評価する。テスト中のプログラムの複数の特徴を抽出し、決定木による境界モデルチェッカーの最適構成を予測する。
参考スコア（独自算出の注目度）: 15.600922269515756
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We describe and evaluate LF-checker, a metaverifier tool based on machine learning. It extracts multiple features of the program under test and predicts the optimal configuration (flags) of a bounded model checker with a decision tree. Our current work is specialised in concurrency verification and employs ESBMC as a back-end verification engine. In the paper, we demonstrate that LF-checker achieves better results than the default configuration of the underlying verification engine.
Abstract（参考訳）: 機械学習に基づくメタ検証ツールLF-checkerを記述・評価する。テスト中のプログラムの複数の特徴を抽出し、決定木による境界モデルチェッカーの最適設定(フラグ)を予測する。現在の作業は並列性検証に特化しており、バックエンド検証エンジンとしてESBMCを使用しています。本稿では,LFチェックが基礎となる検証エンジンのデフォルト設定よりも優れた結果が得られることを示す。

関連論文リスト

BanditCAT and AutoIRT: Machine Learning Approaches to Computerized Adaptive Testing and Item Calibration [7.261063083251448]
本稿では,少数の応答を持つ大規模コンピュータ適応テスト(CAT)の校正と管理を行うための完全なフレームワークを提案する。自動機械学習(AutoML)とアイテム応答理論(IRT)を組み合わせた新しい手法であるAutoIRTを使用している。我々は、コンテキスト的バンディットフレームワークに問題をキャストし、アイテム応答理論(IRT)を利用する手法であるBanditCATフレームワークを提案する。
論文参考訳（メタデータ） (2024-10-28T13:54:10Z)
Optimized Feature Generation for Tabular Data via LLMs with Decision Tree Reasoning [53.241569810013836]
本稿では,大規模言語モデル(LLM)を用いて,効率的な特徴生成ルールを同定するフレームワークを提案する。我々は、自然言語で容易に表現できるため、この推論情報を伝達するために決定木を使用します。 OCTreeは様々なベンチマークで様々な予測モデルの性能を継続的に向上させる。
論文参考訳（メタデータ） (2024-06-12T08:31:34Z)
Learning to Check: Unleashing Potentials for Self-Correction in Large Language Models [5.463333911506443]
我々は,タスクチェックのためのトレーニングデータを構築することで,大規模言語モデル(LLM)の自己チェック能力を向上させることを目指している。ステップCoTチェック(Step CoT Check)と呼ばれる特殊なチェックフォーマットを提案する。実験により、"Step CoT Check"フォーマットによる微調整により、LCMの自己チェックと自己補正能力が大幅に向上することが示された。
論文参考訳（メタデータ） (2024-02-20T14:23:23Z)
Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文参考訳（メタデータ） (2023-11-15T14:41:57Z)
Sparse Conditional Hidden Markov Model for Weakly Supervised Named Entity Recognition [68.68300358332156]
雑音ラベリング機能を評価するために,スパース条件付き隠れマルコフモデル(Sparse-CHMM)を提案する。 Sparse-CHMMは、3段階のトレーニングパイプラインで教師なし学習によって最適化される。 5つの包括的なデータセットで平均F1スコアが3.01向上する。
論文参考訳（メタデータ） (2022-05-27T20:47:30Z)
On the Limits of Evaluating Embodied Agent Model Generalization Using Validation Sets [101.28658250723804]
本稿では,より広い視野を効果的に活用し,次のステップでナビゲーションや操作を行うかを選択するモジュールによるトランスフォーマーモデルの拡張実験を行う。提案したモジュールは改良され,実際に,一般的なベンチマークデータセットであるALFREDの未確認検証セット上での最先端のパフォーマンスが向上した。この結果は、機械学習タスクではより広い現象かもしれないが、主にテストスプリットの評価を制限するベンチマークでのみ顕著である、と我々は考えているので強調する。
論文参考訳（メタデータ） (2022-05-18T23:52:21Z)
Scaling up Memory-Efficient Formal Verification Tools for Tree Ensembles [2.588973722689844]
ツール記述として提示されたVoTEアルゴリズムを形式化し拡張する。コア検証エンジンからプロパティチェックを分離することで、汎用性のある要件の検証が可能となります。数値認識と航空機衝突回避という2つのケーススタディで、このツールの適用を実証します。
論文参考訳（メタデータ） (2021-05-06T11:50:22Z)
Autoencoding Variational Autoencoder [56.05008520271406]
我々は,この行動が学習表現に与える影響と,自己整合性の概念を導入することでそれを修正する結果について検討する。自己整合性アプローチで訓練されたエンコーダは、敵攻撃による入力の摂動に対して頑健な(無神経な)表現につながることを示す。
論文参考訳（メタデータ） (2020-12-07T14:16:14Z)
End-to-End Object Detection with Transformers [88.06357745922716]
本稿では,オブジェクト検出を直接セット予測問題とみなす新しい手法を提案する。我々のアプローチは検出パイプラインを合理化し、手作業で設計された多くのコンポーネントの必要性を効果的に除去する。この新しいフレームワークの主な構成要素は、Detection TRansformerまたはDETRと呼ばれ、セットベースのグローバルな損失である。
論文参考訳（メタデータ） (2020-05-26T17:06:38Z)

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