像物理学家一样剪枝 LLM：把块删除当成 Ising 优化问题
整块删掉 transformer block 最省事，挑哪些块却是多体问题。Multiverse Computing 把它写成二元优化，用 Ising 的低能态对应高分模型，Llama-3.3-70B 砍半深度仍保住 MMLU 76.9。
压缩
更多 压缩
首页用 Lean 写 Zstandard 解压器：当 LLM 把「证明成本」压下来
Adam Langley 用 Lean 写了一个 Zstandard 解压器，把类型级不变量写成类型签名，再让 LLM 去补证明体， 并记下它在哪些步骤上真的省了事。