論文の概要: 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のユースケースを例に挙げ、近く完全な圧縮実装を公開する計画である。

関連論文リスト

• Generalizing the matching decoder for the Chamon code [1.8416014644193066]
  チャモン符号として知られる3次元,非CSS,低密度のパリティチェックコードに対して,マッチングデコーダを実装した。 一般化された整合デコーダは、整合前に信念伝播ステップによって拡張され、偏極雑音に対するしきい値が10.5%となる。
  論文  参考訳（メタデータ） (2024-11-05T19:00:12Z)
• Collective Bit Flipping-Based Decoding of Quantum LDPC Codes [0.6554326244334866]
  可変次数-3(dv-3)QLDPC符号の繰り返し復号化による誤り訂正性能と復号遅延の両方を改善した。 我々の復号方式は、ビットフリップ(BF)デコーディングの修正版、すなわち2ビットビットフリップ(TBF)デコーディングを適用することに基づいている。
  論文  参考訳（メタデータ） (2024-06-24T18:51:48Z)
• Progressive-Proximity Bit-Flipping for Decoding Surface Codes [8.971989179518214]
  トリックやサーフェスコードのようなトポロジカル量子コードは、ハードウェア実装の優れた候補である。 既存のデコーダは、計算複雑性の低いような要求を満たすのに不足することが多い。 トリックおよび表面符号に適した新しいビットフリップ(BF)デコーダを提案する。
  論文  参考訳（メタデータ） (2024-02-24T22:38:05Z)
• Triple-Encoders: Representations That Fire Together, Wire Together [51.15206713482718]
  コントラスト学習(Contrastive Learning)は、バイエンコーダを介して発話間の相対距離を埋め込み空間に符号化する表現学習法である。 本研究では,これら独立に符号化された発話から分散発話混合物を効率よく計算する三重エンコーダを提案する。 トリプルエンコーダはバイエンコーダよりも大幅に改善され、シングルベクトル表現モデルよりもゼロショットの一般化が向上することがわかった。
  論文  参考訳（メタデータ） (2024-02-19T18:06:02Z)
• 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)

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

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