ProofWeaver

展开

agent 已经能写出带 TMA、tensor-core async group、barrier phase、staged-buffer reuse 的 warp-specialized kernel，但 static validator / random test / Compute Sanitizer / agent 自评分都不能证明在所有合法 GPU 调度下安全，更推不出与数学参考等价。

ProofWeaver 的关键设计是：agent 是不可信的提案方和修复方；IR extractor、Z3 obligation、verdict 全部 system-owned。agent 只能提交 source diff，controller 重放后才 re-extract。一个天花乱坠的 patch 说服不了 checker。

真实源码 gate 已落在 PR 上：FlashAttention #2312（ASYNC_WAR → fix 后 ACCEPT）、#2086；CUTLASS #2162（三选一的 typed transfer，Z3 分别给 REJECT / REJECT / ACCEPT）。

方法

translation validation：把 agent 提的 source 与数学参考都翻译到同一 IR，Z3 求解 obligation。Refinement 只做到 functional-index leaf 和 bounded tensor-value（P,dP,D ∈ [-16,16] 全整数域）。