Nov, 2022

验证可逆编程用于验证无损压缩

PDF
TL;DR本文介绍了一种基于对称数字系统的无损压缩方法，特别是它们共享编码器和解码器之间的结构，使得可以使用单一可逆函数同时指定两者。我们提出了一种可逆语言 Flipper，它嵌入在 Agda 中，以支持对程序属性的形式化验证。通过 Flipper，用户不仅可以获得加密 / 解密函数对，还可以获得它们互为逆的证明。本文给出了一个 Flipper 的小例子，计划很快发布一个完整的压缩实现。
lossless compressionasymmetric numeral systemreversible languageformal verificationencoder/decoder
发现论文，激发创造
  • Jeopardy: 可逆的函数式编程语言

    本文介绍了一种名为 Jeopardy 的函数式编程语言，它可以在不实施局部可逆的限制下保证程序可逆性，并且通过一系列方法来解决保证可逆性的通常困难问题，其中一个方法是隐含可用参数分析。

    Sep, 2022

  • Bit-Swap: 递归位回推编码用于层次化潜在变量无损压缩

    本研究提出了一种新的压缩方案 Bit-Swap，用于实现具有 Markov 链结构的分层隐变量模型的失真压缩，实验表明此方案比现有技术更加优越。

    May, 2019

  • iFlow: 通过统一编码器实现数值反转流的高效无损压缩

    本文介绍了使用归一化流实现高效无损压缩的新方法 iFlow, 该方法基于模块化缩放变换提出了一系列数值可逆流变换，同时引入了 Uniform Base Conversion System（UBCS）实现快速均匀分布编码，iFlow 实现了最先进的压缩比，并且比其他高性能方案快 5 倍。

    Nov, 2021

  • 使用 Bits Back 编码和潜在变量进行实用的无损压缩

    我们提出了一种名为 BB-ANS 的方案，用于在潜在变量模型中进行无损压缩，通过使用变分自动编码器模型来压缩 MNIST 数据集，实现了比标准方法更高的压缩率。

    Jan, 2019

  • iVPF：数值可逆守恒体积流用于高效无损压缩

    本文研究体积保持流用于无损压缩，并提出了数值可逆体积保持流 (iVPF)。实验结果表明，基于 iVPF 的算法在轻量级压缩算法中达到了业内领先的压缩比

    Mar, 2021

  • 基于局部比特回传编码的压缩流

    本文提出了一种用于流模型的新的压缩技术 —— 局部 Bits-Back 编码，并为许多流模型提供了高效的算法来实现该技术，实验表明该算法可以实现先进的流模型在高维数据上的理论码率。

    May, 2019

  • IDF++：整数离散流的分析与改进以实现无损压缩

    本文研究和改进针对无损压缩的整数离散流。我们通过探究离散随机变量的可逆流是否比连续随机变量的更为灵活来开始分析，并通过证明发现此理论不适用于整数离散流。此外，我们研究了整数离散流中的梯度偏差效应，并通过实验证明其对模型的性能影响高度依赖于架构选择并不像先前想象的那样突出。最后，我们展示了不同架构修改如何改进该模型类别的性能并使其更加高效：我们发现具有一半数量流层的模型性能不亚于或者比原始整数离散流模型更好。

    Jun, 2020

  • 从 Llama2 7B 权重的无损（~1.5:1）压缩算法到 CNNs 和 LLMs 的可变精度、可变范围、压缩数值数据类型

    这篇论文介绍了一种简单的无损压缩算法，用于处理大型语言模型的权重，可在 AMD FPGAs 中实现，并能每秒处理超过 8 亿个 bfloat16 数字。该算法被扩展应用于可变精度、可变范围的数值数据类型，并讨论了基于 ANS（非对称数系统）的硬件实现方法，该方法在实现数据格式的灵活性和计算引擎之间起到了桥梁作用，并实现了带宽的降低。同时，还给出了使用权重压缩和共享的令牌生成器的示例。

    Apr, 2024

  • 非对称数字系统：将 Huffman 编码的速度与算术编码的压缩比结合的熵编码

    这篇论文讨论了数据压缩中两种熵编码方法的优缺点，并介绍了一种新的方法 —— 非对称数字系统熵编码，它可以在保证压缩率的同时提高解码速度，相当于在速度和效率之间找到了平衡点。

    Nov, 2013

  • LEVER: 学习使用执行验证从语言生成代码

    本研究提出了一种基于语言到代码生成的方法，利用预先训练好的代码语言模型的采样程序生成，再利用后验验证器对生成的程序进行验证，对程序进行重新排序，从而提高最终程序的正确性，实验结果表明该方法在多个领域取得了最优的生成效果。

    Feb, 2023