Fugu-MT 論文翻訳(概要): An Agile Formal Specification Language Design Based on K Framework

論文の概要: An Agile Formal Specification Language Design Based on K Framework

arxiv url: http://arxiv.org/abs/2404.18515v1
Date: Mon, 29 Apr 2024 09:00:50 GMT
ステータス: 処理完了
システム内更新日: 2024-04-30 14:27:01.295212
Title: An Agile Formal Specification Language Design Based on K Framework
Title（参考訳）: Kフレームワークに基づいたアジャイルの形式仕様言語設計
Authors: Jianyu Zhang, Long Zhang, Yixuan Wu, Feng Yang,
Abstract要約: 本稿では,アジャイル形式仕様言語(ASL)を紹介する。 ASLの設計にはアジャイル設計の原則が組み込まれており、形式仕様の記述をシンプルに、より効率的に、スケーラブルにする。 ASLを検証のために実行可能なK形式仕様言語に変換することのできる仕様翻訳アルゴリズムが開発された。
参考スコア（独自算出の注目度）: 11.042686307366818
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Formal Methods (FMs) are currently essential for verifying the safety and reliability of software systems. However, the specification writing in formal methods tends to be complex and challenging to learn, requiring familiarity with various intricate formal specification languages and verification technologies. In response to the increasing complexity of software frameworks, existing specification writing methods fall short in meeting agility requirements. To address this, this paper introduces an Agile Formal Specification Language (ASL). The ASL is defined based on the K Framework and YAML Ain't Markup Language (YAML). The design of ASL incorporates agile design principles, making the writing of formal specifications simpler, more efficient, and scalable. Additionally, a specification translation algorithm is developed, capable of converting ASL into K formal specification language that can be executed for verification. Experimental evaluations demonstrate that the proposed method significantly reduces the code size needed for specification writing, enhancing agility in formal specification writing.
Abstract（参考訳）: フォーマルメソッド(FM)は、ソフトウェアシステムの安全性と信頼性を検証するために現在不可欠である。しかし、形式的手法による仕様記述は複雑で学習が難しい傾向にあり、様々な複雑な形式的仕様言語や検証技術に精通する必要がある。ソフトウェアフレームワークの複雑さが増大する中で、既存の仕様記述メソッドはアジリティ要件を満たすには不十分である。これを解決するために,本稿では,アジャイル形式仕様言語(ASL)を紹介する。 ASL は K Framework と YAML Ain't Markup Language (YAML) に基づいて定義されている。 ASLの設計にはアジャイル設計の原則が組み込まれており、形式仕様の記述をシンプルに、より効率的に、スケーラブルにする。さらに、ASLをK形式仕様言語に変換し、検証のために実行できる仕様翻訳アルゴリズムを開発した。実験により,提案手法は仕様作成に必要なコードサイズを大幅に削減し,形式的な仕様作成におけるアジリティの向上を図っている。

