論文の概要: Verified Reversible Programming for Verified Lossless Compression

• arxiv url: http://arxiv.org/abs/2211.09676v1
• Date: Wed, 2 Nov 2022 16:39:41 GMT
• ステータス: 処理完了
• システム内更新日: 2022-11-20 13:50:53.400887
• Title: Verified Reversible Programming for Verified Lossless Compression
• Title（参考訳）: 検証可逆プログラムによるロスレス圧縮の検証
• Authors: James Townsend and Jan-Willem van de Meent
• Abstract要約: ロスレス圧縮の実装は通常、エンコーダとデコーダの2つのプログラムを含む。 我々は、非対称数値システム(ANS)に基づく圧縮手法のかなりのクラスが、エンコーダとデコーダの間で共有構造を持つことを観察する。 私たちはAgdaに埋め込まれた小さな可逆言語「Flipper」を実装しました。
• 参考スコア（独自算出の注目度）: 11.020543186794459
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Lossless compression implementations typically contain two programs, an encoder and a decoder, which are required to be inverse to one another. Maintaining consistency between two such programs during development requires care, and incorrect data decoding can be costly and difficult to debug. We observe that a significant class of compression methods, based on asymmetric numeral systems (ANS), have shared structure between the encoder and decoder -- the decoder program is the 'reverse' of the encoder program -- allowing both to be simultaneously specified by a single, reversible, 'codec' function. To exploit this, we have implemented a small reversible language, embedded in Agda, which we call 'Flipper'. Agda supports formal verification of program properties, and the compiler for our reversible language (which is implemented as an Agda macro), produces not just an encoder/decoder pair of functions but also a proof that they are inverse to one another. Thus users of the language get formal verification 'for free'. We give a small example use-case of Flipper in this paper, and plan to publish a full compression implementation soon.
• Abstract（参考訳）: ロスレス圧縮の実装は、典型的にはエンコーダとデコーダという2つのプログラムを含んでいる。 開発中の2つのプログラム間の一貫性を維持するには注意が必要だ。 我々は、非対称数値システム(ANS)に基づく圧縮手法のかなりのクラスが、エンコーダとデコーダの間で共有構造を持つことを観察し、デコーダプログラムはエンコーダプログラムの「逆」であり、どちらも単一の可逆な「コーダc」関数で同時に指定できる。 これを利用するために、私たちはAgdaに埋め込まれた小さな可逆言語を実装しました。 Agdaはプログラムプロパティの形式的検証をサポートし、(Agdaマクロとして実装されている)可逆言語用のコンパイラは、エンコーダ/デコーダのペア関数を生成するだけでなく、それらが互いに逆であることを示す。 したがって、この言語のユーザは'無料で'正式な検証を受ける。 本稿では、Flipperのユースケースを例に挙げ、近く完全な圧縮実装を公開する計画である。

関連論文リスト

• Cryptographic Compression [0.8057006406834466]
  我々はENCOREと呼ばれるプロトコルを導入し、ワンパスプロセスでデータを同時に圧縮して暗号化する。 我々は、マルコフモデルの出力により、少なくとも安定な分布を持つ典型的な'データに対して、これらを同時に行うことができることを示す。 戦略は、ハフマン符号化が一様に近いダイアド分布にデータを変換し、そのデータに対する変換を圧縮された二次ストリームに格納する。
  論文  参考訳（メタデータ） (2025-01-27T16:32:08Z)
• Better Prompt Compression Without Multi-Layer Perceptrons [33.53334153279698]
  本稿では,エンコーダが本来の言語モデルのアーキテクチャを維持して有用な圧縮を実現する必要はないことを示す。 言語モデルのトランスフォーマーブロックにおいて,多層パーセプトロン(MLP)層を除去した後に,プロンプト圧縮エンコーダを導入する。
  論文  参考訳（メタデータ） (2025-01-12T06:57:06Z)
• Generalizing the matching decoder for the Chamon code [1.8416014644193066]
  チャモン符号として知られる3次元,非CSS,低密度のパリティチェックコードに対して,マッチングデコーダを実装した。 一般化された整合デコーダは、整合前に信念伝播ステップによって拡張され、偏極雑音に対するしきい値が10.5%となる。
  論文  参考訳（メタデータ） (2024-11-05T19:00:12Z)
• Progressive-Proximity Bit-Flipping for Decoding Surface Codes [8.971989179518214]
  トリックやサーフェスコードのようなトポロジカル量子コードは、ハードウェア実装の優れた候補である。 既存のデコーダは、計算複雑性の低いような要求を満たすのに不足することが多い。 トリックおよび表面符号に適した新しいビットフリップ(BF)デコーダを提案する。
  論文  参考訳（メタデータ） (2024-02-24T22:38:05Z)
• Estimating the Decoding Failure Rate of Binary Regular Codes Using Iterative Decoding [84.0257274213152]
  並列ビットフリップデコーダのDFRを高精度に推定する手法を提案する。 本研究は,本症候群のモデル化およびシミュレーションによる重み比較,第1イテレーション終了時の誤りビット分布の誤検出,復号化復号化率(DFR)について検証した。
  論文  参考訳（メタデータ） (2024-01-30T11:40:24Z)
• SparseCoder: Identifier-Aware Sparse Transformer for File-Level Code Summarization [51.67317895094664]
  本稿では,大規模なソースコードプロジェクトの理解と維持を支援するファイルレベルのコード要約について検討する。 長いコードシーケンスを効果的に処理するための識別子対応スパース変換器であるSparseCoderを提案する。
  論文  参考訳（メタデータ） (2024-01-26T09:23:27Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• Pre-Training Transformer Decoder for End-to-End ASR Model with Unpaired Speech Data [145.95460945321253]
  本稿では,音響単位,すなわち擬似符号を用いたエンコーダ・デコーダネットワークのための2つの事前学習タスクを提案する。 提案したSpeech2Cは,デコーダを事前学習することなく,単語誤り率(WER)を19.2%削減できる。
  論文  参考訳（メタデータ） (2022-03-31T15:33:56Z)
• Trans-Encoder: Unsupervised sentence-pair modelling through self- and mutual-distillations [22.40667024030858]
  バイエンコーダは固定次元の文表現を生成し、計算効率が良い。 クロスエンコーダは、アテンションヘッドを利用して、より優れたパフォーマンスのために文間相互作用を利用することができる。 Trans-Encoderは、2つの学習パラダイムを反復的なジョイントフレームワークに統合し、拡張されたバイ・エンコーダとクロス・エンコーダを同時に学習する。
  論文  参考訳（メタデータ） (2021-09-27T14:06:47Z)
• Dense Coding with Locality Restriction for Decoder: Quantum Encoders vs. Super-Quantum Encoders [67.12391801199688]
  我々は、デコーダに様々な局所性制限を課すことにより、濃密な符号化について検討する。 このタスクでは、送信者アリスと受信機ボブが絡み合った状態を共有する。
  論文  参考訳（メタデータ） (2021-09-26T07:29:54Z)
• On Sparsifying Encoder Outputs in Sequence-to-Sequence Models [90.58793284654692]
  我々はTransformerをテストベッドとして、エンコーダとデコーダの間にあるゲートの層を導入します。 ゲートは、パリシティ誘導L0ペナルティの期待値を用いて正規化される。 このスペーサー化が2つの機械翻訳と2つの要約タスクに与える影響について検討する。
  論文  参考訳（メタデータ） (2020-04-24T16:57:52Z)

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

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