論文の概要: Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs

• arxiv url: http://arxiv.org/abs/2501.12972v1
• Date: Wed, 22 Jan 2025 15:57:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-23 16:53:47.868506
• Title: Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs
• Title（参考訳）: アクセシブルスマートコントラクト検証:リテートLDMによる形式モデルの合成
• Authors: Jan Corazza, Ivan Gavran, Gabriela Moreira, Daniel Neider,
• Abstract要約: ソフトウェア正当性を確立する最も強力な方法の1つは、フォーマルな方法を使用することである。 私たちの仕事は、形式モデルの作成を自動化することで、この重大な欠点に対処します。 このようにして、形式モデルを作成するのに必要な時間を大幅に削減する。
• 参考スコア（独自算出の注目度）: 7.087237546722617
• License:
• Abstract: When blockchain systems are said to be trustless, what this really means is that all the trust is put into software. Thus, there are strong incentives to ensure blockchain software is correct -- vulnerabilities here cost millions and break businesses. One of the most powerful ways of establishing software correctness is by using formal methods. Approaches based on formal methods, however, induce a significant overhead in terms of time and expertise required to successfully employ them. Our work addresses this critical disadvantage by automating the creation of a formal model -- a mathematical abstraction of the software system -- which is often a core task when employing formal methods. We perform model synthesis in three phases: we first transpile the code into model stubs; then we "fill in the blanks" using a large language model (LLM); finally, we iteratively repair the generated model, on both syntactical and semantical level. In this way, we significantly reduce the amount of time necessary to create formal models and increase accessibility of valuable software verification methods that rely on them. The practical context of our work was reducing the time-to-value of using formal models for correctness audits of smart contracts.
• Abstract（参考訳）: ブロックチェーンシステムが信頼できないと言われる場合、これが本当に意味することは、すべての信頼がソフトウェアに組み込まれるということです。 したがって、ブロックチェーンソフトウェアが正しいことを保証する強力なインセンティブがある -- 脆弱性は数百万ドルになり、ビジネスを壊す。ソフトウェア正当性を確立する最も強力な方法の1つは、フォーマルなメソッドを使用することである。しかし、フォーマルなメソッドに基づくアプローチは、それらをうまく採用するのに必要な時間と専門知識の面で重大なオーバーヘッドを生じさせる。我々の研究は、フォーマルなモデル -- ソフトウェアシステムの数学的抽象化 -- を自動生成することで、この重大な欠点に対処する。これは、フォーマルなメソッドを使用する際の中核的なタスクである。 まず、モデルをモデルスタブにトランスパイルし、次に、大きな言語モデル(LLM)を使って「空白を埋める」という3つのフェーズでモデル合成を行い、最後に、構文と意味の両方のレベルで生成されたモデルを反復的に修復します。 このようにして、フォーマルなモデルを作成するのに必要な時間を大幅に削減し、それに依存する価値あるソフトウェア検証手法のアクセシビリティを向上させる。 我々の研究の実践的文脈は、スマートコントラクトの正当性監査に形式モデルを使用する際の時間と価値の削減であった。

関連論文リスト

• Leveraging Fine-Tuned Language Models for Efficient and Accurate Smart Contract Auditing [5.65127016235615]
  本稿では,スマートコントラクト監査において,より小型で微調整されたモデルを用いて,同等あるいは優れた結果が得られる可能性について検討する。 本稿では,スマートコントラクト監査のための費用対効果の高い特化モデルの開発を目的としたFTSmartAuditフレームワークを紹介する。 コントリビューションには,(1)データ準備,トレーニング,評価,継続的な学習を効率化するシングルタスク学習フレームワーク,(2)ドメイン固有知識蒸留を利用した堅牢なデータセット生成手法,(3)モデルの正確性と堅牢性を維持するための適応型学習戦略などが含まれている。
  論文  参考訳（メタデータ） (2024-10-17T09:09:09Z)
• Accelerating Large Language Model Inference with Self-Supervised Early Exits [0.0]
  本稿では,大規模・事前学習型言語モデル(LLM)における推論を高速化する新しい手法を提案する。 本稿では,既存の変圧器層上に早期出口「頭部」を統合し,信頼度基準に基づく条件付き項化を容易にすることを提案する。
  論文  参考訳（メタデータ） (2024-07-30T07:58:28Z)
