开发者与开源 重要度 5

Z3与Lean验证INT4位技巧

作者展示用Z3通过CEGIS合成INT4点积的SWAR位运算公式，并用Lean 4进行形式化正确性证明。该项目面向无原生SIMD硬件上的量化推理优化，兼具底层性能与形式化验证价值。

事件进展（1 篇报道）

  1. 2026-08-09 05:55
    Reddit r/MachineLearning Synthesizing and formally verifying a SWAR bit-hack for INT4 dot products using Z3 and Lean 4 [P]

← 返回首页