論文の概要: QuickCheck for VDM
- arxiv url: http://arxiv.org/abs/2410.02046v1
- Date: Wed, 2 Oct 2024 21:25:10 GMT
- ステータス: 処理完了
- システム内更新日: 2024-11-04 09:15:24.947571
- Title: QuickCheck for VDM
- Title(参考訳): VDM用QuickCheck
- Authors: Nick Battle, Markus Solecki Ellyton,
- Abstract要約: 本稿では,VDM仕様の軽量検証ツールQuickCheckについて述べる。
このツールの目的は、証明義務を迅速に分類することである。
本稿では,このツールを用いて,VDM仕様の大規模な検証を行い,今後の方向性を提案する。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We describe recent work on a lightweight verification tool for VDM specifications, called QuickCheck. The objective of the tool is to quickly categorise proof obligations: identifying those that fail with counterexamples, those that are probably provable and those that require deeper analysis. The paper discusses the design of the tool and its use of pluggable strategies for adding extra checking. We present the results of the tool being used to check a large set of VDM specifications, and suggest future directions.
- Abstract(参考訳): 本稿では,VDM仕様の軽量検証ツールQuickCheckについて述べる。
このツールの目的は、証明義務を迅速に分類することであり、反例で失敗する者、おそらく証明可能なもの、より深い分析を必要とするものを特定することである。
本稿は,ツールの設計と追加チェックのためのプラグイン可能な戦略の利用について論じる。
本稿では,このツールを用いて,VDM仕様の大規模な検証を行い,今後の方向性を提案する。
関連論文リスト
- Verifying Non-friendly Formal Verification Designs: Can We Start Earlier? [2.1626093085892144]
本稿では,2つの主要なステップからなるメタモデリング技術に基づく自動手法を提案する。
まず、C++で書かれた未使用のアルゴリズム記述を、生成されたアサーションを使用して早期に検証する。
第2に、HLECとそのメタモデルパラメータを用いて、このアルゴリズム記述をシーケンシャルな設計に対して検証する。
論文 参考訳(メタデータ) (2024-10-24T06:09:40Z) - Tools Fail: Detecting Silent Errors in Faulty Tools [27.822981272044043]
我々は、モデルが「サイレント」ツールを検出する能力を調べるためのツールのためのフレームワークを紹介します。
制御電卓設定と具体化エージェント計画の両方で有望な結果が得られるような早期の故障復旧手法を提案する。
論文 参考訳(メタデータ) (2024-06-27T14:52:34Z) - DetToolChain: A New Prompting Paradigm to Unleash Detection Ability of MLLM [81.75988648572347]
DetToolChainはマルチモーダル大言語モデル(MLLM)のゼロショットオブジェクト検出能力を解き放つ新しいパラダイムである。
提案手法は,高精度検出にヒントを得た検出プロンプトツールキットと,これらのプロンプトを実装するための新しいChain-of-Thoughtから構成される。
DetToolChainを用いたGPT-4Vは,オープン語彙検出のための新しいクラスセットにおいて,最先端のオブジェクト検出器を+21.5%AP50で改善することを示す。
論文 参考訳(メタデータ) (2024-03-19T06:54:33Z) - What Are Tools Anyway? A Survey from the Language Model Perspective [67.18843218893416]
言語モデル(LM)は強力だが、主にテキスト生成タスクに向いている。
LMが使用する外部プログラムとしてツールを統一的に定義する。
各種ツールの効率を実証的に検討した。
論文 参考訳(メタデータ) (2024-03-18T17:20:07Z) - EASYTOOL: Enhancing LLM-based Agents with Concise Tool Instruction [56.02100384015907]
EasyToolは、多種多様で長いツールドキュメントを統一的で簡潔なツール命令に変換するフレームワークである。
トークン使用量を大幅に削減し、現実のシナリオにおけるツール利用のパフォーマンスを向上させることができる。
論文 参考訳(メタデータ) (2024-01-11T15:45:11Z) - ControlLLM: Augment Language Models with Tools by Searching on Graphs [97.62758830255002]
我々は,大規模言語モデル(LLM)が実世界のタスクを解くためのマルチモーダルツールを利用できる新しいフレームワークであるControlLLMを提案する。
フレームワークは,(1)複雑なタスクを明確なサブタスクに分割し,入力と出力を適切に定義したサブタスクに分解するtextittask Decomposer,(2)構築済みのツールグラフ上で最適なソリューションパスを探索する textitThoughts-on-Graph(ToG)パラダイム,(3)ソリューションパスを解釈して実行するリッチなツールボックスを備えた textitexecution Engine,の3つの主要なコンポーネントから構成される。
論文 参考訳(メタデータ) (2023-10-26T21:57:21Z) - Tool Documentation Enables Zero-Shot Tool-Usage with Large Language
Models [90.96816639172464]
大規模言語モデル(LLM)は、ツールの使用のデモを提供することで、新しいツールを使用するように教えられている。
デモよりも、ツールドキュメンテーションの使用、個々のツール使用方法の説明を推奨します。
論文 参考訳(メタデータ) (2023-08-01T17:21:38Z) - CausalVLR: A Toolbox and Benchmark for Visual-Linguistic Causal
Reasoning [107.81733977430517]
CausalVLR(Causal Visual-Linguistic Reasoning)は、最先端の因果関係の発見と因果推論方法の豊富なセットを含むオープンソースのツールボックスである。
これらのメソッドはNVIDIAコンピューティングシステムの下でPyTorchを実装したツールボックスに含まれている。
論文 参考訳(メタデータ) (2023-06-30T08:17:38Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。