論文の概要: Verified invertible lexer using regular expressions and DFAs
- arxiv url: http://arxiv.org/abs/2412.13581v1
- Date: Wed, 18 Dec 2024 08:03:17 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-12-19 16:48:24.295973
- Title: Verified invertible lexer using regular expressions and DFAs
- Title（参考訳）: 正規表現とDFAを用いた検証可逆レキサ
- Authors: Samuel Chassot, Viktor Kunčak,
- Abstract要約: 本稿では,シリアライズおよびレキシングフレームワークに適用する可逆性の概念について検討する。
シリアライゼーションはデータ構造をビット配列に書き込むプロセスであり、レキシングは文字のストリームを読み取ってトークンに分割するプロセスである。
- 参考スコア（独自算出の注目度）: 0.0
- License:
- Abstract: In this project, we explore the concept of invertibility applied to serialisation and lexing frameworks. Recall that, on one hand, serialisation is the process of taking a data structure and writing it to a bit array while parsing is the reverse operation, i.e., reading the bit array and constructing the data structure back. While lexing, on the other hand, is the process of reading a stream of characters and splitting them into tokens, by following a list of given rules. While used in different applications, both are similar in their abstract operation: they both take a list of simple characters and extract a more complex structure. Applications in which these two operations are used are different but they share a need for the invertibility of the process. For example, when tokenising a code file that was prettyprinted by a compiler, one would expect to get the same sequence of tokens. Similarly, when a spacecraft sends scientific data to the ground, one would expect the parsed data to be the same as the one serialised by the spacecraft. The idea of this project is to explore the idea of having a framework capable of generating parser/serialiser or lexer/prettyprinter pairs with a formally verified notion of invertibility. We first explore related works and frameworks. After that, we present our verified lexer framework developed in Scala and verified using the Stainless framework1. We explain the implementation choices we make and present the specifications and their proofs. The code of the lexer with the proofs is available on Github2. The main branch contains the regular expression (called regex from now on) matcher version and the verified Computable Languages while the dfa match branch contains the version using the DFA matcher.
- Abstract（参考訳）: 本稿では,シリアライズおよびレキシングフレームワークに適用する可逆性の概念について検討する。
一方、シリアライゼーションはデータ構造を取り、解析しながらビット配列に書き込むプロセスであり、逆の操作である、すなわちビット配列を読み、データ構造を逆に構築するプロセスである。
一方、レキシングは、与えられたルールのリストに従うことによって、文字のストリームを読み、トークンに分割するプロセスである。
異なるアプリケーションで使われているが、どちらも抽象的な操作で似ており、単純な文字のリストを取り、より複雑な構造を抽出する。
これら2つの操作が使用されるアプリケーションは異なるが、プロセスの可逆性の必要性を共有している。
例えば、コンパイラによってきれいに印刷されたコードファイルのトークン化では、同じトークンのシーケンスが期待されます。
同様に、宇宙船が地上に科学的データを送信した場合、解析されたデータは宇宙船によってシリアライズされたものと同一であると期待される。
このプロジェクトの目的は、正式に証明された可逆性の概念でパーサー/セリザーまたはレキサ/プレティプリンダーペアを生成することができるフレームワークを持つことを探求することである。
まず、関連する作業とフレームワークについて調べる。
その後、Scalaで開発された検証されたレキサフレームワークを示し、ステンレスフレームワーク1を使って検証する。
実装の選択肢を説明し、仕様とその証明を示します。
証明付きのレキサのコードはGithub2で公開されている。
メインブランチには、正規表現(現在からregexと呼ばれる)と検証可能な計算可能言語が含まれており、dfaマッチブランチには、DFAマッチングを使用したバージョンが含まれている。
関連論文リスト
- StrTune: Data Dependence-based Code Slicing for Binary Similarity Detection with Fine-tuned Representation [5.41477941455399]
BCSDは、悪意のあるコードスニペットの識別や、コードパターンの比較によるバイナリパッチ解析といったバイナリタスクに対処することができる。
バイナリは異なるコンパイル構成でコンパイルされるため、既存のアプローチはバイナリの類似性を比較する際にも注目すべき制限に直面している。
データ依存に基づいてバイナリコードをスライスし,スライスレベルの微調整を行うStrTuneを提案する。
論文 参考訳（メタデータ） (2024-11-19T12:20:08Z) - LILO: Learning Interpretable Libraries by Compressing and Documenting Code [71.55208585024198]
LILOは、反復的に合成、圧縮、文書化を行う、ニューロシンボリックなフレームワークである。
LILOは、LLM誘導プログラム合成と、Stitchから自動化された最近のアルゴリズムの進歩を組み合わせたものである。
LILOのシンセサイザーが学習した抽象化を解釈し、デプロイするのを手助けすることで、AutoDocがパフォーマンスを向上させることが分かりました。
論文 参考訳（メタデータ） (2023-10-30T17:55:02Z) - Lexinvariant Language Models [84.2829117441298]
離散語彙記号から連続ベクトルへの写像であるトークン埋め込みは、任意の言語モデル(LM)の中心にある
我々は、語彙記号に不変であり、したがって実際に固定トークン埋め込みを必要としないテクスチトレキシン変種モデルについて研究する。
十分長い文脈を条件として,レキシン変項LMは標準言語モデルに匹敵する難易度が得られることを示す。
論文 参考訳（メタデータ） (2023-05-24T19:10:46Z) - Linear-Time Modeling of Linguistic Structure: An Order-Theoretic
Perspective [97.57162770792182]
文字列内のトークンのペア間の関係をモデル化するタスクは、自然言語を理解する上で不可欠な部分である。
これらの徹底的な比較は避けられ、さらに、トークン間の関係を文字列上の部分順序としてキャストすることで、複雑さを線形に減らすことができる。
提案手法は,文字列中の各トークンの実際の数を並列に予測し,それに従ってトークンをソートすることで,文字列内のトークンの総順序を決定する。
論文 参考訳（メタデータ） (2023-05-24T11:47:35Z) - Outline, Then Details: Syntactically Guided Coarse-To-Fine Code
Generation [61.50286000143233]
ChainCoderは、Pythonコードを段階的に生成するプログラム合成言語モデルである。
自然言語記述と構文的に整合したI/Oデータサンプルを共同で符号化するために、カスタマイズされたトランスフォーマーアーキテクチャを利用する。
論文 参考訳（メタデータ） (2023-04-28T01:47:09Z) - What Are You Token About? Dense Retrieval as Distributions Over the
Vocabulary [68.77983831618685]
本稿では,2つのエンコーダが生成するベクトル表現を,モデルの語彙空間に投影することで解釈する。
得られたプロジェクションは、リッチな意味情報を含み、それらの間の接続を描画し、スパース検索を行う。
論文 参考訳（メタデータ） (2022-12-20T16:03:25Z) - InCoder: A Generative Model for Code Infilling and Synthesis [88.46061996766348]
InCoderは、プログラム合成(左から右への生成)と編集(埋め込み)が可能な統合生成モデルである。
InCoderは、許可されたコードの大きなコーパスからコードファイルを生成するように訓練されている。
私たちのモデルは、ゼロショットコードの埋め込みを直接実行できる最初の生成モデルです。
論文 参考訳（メタデータ） (2022-04-12T16:25:26Z) - Learning to Look Inside: Augmenting Token-Based Encoders with
Character-Level Information [29.633735942273997]
XRayEmbは、既存のトークンベースのモデルに文字レベルの情報を適合させる手法である。
我々は,XRayEmbの学習ベクトルを事前学習されたトークン埋め込みのシーケンスに組み込むことで,自己回帰型およびマスク付き事前学習されたトランスフォーマーアーキテクチャの性能を向上させることを示す。
論文 参考訳（メタデータ） (2021-08-01T08:09:26Z) - Assessing the Effectiveness of Syntactic Structure to Learn Code Edit
Representations [2.1793134762413433]
ソースコード編集の表現には抽象構文木(AST)の構造情報を用いる。
code2seqアプローチに触発されて,ASTの構造情報の利用がコード編集のタスクにどのように役立つかを評価する。
論文 参考訳（メタデータ） (2021-06-11T01:23:07Z) - A Unifying Theory of Transition-based and Sequence Labeling Parsing [14.653008985229617]
文を左から右へ読み取る遷移に基づく構文解析アルゴリズムを,構文木をエンコードするシーケンスラベリングアルゴリズムにマップする。
これにより、トランジションベースの構文解析とシーケンスラベル解析の理論的関係が確立される。
4つのアルゴリズムのシーケンスラベリングバージョンを実装し、学習可能であり、既存のエンコーディングに匹敵する性能が得られることを示す。
論文 参考訳（メタデータ） (2020-11-01T18:25:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。