Aristotle 用 Lean 4 形式化验证多尺寸 FP16 脉动阵列矩阵乘法器
satnam6502 · x · 2026-11-07
研究者 satnam6502 发布系列报告，展示用 Aristotle 对脉动阵列矩阵乘法器进行形式化验证的结果。
- 覆盖 4x4、8x8、16x16、32x32、64x64 五种规模，均针对 FP16 数值。
- 报告包含在 Lean 4 中形式化验证的性质、对应 SystemVerilog 代码及验证摘要。
- 验证方式是与流水线脉动阵列乘法器的高层功能规范做直接对比；作者指出，这种针对相当直接的高层规范做形式化验证的做法并不常见。
- 配图演示了 4x4 阵列中各处理单元（PE）逐周期的数据流与累加过程。
「Infra」频道最新
- Epoch 估算:华为和林格尔数据中心算力仅为主流 Colossus 2 的 7% — Jsevillamol · 2026-11-07
- Musk 宣布 SpaceX 2027 Q3 起发射轨道超算 StarMind,与 NVIDIA 共同设计 — XFreeze · 2026-11-07
- Netflix 用本体做可观测性:遥测、事故与服务关系连成知识图谱 — JeremyCMorgan · 2026-11-07
- 超大规模云厂商开始收割 Neocloud:Google 买下 Crusoe 怀俄明数据中心 — SumitGup · 2026-11-07
- Burry 做空 Oracle 301 天：股价自高点跌 66%，验证空头判断 — kingslyj · 2026-11-07
- 分析师：中期选举后 AI 供应商估值已低于自家增长预测 — BenBajarin · 2026-11-07