- GRPO 实践：读懂训练曲线，再排查不稳定
- 从答案验证器开始，学习推理模型的训练与评测
- Thomas Hales：通过 Lean 检查之后，还需要相信什么？
- 一个普通用户的评测困惑：会做一次，还是稳定做对？
- BranchOPD：在有信息的分叉处采样，生成费用与总成本分开看
- 读对事实，仍选错动作：System One 模型的配对诊断
- ARC Prize 的 Argon 结果：同模型，两种执行层与不完整运行
- 时钟生成了曲线种子，仍有候选跳过的原因未明
- Claude 重设计量子电路：少存历史，也显式使用失败预算
- Lean 把“再检查一次”做进工具链
- KillSwitch：故意为难模型的语言，究竟测到了什么
- HybridAgent：内部用潜在状态思考，对外仍能调用工具
- Anthropic 与 Theorem：把模糊测试入口变成可检查的证明
- ThinkingCap 缩短 Gemma 推理，但平均分会藏住单项退步
- 数学社区开始整理 AI 证明稿，也在争论这份劳动该由谁承担
- Axiom 将有限单群分类证明形式化：难点也在把定义接起来
- Frank Calegari：数学研究还需要选择问题、理解结果
- 直接改 0.016% 权重：先修复小模型的重复推理