関連論文リスト

Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文参考訳（メタデータ） (2024-06-14T06:52:08Z)
Identifying and Analyzing Task-Encoding Tokens in Large Language Models [55.03191279766383]
本稿では,タスク性能が依存するタスク符号化トークンの識別と解析を行う。テンプレートとストップワードトークンはタスクエンコーディングが最も困難であることを示す。我々の研究は、大規模言語モデル(LLM)がいかにして、デモからタスクを実行するかを学習し、LLMでプレイされるさまざまな種類のトークンの役割の理解を深め、タスクエンコーディングトークンを不適切な利用から不安定を避けるための洞察を提供する。
論文参考訳（メタデータ） (2024-01-20T20:55:21Z)
SpecGen: Automated Generation of Formal Program Specifications via Large Language Models [20.36964281778921]
SpecGenは、大規模言語モデルに基づく形式的なプログラム仕様生成のための新しいテクニックである。 SV-COMP 279ベンチマークと手動で構築したデータセットを含む2つのデータセット上でSpecGenを評価する。
論文参考訳（メタデータ） (2024-01-16T20:13:50Z)
How Proficient Are Large Language Models in Formal Languages? An In-Depth Insight for Knowledge Base Question Answering [52.86931192259096]
知識ベース質問回答(KBQA)は,知識ベースにおける事実に基づいた自然言語質問への回答を目的としている。最近の研究は、論理形式生成のための大規模言語モデル(LLM)の機能を活用して性能を向上させる。
論文参考訳（メタデータ） (2024-01-11T09:27:50Z)
Validation of Rigorous Requirements Specifications and Document Automation with the ITLingo RSL Language [0.0]
ITLingoイニシアチブは、技術的文書の厳密さと一貫性を高めるためにRSLという要求仕様言語を導入した。本稿では、要求検証と文書自動化の分野における既存の研究・ツールについてレビューする。我々は、カスタマイズされたチェックと、RSL自体で動的に定義された言語規則に基づいて、仕様の検証によりRSLを拡張することを提案する。
論文参考訳（メタデータ） (2023-12-17T21:39:26Z)
Quantifying Language Models' Sensitivity to Spurious Features in Prompt Design or: How I learned to start worrying about prompt formatting [68.19544657508509]
言語モデル(LLM)は、言語技術の基本コンポーネントとして採用されている。いくつかの広く使われているオープンソースLLMは、数ショット設定でプロンプトフォーマットの微妙な変更に対して非常に敏感であることがわかった。本稿では,与えられたタスクに対して有効なプロンプトフォーマットのサンプルセットを迅速に評価するアルゴリズムを提案し,モデル重み付けにアクセスせずに期待性能の間隔を報告する。
論文参考訳（メタデータ） (2023-10-17T15:03:30Z)
Soft Language Clustering for Multilingual Model Pre-training [57.18058739931463]
本稿では,インスタンスを条件付きで符号化するためのフレキシブルガイダンスとして,コンテキスト的にプロンプトを検索するXLM-Pを提案する。我々のXLM-Pは、(1)言語間における言語不変および言語固有知識の軽量なモデリングを可能にし、(2)他の多言語事前学習手法との容易な統合を可能にする。
論文参考訳（メタデータ） (2023-06-13T08:08:08Z)
nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [3.1143846686797314]
大規模言語モデル(LLM)を適用するためのフレームワークであるnl2specは、構造化されていない自然言語から正式な仕様を導出する。本稿では,自然言語におけるシステム要求のあいまいさを検知し,解決する新たな手法を提案する。ユーザは、これらのサブ翻訳を反復的に追加、削除、編集して、不正なフォーマル化を修正する。
論文参考訳（メタデータ） (2023-03-08T20:08:53Z)
Prompting Language Models for Linguistic Structure [73.11488464916668]
本稿では,言語構造予測タスクに対する構造化プロンプト手法を提案する。提案手法は, 音声タグ付け, 名前付きエンティティ認識, 文チャンキングについて評価する。 PLMはタスクラベルの事前知識を事前学習コーパスに漏えいすることで有意な事前知識を含むが、構造化プロンプトは任意のラベルで言語構造を復元することも可能である。
論文参考訳（メタデータ） (2022-11-15T01:13:39Z)
Zero-shot Cross-lingual Transfer of Prompt-based Tuning with a Unified Multilingual Prompt [98.26682501616024]
我々はUniPromptと呼ばれるすべての言語に対して統一的なプロンプトを使用する新しいモデルを提案する。統一的なプロンプトは多言語 PLM による計算であり、言語に依存しない表現を生成する。提案手法は、異なる言語間で強いベースラインを著しく上回ることができる。
論文参考訳（メタデータ） (2022-02-23T11:57:52Z)
From English to Signal Temporal Logic [7.6398837478968025]
本稿では,サイバー物理システムのための公式な仕様言語であるSignal Temporal Logic (STL) に,自由英語文として与えられる非公式な要件を翻訳するためのツールおよびテクニックであるDeepSTLを提案する。このような翻訳を考案する上での大きな課題は、公式な非公式な要件と公式な仕様の欠如である。 2番目のステップでは、最先端のトランスフォーマーベースのニューラル翻訳技術を用いて、英語からSTLへの正確な注意翻訳を訓練する。
論文参考訳（メタデータ） (2021-09-21T16:13:29Z)

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

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