@leloykun: 我又忙忘了时间 >.< 最近如果给我发过私信，真的非常抱歉。我保证会逐一查看！--- 在本次迭代中，我……

我又忙忘了时间 >.< 最近如果给我发过私信，真的非常抱歉。我保证会逐一查看！--- 在本次迭代中，我构建了一个 Lean4-to-TileLang 张量程序超优化器。借助它，我现在拥有了一套形式化基础设施，让我（或我的智能体）能够在 Lean4 中定义神经网络架构，并自动获得：1. TileLang 中经过优化的 IO 感知加速器内核。它可以自动发现 FlashAttention2、FlashNorm、split-k matmul 等模式。目前在我的基准测试集上，于 A100 上实现了约 1.8 倍的几何平均加速比。2. 优化器选择与参数化方案，支持超参数在模型宽度和深度之间进行迁移（参见我之前的博客文章）。3. 超参数缩放定律，指导我们在扩展 batch size、训练步数、数据集规模等时如何调整超参数（参见引用推文）。4. 优化器的低秩代理，用于在小规模下加速超参数调优，并能将结果迁移至全秩场景（我们即将发表相关论文，敬请期待！）。