論文の概要: Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
- arxiv url: http://arxiv.org/abs/2509.20421v2
- Date: Fri, 26 Sep 2025 09:51:15 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-09-29 12:12:20.343408
- Title: Formal Verification of Legal Contracts: A Translation-based Approach (Extended Version)
- Title(参考訳): 法的契約の形式的検証:翻訳に基づくアプローチ(拡張版)
- Authors: Reiner Hähnle, Cosimo Laneve, Adele Veschetti,
- Abstract要約: 本稿では,Java モデリング言語仕様に注釈付けされた Java コードへの変換を通じて,Stipula 契約の正当性を正式に検証する手法を提案する。
検証バックエンドとしては、推論検証ツールのKeYが使用されている。
- 参考スコア(独自算出の注目度): 0.2446948464551684
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Stipula is a domain-specific programming language designed to model legal contracts with enforceable properties, especially those involving asset transfers and obligations. This paper presents a methodology to formally verify the correctness of Stipula contracts through translation into Java code annotated with Java Modeling Language specifications. As a verification backend, the deductive verification tool KeY is used. Both, the translation and the verification of partial and total correctness for a large subset of Stipula contracts, those with disjoint cycles, is fully automatic. Our work demonstrates that a general-purpose deductive verification tool can be used successfully in a translation approach.
- Abstract(参考訳): Stipulaは、強制可能な資産、特に資産譲渡と義務を含む法的契約をモデル化するために設計されたドメイン固有プログラミング言語である。
本稿では,Java モデリング言語仕様に注釈付けされた Java コードへの変換を通じて,Stipula 契約の正当性を正式に検証する手法を提案する。
検証バックエンドとしては、推論検証ツールのKeYが使用されている。
スチューラ契約の大規模な部分集合に対する変換と完全正当性(英語版)の検証はともに完全自動である。
本研究は, 汎用推論検証ツールを翻訳手法でうまく利用できることを実証するものである。
関連論文リスト
- Formal verification in Solidity and Move: insights from a comparative analysis [0.40964539027092906]
SolidityとMoveは、異なる設計と検証アプローチを備えた2つのコントラクト言語である。
本稿では,2つの言語が検証にどのように影響するか,また2つの言語に対する検証ツールの現状について検討する。
我々の調査は、CertoraとAptos Move Proverで実施された検証タスクのオープンデータセットによって支援されている。
論文 参考訳(メタデータ) (2025-02-19T18:06:01Z) - Lost in Translation, Found in Context: Sign Language Translation with Contextual Cues [56.038123093599815]
我々の目的は、連続手話から音声言語テキストへの翻訳である。
署名ビデオと追加のコンテキストキューを組み込む。
文脈的アプローチが翻訳の質を著しく向上させることを示す。
論文 参考訳(メタデータ) (2025-01-16T18:59:03Z) - LegalPro-BERT: Classification of Legal Provisions by fine-tuning BERT Large Language Model [0.0]
契約分析は、合意の範囲内で重要な規定及び段落の識別及び分類を必要とする。
LegalPro-BERTはBERTトランスフォーマーアーキテクチャモデルであり、法定条項の分類処理を効率的に行うために微調整を行う。
論文 参考訳(メタデータ) (2024-04-15T19:08:48Z) - DELTA: Pre-train a Discriminative Encoder for Legal Case Retrieval via Structural Word Alignment [55.91429725404988]
判例検索のための識別モデルであるDELTAを紹介する。
我々は浅層デコーダを利用して情報ボトルネックを作り、表現能力の向上を目指しています。
本手法は, 判例検索において, 既存の最先端手法よりも優れている。
論文 参考訳(メタデータ) (2024-03-27T10:40:14Z) - Enhancing Translation Validation of Compiler Transformations with Large
Language Models [5.103162976634333]
本稿では,Large Language Models (LLM) を翻訳検証に組み込むフレームワークを提案する。
まず,既存の形式検証ツールを用いて翻訳検証を行う。
フォーマルな検証ツールが変換の健全性を確認することができない場合、我々のフレームワークは予測に微調整のLLMを用いる。
論文 参考訳(メタデータ) (2024-01-30T07:24:04Z) - Formal Modeling and Analysis of Legal Contracts using ContractCheck [0.0]
textitContractCheckは、法律契約、特に販売購入協定(SPA)の整合性解析を可能にする
この分析は、SPAの節の実行のための前提の符号化と、一階述語論理の決定可能な断片を用いた制約の提案に依存している。
論文 参考訳(メタデータ) (2022-12-06T22:03:11Z) - Multilingual Extraction and Categorization of Lexical Collocations with
Graph-aware Transformers [86.64972552583941]
我々は,グラフ対応トランスフォーマアーキテクチャにより拡張されたBERTに基づくシーケンスタグ付けモデルを提案し,コンテキストにおけるコロケーション認識の課題について評価した。
以上の結果から, モデルアーキテクチャにおける構文的依存関係を明示的に符号化することは有用であり, 英語, スペイン語, フランス語におけるコロケーションのタイプ化の差異について考察する。
論文 参考訳(メタデータ) (2022-05-23T16:47:37Z) - Automatic Extraction of Rules Governing Morphological Agreement [103.78033184221373]
原文から第一パス文法仕様を抽出する自動フレームワークを開発する。
我々は、世界の多くの言語の文法の中核にあるモルフォシンタクティックな現象である合意を記述する規則の抽出に焦点をあてる。
我々のフレームワークはUniversal Dependenciesプロジェクトに含まれるすべての言語に適用され、有望な結果が得られます。
論文 参考訳(メタデータ) (2020-10-02T18:31:45Z) - Multilingual Alignment of Contextual Word Representations [49.42244463346612]
BERTはXNLIのゼロショット性能をベースモデルに比べて大幅に改善した。
単語検索の文脈バージョンを導入し、下流のゼロショット転送とよく相関していることを示す。
これらの結果は、大規模多言語事前学習モデルの理解に有用な概念としてコンテキストアライメントをサポートする。
論文 参考訳(メタデータ) (2020-02-10T03:27:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。