Paper deep dive
Lossless Tensor Compression as Program Synthesis
Jieke Shi, Junda He, Wenjia Jiang, Weifeng Sun, Shidong Pan, Zhensu Sun, Chengran Yang, Peixin Zhang, Yifan Jia, Zhou Yang, Thong Hoang, Xiwei Xu, Zhenchang Xing, David Lo
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Model checkpoints are growing in both number and size, which makes archival, transfer, and deployment increasingly costly. General-purpose compressors can reduce storage requirements but ignore tensor structure, whereas existing tensor-specific compressors rely on fixed and format-specific pipelines. We present Brevis, which formulates lossless tensor compression as program synthesis. We design a typed domain-specific language (DSL) that captures recurring tensor structures, such as repeated regions and floating-point fields, through a set of reversible operators. Given a tensor, Brevis synthesizes a self-contained DSL program that reconstructs it bit-exactly. A checkpoint-specific production prior, learned from a small representative sample of tensors, guides a bounded A* search to synthesize compact programs, which can later be executed directly for bit-exact decompression. On 10 public checkpoints spanning language, audio, and image generation models, Brevis reduces 2.13 TB of checkpoint data to 1.41 TB, a 33.93% storage reduction. It produces archives up to 30.87% smaller than those of four general-purpose compressors, including zstd and gzip, and smaller archives than the tensor-specific compressors ZipNN and DFloat11. Under a practical concurrency configuration, Brevis achieves 3.60 GB/s compression and 6.61 GB/s decompression while preserving every source byte.
Tags
Links
- Source: https://arxiv.org/abs/2608.02162v1
- Canonical: https://arxiv.org/abs/2608.02162v1
Trouble viewing inline? Open PDF directly →
Full Text
54,019 characters extracted from source content.
Expand or collapse full text
\@ACM@balancefalse Lossless Tensor Compression as Program Synthesis Jieke Shi jiekeshi@smu.edu.sg Singapore Management UniversitySingapore , Junda He jundahe.2022@smu.edu.sg Singapore Management UniversitySingapore , Wenjia Jiang wjjiang@smu.edu.sg Singapore Management UniversitySingapore , Weifeng Sun wfsun@smu.edu.sg Singapore Management UniversitySingapore , Shidong Pan shidong.pan@anu.edu.au CSIRO’sAustralia , Zhensu Sun zssun@smu.edu.sg Singapore Management UniversitySingapore , Chengran Yang cryang.2021@smu.edu.sg Singapore Management UniversitySingapore , Peixin Zhang pxzhang@smu.edu.sg AIDX TECH PTE LTDSingapore , Yifan Jia yifan.jia@aidxtech.com AIDX TECH PTE LTDSingapore , Zhou Yang zy25@ualberta.ca University of Alberta & Alberta Machine Intelligence InstituteCanada , Thong Hoang (James) James.Hoang@csiro.au CSIRO’sAustralia , Xiwei (Sherry) Xu Xiwei.Xu@csiro.au CSIRO’sAustralia , Zhenchang Xing Zhenchang.Xing@csiro.au CSIRO’sAustralia and David Lo davidlo@smu.edu.sg Singapore Management UniversitySingapore Abstract. Model checkpoints are growing in both number and size, which makes archival, transfer, and deployment increasingly costly. General-purpose compressors can reduce storage requirements but ignore tensor structure, whereas existing tensor-specific compressors rely on fixed and format-specific pipelines. We present Brevis, which formulates lossless tensor compression as program synthesis. We design a typed domain-specific language (DSL) that captures recurring tensor structures, such as repeated regions and floating-point fields, through a set of reversible operators. Given a tensor, Brevis synthesizes a self-contained DSL program that reconstructs it bit-exactly. A checkpoint-specific production prior, learned from a small representative sample of tensors, guides a bounded A* search to synthesize compact programs, which can later be executed directly for bit-exact decompression. On 10 public checkpoints spanning language, audio, and image generation models, Brevis reduces 2.13 TB of checkpoint data to 1.41 TB, a 33.93% storage reduction. It produces archives up to 30.87% smaller than those of four general-purpose compressors, including zstd and gzip, and smaller archives than the tensor-specific compressors ZipNN and DFloat11. Under a practical concurrency configuration, Brevis achieves 3.60 GB/s compression and 6.61 GB/s decompression while preserving every source byte. Introduction As large language models (LLMs) become increasingly capable and widely used, the number of publicly-available model repositories continues to grow rapidly. As shown in Figure 1(a), Hugging Face has grown from 425 publicly listed model repositories in April 2020 to 2.95 million today, hosting more than 15 petabytes (PB) of data (Fahlgren, 2026; Wang et al., 2026). Each repository may contain multiple large tensor checkpoints or revisions that are replicated across model hubs, storage systems, and deployment clusters. As model repositories continue to proliferate, the cost of archival, transfer, and deployment grows accordingly, making efficient compression increasingly important. (a) Repository growth (b) Compression tradeoff Figure 1. Growth in public model repositories and the compression tradeoff. (a) Hugging Face repositories (log scale). (b) Storage reduction versus compression throughput. Model compression can be broadly divided into lossy and lossless approaches. Lossy methods, such as quantization and pruning, reduce model size by modifying or discarding weight information (Frantar et al., 2023; Lin et al., 2024; Xu et al., 2025). They are designed for efficient inference and often require specific numerical formats (e.g., GGUF (Gerganov, 2026)) or execution environments, making them unsuitable for archival or exact checkpoint transfer because the original weights cannot be recovered bit exactly. In contrast, lossless compression preserves every source bit while reducing checkpoint size. General-purpose compressors, such as gzip and Zstandard (zstd), are widely used for storage and transmission but treat tensor weights as generic byte sequences, ignoring tensor-specific information such as dtypes, shapes, floating-point layouts, and relationships among elements. Model-specific compressors exploit common properties of floating-point tensors, such as redundancy in exponent fields (Hershcovitch et al., 2025; Zhang et al., 2025), while scientific-data compressors combine predefined transformations and codecs for floating-point arrays (Burtscher et al., 2016; Claggett et al., 2018; Rodriguez et al., 2024). Although effective, these methods rely on fixed compression schemes or predefined pipelines, which may fail to capture tensor-specific patterns such as repeated values, recurring subsequences, and simple relationships among elements. This limitation raises a natural question: rather than selecting a fixed compression scheme or predefined pipeline, can we synthesize a compact program that directly represents a tensor? Such a program serves as the compressed representation and can be executed to reconstruct the original tensor bit exactly. Since each tensor can use a different program, this formulation can capture tensor-specific structures. Realizing this idea introduces three challenges. First, the language must express diverse tensor structures while guaranteeing bit-exact reconstruction. Second, the program space is large, so the search must efficiently discover compact programs within a practical budget. Third, self-contained programs must remain compact despite the overhead of storing instructions, parameters, and literals required for reconstruction. We present Brevis, which addresses these challenges with a typed domain-specific language (DSL) whose reversible operators capture recurring tensor structures, including repeated values, subsequences, element relations, and floating-point fields, while exact literals provide a fallback for values that cannot be represented more compactly. During compression, Brevis learns a checkpoint-specific production prior, i.e., a probability distribution over DSL productions, from a small representative sample of tensors. This prior guides a novel bounded A* search that prioritizes promising program expansions and explores the search space within a search budget. Each complete candidate is evaluated by its exact serialized size, and the smallest synthesized program is selected for storage. During decompression, the synthesized program is executed directly for high-throughput bit-exact reconstruction, without requiring search or the learned prior. We evaluate Brevis on 10 public checkpoints spanning language, audio, and image generation models, three floating-point formats, 420 shards, and 2.13 TB of checkpoint data. Brevis produces the smallest archive on all 10 checkpoints against six baselines, reducing archive size by 12.94%-30.87% on average relative to four general-purpose compressors. Compared with the tensor-specific baselines ZipNN and DFloat11, Brevis produces archives up to 2.90% smaller and saves 10.53 GB in total. The improvements over all paired baselines remain statistically significant after Holm correction (pH=0.0098p_H=0.0098, rrb=1.0r_rb=1.0). Figure 1(b) shows the storage-throughput tradeoff, where Brevis reaches 3.60 GB/s compression and 6.61 GB/s decompression while lying on the Pareto frontier. This paper makes the following contributions: • We formulate bit-exact checkpoint compression as program synthesis, where each tensor is represented by a compact, self-contained DSL program that reconstructs the original tensor exactly. • We design a typed domain-specific language (DSL) with reversible operators that capture recurring tensor structures and element relationships. • We develop a bounded A* synthesis algorithm guided by a checkpoint-specific production prior learned from a small representative sample of tensors. • We evaluate Brevis on 10 public checkpoints totaling 2.13 TB of checkpoint data. Brevis significantly outperforms six baselines, producing the smallest archive on every checkpoint and reducing archive size by up to 30.87% over existing compressors. 1. Background and Related Work 1.1. Lossless Compression Given a tensor X and archive c, lossless compression requires (1) (c)=bitX,(X,c)=1−|c||X|, Decompress(c)=_bitX, Reduction(X,c)=1- |c||X|, where =bit=_bit denotes bitwise equality and |c||c| includes all data and metadata required for reconstruction. General-purpose codecs, such as gzip and Zstandard, combine dictionary matching, reversible transforms, and entropy coding but treat tensors as generic byte streams (Deutsch, 1996; Collet and Kucherawy, 2021). Float-aware preprocessing further exploits numerical structure through Bitshuffle, Typed Data Transformation (TDT), and ALP (Masui et al., 2015; Jamalidinan and Cheshmi, 2025; Afroozeh et al., 2023). These methods improve compression through fixed transformations or predefined codec families. Model-specific compressors exploit statistical properties of learned weights. ZipNN rearranges floating-point fields before lossless coding (Hershcovitch et al., 2025); DFloat11, ECF8, and ZipMoE target exponent distributions or model-specific layouts (Zhang et al., 2025; Yang et al., 2026c, b; Wang et al., 2026); Huff-LLM and tile-aligned ANS integrate entropy coding with efficient inference (Yubeaton et al., 2025; Tan et al., 2026); ZipServ, DFloat11, and ENEC further co-design representations with hardware decoders (Fan et al., 2026; Zhang et al., 2025; Yang et al., 2026a). In contrast, Brevis targets bit-exact archival by synthesizing a self-contained tensor program rather than selecting a predefined codec or hardware-specific representation. (X) Bits(X)the tensor as it sits on diskPPa short reversible program(X′)=(X) Bits(X )= Bits(X)every bit, not a tolerancesynthesiseexecute1Where the redundancy isvalues+1+1−1-1+1+1−1-1+1+1−1-1the same bits, read as ieee 754 fieldssign 11b010101Repeatexponent 88b127127127127127127Constfraction 2323b000000Const Each field is regular in its own way, so no single codec catches all three. 2A program is synthesised, not chosen Target-directed A∗A^*: a production is admitted only when its decomposition recomposes the hole’s exact target. LitConstConcatRepeatMapScanMergeP=fp32(3(1(0,1)),P= Merge_ fp32 ( Repeat_3( Lit_1(0,1)),8(127),23(0)) Const_8(127),\; Const_23(0) ) Ranked by the complete serialized size L(P)L(P), not by structure alone: structureparametersliteralstables Lit alone offers four physical encodings, picked by measured bytes. 3Decoding is execution(P) Exec(P)+1+1−1-1+1+1−1-1+1+1−1-1 BIT-EXACT signed zeros and nan payloads survive too No search at decode: the decoder validates P against the stored shape, then runs it. Figure 2. Compression as program synthesis in Brevis. Each tensor is represented by a short reversible program whose execution regenerates its bits exactly. (1) Read as IEEE 754 fields, 6 FP32 words expose 3 different regularities, and no single codec captures all of them. (2) Target-guided A∗A^* searches the typed grammar and ranks candidates by the complete serialized size L(P)L(P), which includes the literal payload and codec tables rather than the program structure. (3) Decoding validates P and executes it without search and without the learned prior; a universal Lit fallback keeps every supported tensor representable. 1.2. Lossy Tensor and Model Compression Lossy compression trades information for storage or execution efficiency. Quantization and pruning reduce model size by modifying weights (Frantar et al., 2023; Lin et al., 2024); LLM.265 repurposes video codecs for tensors (Xu et al., 2025); and NeuZip studies lossless training with near-lossless inference (Hao et al., 2024). These methods target inference efficiency rather than exact reconstruction, whereas Brevis focuses on bit-exact checkpoint archival. 1.3. Program Synthesis Program synthesis searches a program space P for a program that satisfies a specification ϕφ while minimizing a cost function Cost: (2) P∗∈argminP∈(P)s.t.ϕ(P,X).P^*∈ _P Cost(P) .t. φ(P,X). Syntax-guided synthesis restricts the search space with a grammar, while probability-guided methods prioritize likely productions (Alur et al., 2013). PHOG, Euphony, and TF-Coder learn production probabilities or operation priors to accelerate search (Bielik et al., 2016; Lee et al., 2018; Shi et al., 2022), and the KoLMogorov Test studies exact sequence generation through synthesized programs (Yoran et al., 2025). Compression systems have also synthesized floating-point algorithms or searched transformation pipelines, including OpenZL’s graph-based framework (Burtscher et al., 2016; Claggett et al., 2018; Rodriguez et al., 2024; Collet et al., 2025). Unlike these approaches, Brevis formulates tensor compression itself as program synthesis: the DSL defines the search space, exact reconstruction defines correctness, serialized program size defines the objective, and a checkpoint-specific prior guides bounded A* search. 2. Method 2.1. Overview and Problem Formulation Brevis represents each tensor as a typed, self-contained program whose execution reconstructs the original bits. Figure 2 summarizes the workflow. During compression, Brevis learns a checkpoint-specific production prior, i.e., a probability distribution over DSL productions, from a small deterministic sample of tensors. This prior guides bounded A* synthesis over a tensor-oriented grammar, while exact serialized size determines the selected program. Reversible operators expose repeated regions, element relationships, and low-entropy floating-point fields, while literal codecs encode the remaining streams. During decompression, the synthesized program is validated and executed directly without search or the learned prior. (a) Abstract Syntax Types and records τ τ ::=b[n], :=b[n] 24891 A A ::=⟨d,,P⟩. := d 24891 24891 P . Programs P::= P:= litb()∣constb,n(v)∣concat(P1,…,Pk) _b(v) _b 24891 n(v) (P_1 24891 … 24891 P_k) ∣repeatk(P)∣mapu,θ(P)∣scanq,θ(v0,P) _k(P) _u 24891 θ(P) _q 24891 θ(v_0 24891 P) ∣mergef,θ(P1,…,Pk). _f 24891 θ(P_1 24891 … 24891 P_k). (b) Well-Formedness ∈vWbn ≥n0 ⊢litb(v):b[n] 26.00235pt $ _b^n$ $ n≥ 0$ 26.00655pt $ _b(v):b[n]$ T-Lit ∈vWb ≥n1 ⊢constb,n(v):b[n] 26.80977pt $ v _b$ $ n≥ 1$ 34.91779pt $ _b 24891 n(v):b[n]$ T-Const ⊢Pi:b[ni](1≤i≤k) ≥k2 ≥ni1(1≤i≤k) =n∑=i1kni ⊢concat(P1,…,Pk):b[n] 126.24968pt $ P_i:b[n_i] (1≤ i≤ k)$ $ k≥ 2$ $ n_i≥ 1 (1≤ i≤ k)$ $ n= _i=1^kn_i$ 46.63763pt $ (P_1 24891 … 24891 P_k):b[n]$ T-Concat ⊢P:b[m] ≥k2 ≥m1 =nkm ⊢repeatk(P):b[n] 67.1851pt $ P:b[m]$ $ k≥ 2$ $ m≥ 1$ $ n=km$ 34.7771pt $ _k(P):b[n]$ T-Repeat ⊢P:b[n] ≥n1 uθ:Wb↔Wb ⊢mapu,θ(P):b[n] 59.37515pt $ P:b[n]$ $ n≥ 1$ $ u_θ:W_b _b$ 34.33842pt $ _u 24891 θ(P):b[n]$ T-Map ⊢P:b[-n1] ≥n2 ∈v0Wb ∀a∈Wb.qθ(a,⋅):Wb↔Wb ⊢scanq,θ(v0,P):b[n] 109.70279pt $ P:b[n-1]$ $ n≥ 2$ $ v_0 _b$ $ ∀ a _b.\;q_θ(a 24891 ·):W_b _b$ 40.19594pt $ _q 24891 θ(v_0 24891 P):b[n]$ T-Scan ⊢Pi:bi[n](1≤i≤k) ≥k2 ≥n1 =b∑=i1kbi fθ:∏=i1kWbi↔Wb ⊢mergef,θ(P1,…,Pk):b[n] 138.46785pt $ P_i:b_i[n] (1≤ i≤ k)$ $ k≥ 2$ $ n≥ 1$ $ b= _i=1^kb_i$ $ f_θ: _i=1^kW_b_i _b$ 51.04251pt $ _f 24891 θ(P_1 24891 … 24891 P_k):b[n]$ T-Merge ⊢P:b(d)[n] =n∏jsj ⊢⟨d,s,P⟩:Tensor 45.97305pt $ P:b(d)[n]$ $ n= _js_j$ 32.81863pt $ d 24891 24891 P : Tensor$ T-Tensor Notation. b=0,…,2b−1W_b=\0 24891 … 24891 2^b-1\; ↔ marks a bijection; θ denotes stored operator parameters; u∗u^* applies u to every word; P represents X when ⊢⟨d,,P⟩: d 24891 24891 P : Tensor and (P)=(X) Exec(P)= Bits(X). Figure 3. Typed operators in the Brevis language. Lit is the universal fallback; all internal operators are reversible for their stored parameters. Let tensor X have dtype d, shape s, and n elements. If b(d)b(d) is the physical width of d, Brevis flattens X in checkpoint order into (3) =(X)∈b(d)n,b=0,…,2b−1.x= Bits(X) _b(d)^n 24891 _b=\0 24891 … 24891 2^b-1\. This representation preserves signed zeros, NaN payloads, and every other bit pattern. We write P:b[n]P:b[n] when program P produces n words of width b, and (P) Exec(P) for its output. Program P represents X exactly when (4) (P)=(X). Exec(P)= Bits(X). The type b[n]b[n] allows both the synthesizer and decoder to reject incompatible widths and lengths. The canonical encoding of P contains its operation tags, parameters, literal coding tables, lengths, and payloads. Let L(P)L(P) denote the byte length of this complete representation. Given expansion budget B, Brevis selects (5) P^=argminP∈B()L(P)subject to(P)=, P_x= _P _B(x)L(P) to Exec(P)=x 24891 where B()C_B(x) contains the initial literal program and all complete candidates found within the budget. The literal fallback makes B()C_B(x) nonempty, while the equality constraint excludes inexact programs. Thus, Brevis minimizes exact serialized size within the configured finite search space without claiming global optimality. 2.2. Typed Tensor Language Figure 3 presents the seven DSL operators and their well-formedness rules. Each synthesis hole carries both a type b[n]b[n] and the exact stream that its completed subprogram must generate. Grammar rules may therefore introduce only type-compatible children, and the decoder independently validates the same widths, lengths, arities, and parameters. Lit stores an arbitrary word stream and provides a universal fallback, whereas Const stores one word and its repetition count. Concat joins programs for adjacent regions, and Repeat expands one nonempty child multiple times. Together, these operators capture arbitrary values, constants, piecewise regions, and recurring subsequences. Map, Scan, and Merge expose relationships that are not visible as repeated strings. Map applies a width-preserving bijection, including XOR or modular addition with a constant, ZigZag coding (Google, 2026), Gray coding (Doran, 2007), bit reversal, and rotation. Scan stores an initial word followed by XOR or modular-addition updates, exposing adjacent correlations. Merge combines equal-length children whose widths sum to the parent width, using contiguous floating-point fields, or bit and byte planes. The basic execution rules are (litb()) Exec(lit_b(v)) =, =v 24891 (constb,n(v)) Exec(const_b 24891 n(v)) =(v,…,v), =(v 24891 … 24891 v) 24891 (concat(P1,…,Pk)) Exec(concat(P_1 24891 … 24891 P_k)) =(P1)⋯(Pk), = Exec(P_1)·s Exec(P_k) 24891 (repeatk(P)) Exec(repeat_k(P)) =(P)k, = Exec(P)^k 24891 (6) (mapu,θ(P)) Exec(map_u 24891 θ(P)) =uθ∗((P)). =u_θ^*( Exec(P)). For scanq,θ(v0,P)scan_q 24891 θ(v_0 24891 P), execution starts with v0v_0 and applies qθq_θ to the previous output and each update generated by P. A Merge applies its stored composition pointwise. Every parameter is serialized, every child has a fixed type, and the root must produce exactly the words required by the tensor record. Physical literal coding. Lit is a semantic leaf rather than necessarily a raw byte copy. The encoder tries raw words, fixed-width bit packing, canonical Huffman coding, and rANS, then selects the smallest complete encoding, including codec tags, tables, lengths, and payloads. The decoder first restores the literal words and then executes the surrounding program. Raw words remain available when codec metadata would outweigh the compression benefit. Running example. Consider the FP32 sequence (+1.0,−1.0,+1.0,−1.0,+1.0,−1.0)(+1.0 24891 -1.0 24891 +1.0 24891 -1.0 24891 +1.0 24891 -1.0). One synthesized program is (7) P= P= mergeFP32(repeat3(lit1(0,1)), _FP32\! (repeat_3(lit_1(0 24891 1)) 24891 const8,6(127),const23,6(0)). _8 24891 6(27) 24891 _23 24891 6(0) ). Its three children represent the sign, exponent, and fraction fields. The sign child stores (0,1)(0 24891 1) once and repeats it three times, while the other two generate the shared exponent and fraction. Merge reconstructs all six FP32 words. A direct literal remains valid, and Brevis selects the synthesized program only if its serialized form is smaller. 2.3. Target-Directed Synthesis Target-directed expansion. A naive synthesizer would enumerate programs and execute each one against the target tensor, although most candidates would fail to reproduce it. Brevis instead searches backward from the target. Every hole is paired with the exact stream that its completed subprogram must generate, and applying an operator decomposes that stream into the required outputs of its children. For operator r with parameters θ, let Gr,θG_r 24891 θ compose child streams and Dr,θD_r 24891 θ decompose a target stream. Brevis accepts only decompositions satisfying (8) Dr,θ()=(1,…,k)⟹Gr,θ(1,…,k)=.D_r 24891 θ(x)=(x_1 24891 … 24891 _k) G_r 24891 θ(x_1 24891 … 24891 _k)=x. Thus, if each child program generates its assigned stream, the parent is guaranteed to generate x. Correctness is preserved by construction rather than checked by repeatedly executing complete candidates. Each operator provides a target-specific inverse expansion. Repeat applies only when the target consists of exact copies, Map inverts its bijection, Scan derives updates from adjacent words, and Merge splits each word into fields or planes. Concat proposes boundaries derived from the target, while Const applies only to constant streams. Each rule considers finitely many target-derived parameters. Node, depth, arity, and memory limits keep the search finite, while canonical forms remove identity and equivalent programs. The search budget is therefore spent comparing exact representations rather than testing arbitrary programs for correctness. Checkpoint-specific production prior. The useful DSL productions vary across checkpoints. Brevis therefore selects a small deterministic sample stratified by dtype and tensor size, searches these tensors with uniform production costs, and counts the productions used by the smallest programs found. For each production, the context κ records the hole type, parent operator, child position, depth, dtype, size bucket, zero fraction, distinct-value ratio, repetition ratio, and entropy of adjacent differences. Algorithm 1 Bounded A* synthesis for one tensor. 0: Target :b[n]x:b[n], prior q q, expansion budget B 1: Pbest←litb()P_best _b(x) 2: Q←H(b[n],)Q←\H(b[n] 24891 )\; e←0e← 0 3: scut←⊥s_cut← 4: while Q is not empty do 5: s←PopMin(Q)s← PopMin(Q) by A* cost and byte bound 6: if LBL(s)≥L(Pbest)LB_L(s)≥ L(P_best) then 7: continue 8: end if 9: if s is complete then 10: Pbest←argminP∈Pbest,sL(P)P_best← _P∈\P_best 24891 s\L(P) 11: continue 12: end if 13: if e=Be=B then 14: scut←Prefer(scut,s)s_cut← Prefer(s_cut 24891 s) 15: continue 16: end if 17: e←e+1e← e+1 18: H(τ,)←LeftmostHole(s)H(τ 24891 )← LeftmostHole(s) 19: for each valid target-directed expansion of H(τ,)H(τ 24891 ) do 20: push the resulting typed state into Q 21: end for 22: end while 23: if scut≠⊥s_cut≠ then 24: Proll←CompleteWithLiterals(scut)P_roll← CompleteWithLiterals(s_cut) 25: Pbest←argminP∈Pbest,ProllL(P)P_best← _P∈\P_best 24891 P_roll\L(P) 26: end if 27: return PbestP_best With rule counts N(r,κ)N(r 24891 κ), admissible production set ℛ(κ)R(κ), and additive smoothing β>0β>0, we follow PHOG and Euphony (Bielik et al., 2016; Lee et al., 2018) to estimate the production prior: (9) q^(r∣κ)=N(r,κ)+β∑r′∈ℛ(κ)N(r′,κ)+β|ℛ(κ)|. q(r κ)= N(r 24891 κ)+β _r (κ)N(r 24891 κ)+β|R(κ)|. Unseen detailed contexts back off to coarser ones. Every valid production retains nonzero probability, so the prior changes only the exploration order and never makes a valid program unreachable. The prior is deterministic for a fixed checkpoint and is not stored with the compressed representation. Bounded A* search. A search state s contains a partial typed program whose holes are paired with their required output streams; H(τ,)H(τ 24891 ) is a hole of type τ targeting v. Applying production r under context κ incurs cost (10) w(r,κ)=−log2q^(r∣κ).w(r 24891 κ)=- _2 q(r κ). States are prioritized by g(s)+h(s)g(s)+h(s), where g(s)g(s) is the accumulated production cost and h(s)h(s) is an admissible completion cost computed from a relaxed grammar. The relaxation preserves width and coarse length constraints while omitting target guards and concrete parameters, ensuring that h(s)h(s) remains optimistic. Consequently, the learned prior affects only the exploration order, whereas candidate quality is determined independently by their serialized size. A separate byte lower bound LBL(s)LB_L(s) accounts for fixed operation tags, parameters, and a minimum closing cost for each remaining hole. States whose lower bound cannot improve upon the current best program are pruned, while complete candidates are evaluated using their exact serialized size L(P)L(P). Algorithm 1 summarizes the procedure. The initial incumbent is a literal program for the complete target, and search continues after the first complete candidate because the most probable program need not be the smallest. When the expansion budget is exhausted, Prefer retains the open state the queue orders first, and Brevis completes its remaining holes with literals and evaluates the rollout, allowing structures discovered near the search boundary to remain competitive. If the frontier is exhausted or safely pruned, the result is optimal within the configured finite search space. If the expansion budget is reached, Brevis returns the smallest exact candidate encountered, including the literal-completed rollout. The procedure does not claim global optimality over unbounded programs, but every returned program reconstructs the target exactly. 2.4. Archive Format and Bit-Exact Reconstruction The archive preserves the original safetensors header and layout. Each tensor record stores its name, dtype, shape, and synthesized program. Tensor records can be compressed and decoded independently by a bounded worker pool, while source-order emission keeps the archive deterministic. Before execution, the decoder parses the complete program and validates the type rules in Figure 3. It rejects invalid widths, lengths, parameters, or literal payloads, executes the program, and restores the bytes at their original offsets. Table 1. Complete archive results across 10 checkpoints. Each method cell reports archive size in decimal GB/storage reduction. Bold cells and underlined reductions mark the best and second-best comparable results. Domain Checkpoint Data type Source Archive size (GB)/storage reduction (GB) zstd LZ4 gzip† Snappy ZipNN DFloat11‡ Brevis Language BERT Base FP32 0.440 0.407/7.59% 0.440/0.00% 0.407/7.56% 0.440/−-0.01% 0.366/16.84% – 0.365/17.11% Llama-3.1-8B BF16 16.061 12.38/22.91% 15.94/0.77% 12.50/22.17% 16.06/0.00% 10.66/33.63% 10.90/32.16% 10.58/34.13% Ministral-3-8B BF16 17.836 13.79/22.67% 17.70/0.79% 13.94/21.85% 17.84/0.01% 11.83/33.68% – 11.74/34.18% Qwen3-32B FP8 34.323 28.41/17.21% 34.30/0.07% 28.29/17.57% 34.33/−-0.01% 28.08/18.18% – 27.85/18.85% Qwen3-32B BF16 65.524 50.84/22.41% 65.05/0.72% 51.36/21.62% 65.53/−-0.01% 43.65/33.38% – 43.28/33.94% Llama-3.1-70B BF16 141.107 108.58/23.05% 140.00/0.79% 109.67/22.28% 141.12/−-0.01% 93.50/33.74% – 92.73/34.28% Mixtral-8×22B BF16 281.241 217.40/22.70% 279.15/0.74% 219.97/21.79% 281.28/−-0.01% 186.23/33.78% – 184.85/34.27% GLM-5.2 BF16 1,506.667 1,159.70/23.03% 1,494.27/0.82% 1,171.85/22.22% 1,506.85/−-0.01% 998.71/33.71% – 991.73/34.18% Audio Voxtral-Mini-3B BF16 9.356 7.215/22.89% 9.269/0.93% 7.297/22.01% 9.355/0.02% 6.226/33.46% – 6.186/33.89% Image Qwen-Image BF16 57.699 44.64/22.63% 57.25/0.79% 45.07/21.89% 57.70/0.00% 38.42/33.42% – 38.14/33.89% †gzip uses libdeflate 1.19 in gzip mode at DEFLATE level 1. ‡DFloat11 reconstructs BF16 tensor bits in its native directory format; its Llama-3.1-8B result was independently validated at the bit level. Dashes indicate unsupported or unevaluated combinations. DFloat11 is excluded from the paired statistical analysis. Proposition 0 (Compositional bit-exact reconstruction). Let P be a complete, well-formed program whose root is assigned root=(X)x_root= Bits(X). Assume that (i) serialization and parsing preserve the typed tree and all stored parameters, (i) every physical literal codec c satisfies Decc(Encc())=Dec_c(Enc_c(v))=v, and (i) every internal node uses child targets returned by a decomposition satisfying Equation 8. Then executing the parsed program yields (X) Bits(X). Proof. Let tx_t be the target assigned to node t. We prove by induction on subtree height that (11) (Pt)=t Exec(P_t)=x_t for every parsed subtree PtP_t. For a Lit leaf, assumption (i) restores its stored stream exactly. For a Const leaf, well-formedness requires the assigned target to equal the stored value repeated to the specified length. Now consider an internal node using production r, parameters θ, and children t1,…,tkt_1 24891 … 24891 t_k. By induction, (Pti)=ti Exec(P_t_i)=x_t_i for every child. The decoder applies the stored composition function Gr,θG_r 24891 θ, and Equation 8 gives (Pt) Exec(P_t) =Gr,θ((Pt1),…,(Ptk)) =G_r 24891 θ ( Exec(P_t_1) 24891 … 24891 Exec(P_t_k) ) (12) =Gr,θ(t1,…,tk)=t. =G_r 24891 θ(x_t_1 24891 … 24891 _t_k)=x_t. The invariant thus holds at the root, where root=(X)x_root= Bits(X). ∎ The root type agrees with the stored dtype, shape, and layout, so placing the generated words at their recorded offsets reconstructs X bit for bit. The guarantee assumes correct operator implementations and does not imply global search optimality. 3. Evaluation 3.1. Experimental Setup Corpus and baselines. Our corpus contains 10 public checkpoints from Hugging Face, including eight language models (Devlin et al., 2019; Grattafiori and others, 2024; Qwen Team, 2025; Jiang et al., 2024; GLM-5 Team, 2026), one audio model, and one image generation model. It spans eight BF16, one FP32, and one FP8 checkpoint, comprising 420 canonical shards and 2,130,256,127,862 source bytes (2.130 TB). We compare Brevis against zstd 1.5.7 (level 9), ZipNN 0.5.4, LZ4 1.9.4 (HC level 9), gzip, and Snappy 0.7.3. We additionally compare with DFloat11 on Llama-3.1-8B, the only model for which a validated native result is available. TDT, ZipServ, and ENEC require different software or hardware backends, LLM.265 is lossy, and ECF8 (Yang et al., 2026c) is excluded because its official CUDA validator rejected the decoded output in our experiment. These methods are therefore not directly comparable. Configuration. The main Brevis configuration uses one A* expansion per tensor and 32 workers. To learn the checkpoint-specific production prior, calibration samples at most four tensors, performs six expansions per tensor, and examines at most 1,048,576 elements from each tensor. Programs are limited to 64 nodes and depth 4, with at most 512 MiB for open decompositions. All experiments use warm file caches on one AMD EPYC 9654 server with 192 physical cores, 724 GiB RAM. Measurement. For each checkpoint, we aggregate source and archive bytes over canonical shards and compute CR=∑iSi∑iCi,Savingm=Cm−CBrevisCm,CR= _iS_i _iC_i, _m= C_m-C_ BrevisC_m, where SiS_i and CiC_i denote the source and archive sizes of shard i, and CmC_m is the total archive size produced by baseline m. All 60 archives in the complete comparison matrix were decoded and retained only after exact reconstruction. Brevis, zstd, LZ4, gzip, and Snappy reconstruct the original files byte for byte; ZipNN preserves tensor names, metadata, dtypes, shapes, and payload bits but may alter the safetensors layout. We compute 95% percentile bootstrap intervals by resampling checkpoints 10,000 times with seed 20260729. For the five complete-corpus baselines, we use two-sided exact Wilcoxon signed-rank tests and report Holm-adjusted p-values pHp_H with matched-pairs rank-biserial correlation rrbr_rb. 3.2. Compression Effectiveness Across the complete corpus, Brevis reduces 2.130 TB to 1.407 TB, yielding a compression ratio of 1.5135 and a 33.93% storage reduction, or 722.79 GB saved. As shown in Table 1, Brevis produces the smallest archive for every checkpoint and available comparison. Against the four general-purpose compressors, it is smaller on all 10 checkpoints, with mean per-checkpoint savings ranging from 12.94% over zstd to 30.87% over Snappy (Figure 4). All five complete-corpus comparisons, including ZipNN, remain significant after Holm correction (pH=0.0098p_H=0.0098), with the maximum matched-pairs effect size (rrb=1.0r_rb=1.0). ZipNN is the closest complete-corpus baseline. Brevis is smaller on all 10 checkpoints and saves 10.21 GB in aggregate. Its pooled saving is 0.72% [0.70%, 0.81%], and its mean per-checkpoint saving is 0.71% [0.61%, 0.78%]. The mean saving across the eight BF16 checkpoints is 0.75% [0.71%, 0.79%], while the FP32 and FP8 savings are 0.32% and 0.81%, respectively, indicating that the aggregate result is not driven solely by the largest checkpoint. We additionally compare with DFloat11 using its only publicly available and independently validated native result on Llama-3.1-8B. DFloat11 occupies 10.896 GB, compared with 10.579 GB for Brevis, making Brevis 316.27 MB, or 2.90%, smaller. Because DFloat11 does not provide comparable results for the remaining checkpoints and uses a different container format, we do not generalize this comparison beyond Llama-3.1-8B. 3.3. Throughput Figure 5 compares storage reduction and throughput on Llama-3.1-70B. Brevis reaches 3.60 GB/s compression and 6.61 GB/s decompression with a compression ratio of 1.522. Compared with ZipNN, it compresses 7.2% faster while producing a 0.82% smaller archive, placing it on both Pareto frontiers. zstd and LZ4 decompress faster, and Snappy compresses faster, but all achieve lower storage reduction. Throughput uses the 141.11-GB source size and full-checkpoint elapsed time, including process launch and output fsync, but excluding cache conditioning and verification. Because methods use practical rather than identical resource configurations, these comparisons are descriptive. Figure 4. Mean archive saving of Brevis over the five complete-corpus baselines. Lines show 95% bootstrap intervals over checkpoints. Figure 5. Storage reduction versus compression and decompression throughput. Upper right is better; lines show the Pareto frontiers. 3.4. Synthesis Analysis and Ablation We analyze synthesis on the first 4.98 GB shard of Llama-3.1-8B. At budget 1, Brevis already captures most of the achievable compression and completes in 9.04 seconds. Budgets 32 and 256 save an additional 3.13 MB and 5.48 MB but require 135.04 and 1,399.89 seconds, respectively, motivating the budget of one expansion used in the main evaluation. Table 2 further evaluates A* search and the checkpoint-specific production prior. Removing A* increases archive size by 2,873,336 bytes, removing the prior adds 389 bytes, and removing both increases it by 3,123,197 bytes. Together, these results suggest that bounded A* and the learned prior work synergistically, with A* providing the primary compression gain while the prior further improves guided search. Table 2. Search-guidance ablation on the Llama-3.1-8B shard. Extra bytes are relative to the full configuration. Configuration Extra bytes vs. full Time (s) Full A* + prior 0 140.24 No A* +2,873,336 118.09 No prior +389 88.82 No A* or prior +3,123,197 70.69 Limitations and Conclusion Brevis formulates lossless tensor compression as program synthesis over typed, self-contained programs. Its reversible operators expose value, sequence, field, and plane structure, while literal codecs encode the resulting streams. Target-directed expansion preserves bit exactness by construction, a checkpoint-specific production prior guides bounded A* search, and exact serialized size determines the selected program. On 10 public checkpoints spanning language, audio, and image generation models, Brevis reduces 2.130 TB of checkpoint data to 1.41 TB, achieving a 33.93% storage reduction. It produces archives up to 30.87% smaller than four general-purpose compressors, and smaller archives than the tensor-specific compressors. Several limitations remain. The evaluation covers public model checkpoints rather than all tensor workloads, with limited and partly confounded domain and format diversity. The current implementation synthesizes each tensor independently, so cross-tensor synthesis, broader corpora, and accelerator-aware decoding remain future work. Data and Artifact Availability The anonymous implementation and datasets, as well as the scripts used to generate the evaluation results, are included in our GitHub repository: https://github.com/jiekeshi/Brevis. References A. Afroozeh, L. Kuffó, and P. Boncz (2023) ALP: adaptive lossless floating-point compression. Proceedings of the ACM on Management of Data 1 (4), p. 230:1–230:26. External Links: Document Cited by: §1.1. R. Alur, R. Bodík, G. Juniwal, M. M. K. Martin, M. Raghothaman, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak, and A. Udupa (2013) Syntax-guided synthesis. In Formal Methods in Computer-Aided Design (FMCAD), p. 1–8. External Links: Document Cited by: §1.3. P. Bielik, V. Raychev, and M. Vechev (2016) PHOG: probabilistic model for code. In Proceedings of the 33rd International Conference on Machine Learning (ICML), Vol. 48, p. 2933–2942. External Links: Link Cited by: §1.3, §2.3. M. Burtscher, H. Mukka, A. Yang, and F. Hesaaraki (2016) Real-time synthesis of compression algorithms for scientific data. In SC16: International Conference for High Performance Computing, Networking, Storage and Analysis, p. 264–275. External Links: Document Cited by: §1.3, Introduction. S. Claggett, S. Azimi, and M. Burtscher (2018) SPDP: an automatically synthesized lossless compression algorithm for floating-point data. In 2018 Data Compression Conference (DCC), p. 335–344. External Links: Document Cited by: §1.3, Introduction. Y. Collet and M. Kucherawy (2021) Zstandard compression and the application/zstd media type. Note: RFC 8878 External Links: Document, Link Cited by: §1.1. Y. Collet, N. Terrell, W. F. Handte, D. Rozenblit, V. Zhang, K. Zhang, Y. Goldschlag, J. Lee, E. Gorokhovsky, Y. Komornik, D. Riegel, S. Angelov, and N. Rotem (2025) OpenZL: a graph-based model for compression. arXiv preprint arXiv:2510.03203. External Links: 2510.03203, Document, Link Cited by: §1.3. L. P. Deutsch (1996) GZIP file format specification version 4.3. Note: RFC 1952 External Links: Document, Link Cited by: §1.1. J. Devlin, M. Chang, K. Lee, and K. Toutanova (2019) BERT: pre-training of deep bidirectional transformers for language understanding. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, p. 4171–4186. External Links: Document Cited by: §3.1. R. W. Doran (2007) The gray code. Technical report Department of Computer Science, The University of Auckland, New Zealand. Cited by: §2.2. C. Fahlgren (2026) Cfahlgren1/hub-stats · Datasets at Hugging Face. Note: https://huggingface.co/datasets/cfahlgren1/hub-stats Cited by: Introduction. R. Fan, X. Yu, X. Pan, Z. Li, W. Luo, Q. Wang, W. Wang, and X. Chu (2026) ZipServ: fast and memory-efficient LLM inference with hardware-aware lossless compression. In Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2 (ASPLOS), p. 2264–2280. External Links: 2603.17435, Document, Link Cited by: §1.1. E. Frantar, S. Ashkboos, T. Hoefler, and D. Alistarh (2023) OPTQ: accurate quantization for generative pre-trained transformers. In The Eleventh International Conference on Learning Representations, External Links: Link Cited by: §1.2, Introduction. G. Gerganov (2026) Ggml/docs/gguf.md. Note: https://github.com/ggml-org/ggml/blob/master/docs/gguf.md Cited by: Introduction. GLM-5 Team (2026) GLM-5: from vibe coding to agentic engineering. arXiv preprint arXiv:2602.15763. External Links: 2602.15763, Link Cited by: §3.1. Google (2026) Protocol buffers: encoding. Note: https://protobuf.dev/programming-guides/encoding/Defines the ZigZag signed-integer encoding Cited by: §2.2. A. Grattafiori et al. (2024) The llama 3 herd of models. arXiv preprint arXiv:2407.21783. External Links: 2407.21783, Link Cited by: §3.1. Y. Hao, Y. Cao, and L. Mou (2024) NeuZip: memory-efficient training and inference with dynamic compression of neural networks. arXiv preprint arXiv:2410.20650. External Links: 2410.20650, Document, Link Cited by: §1.2. M. Hershcovitch, A. Wood, L. Choshen, G. Girmonsky, R. Leibovitz, O. Ozeri, I. Ennmouri, M. Malka, P. Chin, S. Sundararaman, and D. Harnik (2025) ZipNN: lossless compression for AI models. In 2025 IEEE 18th International Conference on Cloud Computing (CLOUD), p. 186–198. External Links: Document, Link Cited by: §1.1, Introduction. S. Jamalidinan and K. Cheshmi (2025) Floating-point data transformation for lossless compression. arXiv preprint arXiv:2506.18062. External Links: 2506.18062, Document, Link Cited by: §1.1. A. Q. Jiang, A. Sablayrolles, A. Roux, A. Mensch, B. Savary, C. Bamford, D. S. Chaplot, D. de las Casas, E. B. Hanna, F. Bressand, G. Lengyel, G. Bour, G. Lample, L. R. Lavaud, L. Saulnier, M. Lachaux, P. Stock, S. Subramanian, S. Yang, S. Antoniak, T. Le Scao, T. Gervet, T. Lavril, T. Wang, T. Lacroix, and W. El Sayed (2024) Mixtral of experts. arXiv preprint arXiv:2401.04088. External Links: 2401.04088, Link Cited by: §3.1. W. Lee, K. Heo, R. Alur, and M. Naik (2018) Accelerating search-based program synthesis using learned probabilistic models. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), p. 436–449. External Links: Document Cited by: §1.3, §2.3. J. Lin, J. Tang, H. Tang, S. Yang, G. Xiao, and S. Han (2024) AWQ: activation-aware weight quantization for on-device LLM compression and acceleration. GetMobile: Mobile Computing and Communications 28 (4), p. 12–17. External Links: Document Cited by: §1.2, Introduction. K. Masui, M. Amiri, L. Connor, M. Deng, M. Fandino, C. Höfer, M. Halpern, D. Hanna, A. D. Hincks, G. Hinshaw, J. Mena Parra, L. B. Newburgh, J. R. Shaw, and K. Vanderlinde (2015) A compression scheme for radio data in high performance computing. Astronomy and Computing 12, p. 181–190. External Links: Document Cited by: §1.1. Qwen Team (2025) Qwen3 technical report. arXiv preprint arXiv:2505.09388. External Links: 2505.09388, Link Cited by: §3.1. A. Rodriguez, N. Azami, and M. Burtscher (2024) Adaptive per-file lossless compression of floating-point data. In 2024 IEEE International Parallel and Distributed Processing Symposium Workshops (IPDPSW), p. 423–430. External Links: Document Cited by: §1.3, Introduction. K. Shi, D. Bieber, and R. Singh (2022) TF-Coder: program synthesis for tensor manipulations. ACM Transactions on Programming Languages and Systems 44 (2), p. 10:1–10:37. External Links: Document Cited by: §1.3. H. Tan, Y. Chen, G. Alonso, W. Wong, and B. He (2026) Approaching shannon bound with lossless LLM weight compression. In Proceedings of the 53rd Annual International Symposium on Computer Architecture (ISCA), External Links: 2606.15789, Link Cited by: §1.1. Z. Wang, T. Lan, Z. Su, J. Yang, and Y. Cheng (2026) ZipLLM: efficient LLM storage via Model-Aware synergistic data deduplication and compression. In 23rd USENIX Symposium on Networked Systems Design and Implementation (NSDI 26), Renton, WA, p. 2371–2387. External Links: ISBN 978-1-939133-54-0, Link Cited by: §1.1, Introduction. C. Xu, Y. Wu, X. Yang, B. Chen, M. Lentz, D. Zhuo, and L. W. Wills (2025) LLM. 265: video codecs are secretly tensor codecs. In Proceedings of the 58th IEEE/ACM International Symposium on Microarchitecture, p. 445–460. External Links: Document, Link Cited by: §1.2, Introduction. J. Yang, J. Wu, Z. Liu, X. Ma, H. Zhao, Y. Gu, Y. Huang, X. Liu, W. Huang, Z. Wei, J. Xing, Y. Ma, Q. Zhang, B. An, Z. Hu, S. Liu, X. Zhu, J. Lu, G. Tan, and D. Tao (2026a) ENEC: a lossless AI model compression method enabling fast inference on ascend NPUs. In Proceedings of the 53rd Annual IEEE/ACM International Symposium on Computer Architecture, External Links: 2604.03298, Link Cited by: §1.1. Y. Yang, Y. Zhao, P. Yang, S. Wang, and Z. Zhou (2026b) ZipMoE: efficient on-device MoE serving via lossless compression and cache-affinity scheduling. In Proceedings of the 43rd International Conference on Machine Learning (ICML), Proceedings of Machine Learning Research, Vol. 306. External Links: 2601.21198, Link Cited by: §1.1. Z. Yang, T. Zhang, J. Xie, C. Li, Z. Xu, and A. Shrivastava (2026c) To compress or not? pushing the frontier of lossless GenAI model weights compression with exponent concentration. In International Conference on Learning Representations (ICLR), External Links: 2510.02676, Link Cited by: §1.1, §3.1. O. Yoran, K. Zheng, F. Gloeckle, J. Gehring, G. Synnaeve, and T. Cohen (2025) The KoLMogorov test: compression by code generation. In International Conference on Learning Representations (ICLR), External Links: Link Cited by: §1.3. P. Yubeaton, T. Mahmoud, S. Naga, P. Taheri, T. Xia, A. George, Y. Khalil, S. Q. Zhang, S. Joshi, C. Hegde, and S. Garg (2025) Huff-LLM: end-to-end lossless compression for efficient LLM inference. arXiv preprint arXiv:2502.00922. External Links: 2502.00922, Document, Link Cited by: §1.1. T. Zhang, M. Hariri, S. (. Zhong, V. Chaudhary, Y. Sui, X. Hu, and A. Shrivastava (2025) 70% size, 100% accuracy: lossless LLM compression for efficient GPU inference via dynamic-length float (DFloat11). In Advances in Neural Information Processing Systems, Vol. 38, p. 98966–98994. External Links: 2504.11651, Link Cited by: §1.1, Introduction.