論文の概要: Neuroforger: certified violation witnesses for smart contracts verification via LLMs

• arxiv url: http://arxiv.org/abs/2605.31389v1
• Date: Fri, 29 May 2026 14:54:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-01 20:56:50.682644
• Title: Neuroforger: certified violation witnesses for smart contracts verification via LLMs
• Title（参考訳）: Neuroforger: LLMによるスマートコントラクト検証の認定違反証人
• Abstract要約: 近年の大規模言語モデル(LLM)では、スマートコントラクトが特定のプロパティを尊重するかどうかを予測できる推論機能が組み込まれている。 抽象型でSolidityを拡張する新しい形式仕様言語を導入する。 LLMと型チェックと具体的な実行を組み合わせたワークフローを設計し、違反証人を生成し検証する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Recent large language models (LLMs) incorporate reasoning capabilities that allow them to perform well in predicting whether a smart contract respects a certain property, suggesting a complementary approach to traditional formal-methods-based techniques for smart contract verification. However, the application of LLMs in such context has two major issues: 1) properties expressed in natural language are intrinsically ambiguous, and 2) answers returned by LLMs have no guarantee of correctness. In this paper, we address both issues simultaneously by: 1) introducing a new formal specification language that extends Solidity with abstract types, and 2) designing a workflow that combines LLMs with type checking and concrete execution to generate and validate violation witnesses (i.e., counterexamples). The key idea is to represent a specification as a Solidity test with (existentially quantified) variables of abstract type; finding an instantiation of these variables to concrete values (of the correct type) concretizes the test into an executable counterexample (PoC) for the target property. We implemented our procedure in the tool Neuroforger, experimentally evaluating it on a smart-contract verification dataset drawn from literature, obtaining promising results that demonstrate its potential applicability in the wild.
• Abstract（参考訳）: 最近の大規模言語モデル(LLM)では、スマートコントラクトが特定のプロパティを尊重するかどうかを予測できる推論機能が導入されており、スマートコントラクト検証のための従来のフォーマルメソッドベースのテクニックに対する補完的なアプローチが提案されている。 しかし、そのような文脈におけるLLMの適用には2つの大きな問題がある。 1)自然言語で表される性質は本質的に曖昧であり、 2) LLM による回答には正当性の保証がない。 本稿では,2つの課題を同時に解決する。 1)Solidityを抽象型で拡張する新しい形式仕様言語を導入し、 2) LLMと型チェックと具体的な実行を組み合わせたワークフローを設計し、違反証人(反例)を生成し検証する。 重要なアイデアは、抽象型の(存在量化されている)変数で仕様をSolidityテストとして表現することであり、これらの変数を(正しい型の)具体的な値にインスタンス化することで、ターゲットプロパティの実行可能な反例(PoC)にテストを拡大する。 我々はNeuroforgerのツールにこの手順を実装し,文献から抽出したスマートコントラクト検証データセットを用いて実験的に評価し,本手法の適用可能性を示す有望な結果を得た。

関連論文リスト

• Faithful Autoformalization of Natural Language Assertions [2.8921494813790094]
  Monty: アサーションのための自動形式化フレームワークを紹介します。 本手法は,新しい適合度測定値を用いたフィルタリング形式化に基づく。 提案手法は,LLMを用いてアサーションの翻訳を行う場合よりも,基礎的真理を確実に生成することを示す。
  論文  参考訳（メタデータ） (2026-07-14T22:12:14Z)
• ClarifyCodeBench: Evaluating LLMs on Clarifying Ambiguous Requirements for Code Generation [54.788849448970154]
  我々はClarifyCodeBenchを紹介した。ClarifyCodeBenchは、要求のあいまいさを解決するためのLarge Language Modelsの機能を評価するための、インタラクティブなベンチマークだ。 ClarifyCodeBenchを用いて、6つの最先端LCMの体系的評価を行う。 1) 能力の疎結合: 強いコード生成性能は本質的には効果的な要求の明確化に変換されない; 2) 推論パラドックス: 計算思考の増大はコードの正確性を高めるが、あいまいさの識別において限界的な利益をもたらす。
  論文  参考訳（メタデータ） (2026-07-01T09:58:59Z)
• VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents [57.240036084348354]
  本稿では,ロボットスキルコントラクトの検証誘導自己進化のためのフレームワークであるVASOを紹介する。 VASOは論理的に一貫性のないスキル契約を検証し、グローバルおよびローカルな時間的仕様に対してスキルによって誘発される計画を検証する。 Clearpath Jackal と PX4 のクアッドコプタータスクでは、VASO は100点未満の最適化サンプルを使用して97.2% の形式的な仕様準拠に達した。
  論文  参考訳（メタデータ） (2026-06-03T20:02:35Z)
