論文の概要: 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
- arxiv url: http://arxiv.org/abs/2404.10362v2
- Date: Mon, 6 May 2024 23:21:57 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-08 19:03:36.676017
- Title: 3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
- Title（参考訳）: 3DGen:AIによる、おそらく正しいバイナリフォーマットパーザの生成
- Authors: Sarah Fakhoury, Markus Kuppe, Shuvendu K. Lahiri, Tahina Ramananandro, Nikhil Swamy,
- Abstract要約: 3DGenは、AIエージェントを使用して、混合非公式入力を3Dと呼ばれる言語でフォーマット仕様に変換するフレームワークである。
3DGenはテストスイートに準拠した3D仕様を生成する。
- 参考スコア（独自算出の注目度）: 5.102523342662388
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Improper parsing of attacker-controlled input is a leading source of software security vulnerabilities, especially when programmers transcribe informal format descriptions in RFCs into efficient parsing logic in low-level, memory unsafe languages. Several researchers have proposed formal specification languages for data formats from which efficient code can be extracted. However, distilling informal requirements into formal specifications is challenging and, despite their benefits, new, formal languages are hard for people to learn and use. In this work, we present 3DGen, a framework that makes use of AI agents to transform mixed informal input, including natural language documents (i.e., RFCs) and example inputs into format specifications in a language called 3D. To support humans in understanding and trusting the generated specifications, 3DGen uses symbolic methods to also synthesize test inputs that can be validated against an external oracle. Symbolic test generation also helps in distinguishing multiple plausible solutions. Through a process of repeated refinement, 3DGen produces a 3D specification that conforms to a test suite, and which yields safe, efficient, provably correct, parsing code in C. We have evaluated 3DGen on 20 Internet standard formats, demonstrating the potential for AI-agents to produce formally verified C code at a non-trivial scale. A key enabler is the use of a domain-specific language to limit AI outputs to a class for which automated, symbolic analysis is tractable.
- Abstract（参考訳）: 特にプログラマがRFCの非公式な形式記述を低レベルのメモリアンセーフな言語で効率的に解析するロジックに書き起こす場合である。
何人かの研究者が、効率的なコードを抽出できるデータフォーマットの正式な仕様言語を提案している。
しかし、非公式な要件を形式的な仕様に抽出することは困難であり、その利点にもかかわらず、新しい形式言語は人々が学び、使うのが難しい。
本稿では,AIエージェントを用いて自然言語文書(RFC)やサンプル入力を3Dと呼ばれる言語でフォーマット仕様に変換する3DGenを提案する。
生成された仕様を理解し信頼するために、3DGenはシンボリックメソッドを使用して、外部のオラクルに対して検証可能なテストインプットを合成する。
シンボリックテスト生成は、複数の可算解の区別にも役立つ。
我々は、20のインターネット標準フォーマットで3DGenを評価し、AIエージェントが公式に認証されたCコードを非自明なスケールで生成する可能性を実証した。
重要なイネーブルは、AI出力を、自動化されたシンボリック分析が抽出可能なクラスに制限するために、ドメイン固有の言語を使用することである。
関連論文リスト
- Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
形式言語理論は、特に認識者に関するものである。
代わりに、非公式な意味でのみ類似したプロキシタスクを使用するのが一般的である。
ニューラルネットワークを文字列のバイナリ分類器として直接訓練し評価することで、このミスマッチを補正する。
論文 参考訳（メタデータ） (2024-11-11T16:33:25Z) - Automatic deductive coding in discourse analysis: an application of large language models in learning analytics [5.606202114848633]
GPTのような大規模言語モデルの出現は、自動演能符号化のための新たな道を開いた。
我々は、異なる人工知能技術によって駆動される3つの異なる分類手法を採用した。
その結果,GPTは両方のデータセットにおいて,トレーニングサンプル数に制限のある他の2つの手法よりも優れていた。
論文 参考訳（メタデータ） (2024-10-02T05:04:06Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳（メタデータ） (2024-06-14T06:52:08Z) - Decoding at the Speed of Thought: Harnessing Parallel Decoding of Lexical Units for LLMs [57.27982780697922]
大規模言語モデルは、自然言語の理解と生成において例外的な能力を示した。
しかし、それらの生成速度は、その復号過程の本質的にシーケンシャルな性質によって制限される。
本稿では,データ駆動方式で実装された新しいデコーディング手法であるLexical Unit Decodingを紹介する。
論文 参考訳（メタデータ） (2024-05-24T04:35:13Z) - FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。
まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。
次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
論文 参考訳（メタデータ） (2024-03-27T09:45:33Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳（メタデータ） (2023-09-25T15:42:18Z) - From Ambiguity to Explicitness: NLP-Assisted 5G Specification
Abstraction for Formal Analysis [5.526122280732959]
我々はNLPツールを用いてデータを構築し、構築されたデータを用いて識別子と形式的特性を抽出する2段階パイプラインを提案する。
最適モデルの結果は,抽出精度が39%,形式的特性の同定精度が42%に達している。
論文 参考訳（メタデータ） (2023-08-07T03:37:31Z) - Grammar-Constrained Decoding for Structured NLP Tasks without Finetuning [27.59524153097858]
文法制約付き復号法(GCD)は、大言語モデル(LM)の生成を制御するために用いられる。
GCDは一般に構造化NLPタスクの統一フレームワークとして機能する。
文法制約付きLMは、制約なしLMよりも大幅に優れるか、タスク固有の微調整モデルよりも優れていることを示す。
論文 参考訳（メタデータ） (2023-05-23T11:54:37Z) - Detecting Text Formality: A Study of Text Classification Approaches [78.11745751651708]
本研究は,統計的,ニューラルベース,トランスフォーマーベースの機械学習手法に基づく形式性検出手法の体系的研究を初めて行う。
単言語,多言語,言語横断の3種類の実験を行った。
本研究は,モノリンガルおよび多言語形式分類タスクのためのトランスフォーマーベースモデルに対するChar BiLSTMモデルの克服を示す。
論文 参考訳（メタデータ） (2022-04-19T16:23:07Z) - CGEMs: A Metric Model for Automatic Code Generation using GPT-3 [0.0]
本研究は,理論的証明を用いて,あるいはモンテカルロシミュレーション法を用いてAI生成コンテンツを検証することを目的とする。
この場合、後者の手法を用いて統計的にかなりの数のサンプルを検査・検証する。
コンパイル、ロジック変換へのNL記述、必要な編集数、一般的に使用されている静的コードメトリクスとNLPメトリクス。
論文 参考訳（メタデータ） (2021-08-23T13:28:57Z) - Zero-Shot Cross-lingual Semantic Parsing [56.95036511882921]
7つのテスト言語に対する並列データを持たないゼロショット問題として,言語間セマンティックパーシングについて検討した。
英文論理形式ペアデータのみを用いて解析知識を付加言語に転送するマルチタスクエンコーダデコーダモデルを提案する。
このシステムは、ゼロショット解析を潜時空間アライメント問題としてフレーム化し、事前訓練されたモデルを改善し、最小のクロスリンガル転送ペナルティで論理形式を生成することができる。
論文 参考訳（メタデータ） (2021-04-15T16:08:43Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。