• Promises and Pitfalls of Generative Masked Language Modeling: Theoretical Framework and Practical Guidelines [74.42485647685272]
  GMLM(Generative Masked Language Models)に焦点を当てる。 我々は,マルコフ連鎖の入力として使用されるマスキングにより,データ分布の条件付き確率に適合するモデルを訓練し,モデルからサンプルを抽出する。 我々は,T5モデルを並列デコーディングに適応させ,最小品質の犠牲を伴って機械翻訳における2～3倍の高速化を実現した。
  論文  参考訳（メタデータ） (2024-07-22T18:00:00Z)
• Adversarial Contrastive Decoding: Boosting Safety Alignment of Large Language Models via Opposite Prompt Optimization [34.29833630422768]
  Adversarial Contrastive Decoding (ACD)は、プロンプトベースのコントラストデコーディングのための2つの逆のシステムプロンプトを生成する最適化ベースのフレームワークである。 ACDは、元の生成能力を犠牲にすることなく、従来のトレーニング不要復号法よりもはるかに優れた安全性を実現する。
  論文  参考訳（メタデータ） (2024-06-24T15:51:30Z)
• DeAL: Decoding-time Alignment for Large Language Models [59.63643988872571]
  大規模言語モデル(LLM)は、現在、人間の好みに沿ったコンテンツを生成することが期待されている。 本稿では,報酬関数をカスタマイズ可能なフレームワークであるDeALを提案し,LLMのDetime Alignmentを可能にする。 実験の結果,粒度の細かいトレードオフでDeALを実現できること,アライメント目標への適合性の向上,LLMの残差の解消が可能であることがわかった。
  論文  参考訳（メタデータ） (2024-02-05T06:12:29Z)
• Increasing Trust in Language Models through the Reuse of Verified Circuits [1.8434042562191815]
  言語モデル(LM)は、幅広い予測タスクにますます使われていますが、それらのトレーニングは稀なエッジケースを無視します。 数学的および論理的に定義されたフレームワークを使用して構築すれば、この標準を満たすようにモデルをトレーニングできることが示される。 両タスクの加算回路を広範囲に再利用し,より複雑な減算器モデルの検証を容易にする。
  論文  参考訳（メタデータ） (2024-02-04T21:33:18Z)
• Adapting Large Language Models for Content Moderation: Pitfalls in Data Engineering and Supervised Fine-tuning [79.53130089003986]
  大規模言語モデル(LLM)は、様々なドメインでタスクを処理するための実現可能なソリューションとなっている。 本稿では、コンテンツモデレーションのためにプライベートにデプロイ可能なLLMモデルを微調整する方法を紹介する。
  論文  参考訳（メタデータ） (2023-10-05T09:09:44Z)
• Cheaply Evaluating Inference Efficiency Metrics for Autoregressive Transformer APIs [66.30706841821123]
  大規模言語モデル(LLM)は、自然言語処理において多くの最先端システムに電力を供給する。 LLMは、推論時でさえ非常に計算コストが高い。 モデル間での推論効率を比較するための新しい指標を提案する。
  論文  参考訳（メタデータ） (2023-05-03T21:51:42Z)
• CodeLMSec Benchmark: Systematically Evaluating and Finding Security Vulnerabilities in Black-Box Code Language Models [58.27254444280376]
  自動コード生成のための大規模言語モデル(LLM)は、いくつかのプログラミングタスクにおいてブレークスルーを達成した。 これらのモデルのトレーニングデータは、通常、インターネット(例えばオープンソースのリポジトリから)から収集され、障害やセキュリティ上の脆弱性を含む可能性がある。 この不衛生なトレーニングデータは、言語モデルにこれらの脆弱性を学習させ、コード生成手順中にそれを伝播させる可能性がある。
  論文  参考訳（メタデータ） (2023-02-08T11:54:07Z)
• The Right Tool for the Job: Matching Model and Instance Complexities [62.95183777679024]
  NLPモデルが大きくなればなるほど、訓練されたモデルを実行するには、金銭的・環境的なコストを発生させる重要な計算資源が必要である。 我々は、推論中、早期(かつ高速)の"exit"を可能にする文脈表現微調整の修正を提案する。 3つのテキスト分類データセットと2つの自然言語推論ベンチマークの2つのタスクで、5つの異なるデータセットに対して提案した修正を検証した。
  論文  参考訳（メタデータ） (2020-04-16T04:28:08Z)

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

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