• LLM-Based Static Verification of Code Against Natural-Language Requirements: An Industrial Experience Report [3.5867640049033054]
  本稿では,この課題に対処するための2段階のLLMベースのワークフローを,インテリジェント車両サイバーセキュリティケーススタディで紹介する。 第一段階では、AIベースのルールマイナーが自然言語要求から検証可能なルールを抽出する。 第2段階では、AIベースのコード監査者が、抽出されたルールに対する実装証拠をチェックする。
  論文  参考訳（メタデータ） (2026-05-18T06:34:03Z)
• A2RBench: An Automatic Paradigm for Formally Verifiable Abstract Reasoning Benchmark Generation [59.98516959731531]
  抽象推論能力は、抽象ルールを抽出し適用するためのLLMの知性と能力を反映する。 既存のベンチマークは、高価な手作業のアノテーション、そのスケールの制限、あるいは真の推論ではなく暗記のリスク測定に頼っている。 我々はA2RBenchという名の自動パイプラインを導入し、生成、拡張、評価、分析を行う。
  論文  参考訳（メタデータ） (2026-05-17T06:14:20Z)
• Small Language Model Helps Resolve Semantic Ambiguity of LLM Prompt [13.863963355859175]
  本稿では、明示的なプロンプト曖昧化による事前推論プロンプト最適化機構を提案する。 我々は、プロンプト内のセマンティックリスクを特定し、それらのマルチパースペクティブ一貫性を確認し、セマンティックコンフリクトを解決する。 本手法は, 推理性能を0.02ドルで2.5ポイント向上させる。
  論文  参考訳（メタデータ） (2026-04-25T12:13:26Z)
• Improving Dynamic Specification Inference with LLM-Generated Counterexamples [3.555888578860533]
  本稿では,生成したアサーションを無効にしようとするテストを自動的に生成する大規模言語モデル(LLM)について検討する。 その結果,現在最先端のLCMは,SpecFuzzerが推定する無効なアサーションの最大11.68%を破棄する有効な反例を生成できることがわかった。
  論文  参考訳（メタデータ） (2026-04-12T18:09:53Z)
• Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification? [1.9551668880584971]
  大規模言語モデル(LLM)は、自然言語のヒントから正式な後条件を推測する際の約束を示す。 NL2Contractは,非公式な自然言語を形式的関数型コントラクトに変換するためにLLMを使用するタスクである。 NL2Contract with different LLMs and compared it to the task of postcondition generation nl2postcond。
  論文  参考訳（メタデータ） (2025-10-14T16:37:39Z)
• Aligning Large Language Models for Faithful Integrity Against Opposing Argument [71.33552795870544]
  大規模言語モデル(LLM)は複雑な推論タスクにおいて印象的な機能を示している。 原文が正しい場合でも、会話中に不誠実な議論によって容易に誤解される。 本稿では,信頼度と信頼度を両立させる新しい枠組みを提案する。
  論文  参考訳（メタデータ） (2025-01-02T16:38:21Z)
• Aligning Language Models to Explicitly Handle Ambiguity [22.078095273053506]
  我々は,あいまいなクエリを扱うために,言語モデルを整列する新しいパイプラインであるAlignment with Perceived Ambiguity (APA)を提案する。 質問応答データセットの実験結果から、APAはLLMに対して、あいまいなクエリを明示的に検出し、管理する権限を持つことが示された。 我々の発見は、APAがゴールドスタンダードラベルのトレーニング、特にアウト・オブ・ディストリビューションのシナリオで優れていることを証明している。
  論文  参考訳（メタデータ） (2024-04-18T07:59:53Z)
• Uncertainty Quantification for In-Context Learning of Large Language Models [52.891205009620364]
  大規模言語モデル(LLM)の画期的な能力として、文脈内学習が登場している。 両タイプの不確かさを定量化するための新しい定式化法とそれに対応する推定法を提案する。 提案手法は、プラグイン・アンド・プレイ方式でコンテキスト内学習の予測を理解するための教師なしの方法を提供する。
  論文  参考訳（メタデータ） (2024-02-15T18:46:24Z)
• Which Syntactic Capabilities Are Statistically Learned by Masked Language Models for Code? [51.29970742152668]
  精度に基づく測定に依存することで、モデルの能力が過大評価される可能性があることを強調する。 これらの問題に対処するために,SyntaxEval in Syntactic Capabilitiesというテクニックを導入する。
  論文  参考訳（メタデータ） (2024-01-03T02:44:02Z)
• ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
  本稿では,LLMベースのフレームワークであるReEvalについて述べる。 本稿では、ChatGPTを用いてReEvalを実装し、2つの人気のあるオープンドメインQAデータセットのバリエーションを評価する。 我々の生成したデータは人間可読であり、大きな言語モデルで幻覚を引き起こすのに役立ちます。
  論文  参考訳（メタデータ） (2023-10-19T06:37:32Z)

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

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