读懂论文，保留问题。 每日读一篇相关论文，关注作者提出了什么问题、如何论证，以及留下了哪些值得继续思考的疑问。
| 方向 | 关注的问题 |
|---|---|
| AI for Silicon / EDA | Agent 如何生成、优化与验证硬件设计？ |
| 编译器与 GPU 工具链 | AI 如何参与程序变换、kernel 优化与工具链测试？ |
| 规格、验证与评测 | 如何表达约束、构造可靠反馈、识别错误与评测漏洞？ |
| 知识与工程工作流 | 如何沉淀领域经验、组织工具调用、衡量可靠性与成本？ |
每篇包含论文定位、简短中文导读、arXiv / 全文 / alphaXiv 入口、阅读路线、思想启发，以及 3 个思考问题；参考思路默认折叠。优先开放全文和有实验依据的工作，也收录能明确提出研究问题的观点论文，并区分作者结论、作者预测和导读者的延伸。
新论文与经典工作结合，按论文编号去重。没有合适新作时回读经典，不以新闻凑数。
SpecAgent 用依赖感知规划、形式验证、跨规格修复与强度审查生成 ACSL 规格；其完备性探针能识别返回值欠约束，但不能单独证明规格已表达全部重要语义。
ChipBench 用更长、更复杂的 RTL 模块，以及调试和参考模型生成任务，让先进模型的成绩显著下降；但 benchmark 的难度、真实性与结论外推范围仍需分别判断。
CUDA Agent 在执行反馈环境中训练 CUDA 优化策略，并在 KernelBench 上显著超过 torch.compile；但评测允许每题最多 200 轮并选取轨迹中的最快正确解，策略能力与搜索预算仍需分开理解。
ProofLoop 让 Agent 查询 RTL 结构并利用形式反例修正 SVA，显著提高可证明断言的比例；但在 Design2SVA 中，性质成立、性质非空洞与性质重要仍是三个不同判断。
FIXME 用 180 道题覆盖规格理解、参考模型、测试用例、testbench、断言和调试；它拓宽了 LLM 硬件验证评测，却也留下一个概念边界：流程覆盖不等于端到端执行。
Alpha-RTL 在每道 RTL 优化题上用 testbench 与 PPA 反馈在线更新 Qwen3-8B；结果显著优于冻结策略的 Agent，但也把评测对象从静态模型能力改成了带逐题训练预算的完整优化系统。
ACDC 以 Axon 为对象，分别测试已验证核心、可信检查、未验证文本接口与机器语义；实验说明形式证明能封闭一部分错误，却不能替代对规格、信任边界和拒绝行为的测试。
这篇论文把 kernel benchmark 的局部加速与真实 workload 的时间占比相乘：在 Transformer 中，可被生成式优化触及的部分仅占 8.9%–16.8%，因此看似不错的 kernel speedup 往往只能投射为约 1%–2.5% 的端到端收益。
Agentic Kernel Optimization 用多 Agent、性能分析和人工搜索纠偏，在 B200 上为三类 FlashInfer-Bench workload 生成高性能 CUDA kernel；论文证明了代码可由 Agent 完成，却也留下了系统自主性、基线口径与验证边界的问题。
KernelOPT 尊重 Inductor 已做出的库调用分派，只搜索生成的 Triton 子 kernel，并用四级验证决定替换或回退；250 个 KernelBench 问题上的整体加速来自少数显著收益与大量基线保留的组合，不能等同于每个任务都被优化。