Explaining Attention with Program Synthesis（用程序合成解释注意力机制）

Explaining Attention with Program Synthesis（用程序合成解释注意力机制）

图1：四步法流水线——提取注意力矩阵 → LLM 合成 Python 程序 → 排序筛选 → 因果替换验证。

问题与动机

深度学习可解释性（interpretability，即理解神经网络内部在"算什么"）的长期目标是用人类可理解的符号描述替代不透明的神经计算。现有方法主要有两条路线：自上而下（训练探针检测预定义概念）和自下而上（用自然语言描述神经元激活模式）。但前者依赖人类先验定义的概念，后者产生的自然语言解释本身也可能模糊、难以形式化验证。

MIT CSAIL 团队的核心洞察是：可执行程序（executable programs） 天然处于"十亿参数黑箱"和"自然语言解释"之间的甜区——既人类可读，又可被形式化验证，还能直接替换神经组件进行因果检验。他们聚焦于 Transformer 中的注意力头（attention head，即决定每个 token 关注哪些其他 token 的计算单元），因为注意力头是理解模型内部信息流动的关键入口。

方法要点

整体流程可概括为"提取 → 合成 → 排序 → 替换"四步：

（1）注意力模式提取。 对目标模型（GPT-2、TinyLlama-1.1B、Llama-3B、BERT-base）中的每个注意力头，在一组训练样本上记录其注意力矩阵（即每个 token 对每个其他 token 的"关注权重"），保留前 2.5% 最显著的 token 对交互。

（2）LLM 驱动的程序合成。 将过滤后的注意力模式格式化为约 4,000 token 的结构化文本提示，输入给一个"解释器"语言模型（Claude Sonnet 4），要求它生成能仅凭输入文本重现这些注意力模式的 Python 程序。程序可调用 NumPy、spaCy 和 NLTK 等库。首轮生成后，用 Jensen-Shannon 距离（JSD，衡量两个概率分布相似度的指标）选出最优和最差案例，构造对比反馈，再让解释器做一轮修正。

（3）重排序。 对所有候选程序在留出数据上计算 IoU（Intersection-over-Union，交并比）相似度，选出每个头的最佳拟合程序。值得注意：为某个头合成的程序（"目标程序"）往往不如从整个程序库中跨头搜索到的"最佳程序"——说明某些程序足够通用，可以近似多个头。

（4）因果替换验证。 在模型前向传播中，直接用程序输出替换神经注意力矩阵，测量困惑度（perplexity，衡量模型预测不确定性的指标）变化和下游任务表现。这是最关键的一步：不仅看相似度数字，还要看替换后模型还能不能正常工作。

证据

实验覆盖四个模型架构（BERT-base 144 头、GPT-2-small 144 头、TinyLlama-1.1B 704 头、Llama-3B 672 头），在 TinyStories 数据集上生成程序，在六个下游基准（HellaSwag、PIQA、SciQ、ARC-Easy、Social IQA、COPA）上评估替换效果。

主结果：

• 注意力对齐：基于不足 1,000 个程序的库，在 TinyStories 上实现平均 IoU 相似度 > 75%。自回归（因果）模型的拟合质量显著优于双向模型 BERT，且随着模型规模增大，IoU 分数提升：GPT-2 均值 69%、TinyLlama-1.1B 均值 74%、Llama-3B 均值 79%。
• 因果替换：按 IoU 从高到低贪婪替换注意力头，替换 25% 的注意力头仅导致约 16% 的平均困惑度增加；替换 30–40% 的注意力头后，下游问答任务表现仍无明显退化。IoU 分数与替换后困惑度增加之间的 Spearman 相关系数在所有模型上均 > 0.9。
• 定性发现：程序自动聚类为六类（首 token 注意力、句法、话语等），早期层以"首 token 注意力"程序为主，中间层以句法程序为主——与先前关于 BERT 层功能分化的发现一致。
• 成本：整个程序库（1,664 个程序，覆盖四个模型的所有头）使用 Claude Sonnet 4 约 $150 API 费用生成。

局限与边界

1. 覆盖不全：仍有大量注意力头 IoU 低于 40%，尤其 BERT 的双向注意力更难被符号化近似。
2. 程序复杂度有限：许多高分程序并不复杂（如"始终关注首 token"），可能更接近"剪枝效应"而非完整解释。
3. 仅关注注意力模式：未解释 value 投影和后续 FFN 层的计算，解释的是"模型在看哪里"而非"在看什么"。
4. 模型规模：仅在 GPT-2 到 Llama-3B 规模验证，尚未在更大模型上测试。

一句话 Takeaway

Transformer 中相当一部分注意力头可以用不足 50 行 Python 代码替换而几乎不影响模型表现——这意味着"神经网络黑箱"并非铁板一块，用程序合成做可解释性是一条可规模化、可因果验证的路径。

原文：Explaining Attention with Program Synthesis（arXiv:2606.19317v1，2026-06-17 提交，MIT CSAIL，3 位作者）
https://arxiv.org/abs/2606.19317

Self-CTRL: Self-Consistency Training with Reinforcement Learning（自一致性强化学习训练：让模型"说的"和"做的"一致）

图1：Self-CTRL 的两种训练方向——解释训练使模型的自述规则更准确预测其实际行为，行为训练使模型的实际回应更符合其自述原则。

背景：大语言模型经常"说一套做一套"——它们声称拒绝歧视性请求，但实际却顺从了用户指令。这种"言行不一"对用户信任和模型审计都构成严重挑战。现有训练方法只优化单个 prompt 下的输出质量，无法保证模型在"解释自己的行为"（元层面）和"实际行为"（对象层面）之间保持一致。MIT 团队提出了一个核心问题：能否让模型在跨上下文（跨 prompt）的意义上自洽——即模型在元层面说自己会怎么做，真的能预测它在对象层面会怎么做？

方法：Self-CTRL 将自一致性形式化为一个强化学习问题：给定一对输入（元层面问题 x_meta 和对象层面问题 x），让模型分别采样解释 y_meta 和行为 y，用一致性函数 φ 评分（解释是否预测了行为），然后用 GRPO（分组相对策略优化）同时优化解释和行为两个分布。支持三种模式：仅更新解释（λ=0）、仅更新行为（λ=1）、混合更新（λ=0.5）。在概率推理领域，φ 是形式化的对数似然；在宪法 AI 领域，φ 由多个持不同伦理框架的 LLM 陪审员打分。

结果与贡献：（1）在概率推理任务中，Self-CTRL 将模型自报硬币偏差与实际采样偏差之间的 R² 从 −0.23 提升至 0.65，与真实偏差的 R² 从 −0.40 提升至 0.60，在留出硬币上接近直接监督的 oracle 表现。（2）在宪法 AI 设置中，解释训练将第三方审计模型的拒绝预测准确率从 36% 提升至 92%，Normalized Simulatability Gain 从 −0.09 提升至 0.81；行为训练将 HarmBench 攻击成功率从 15.0% 降至 0.5%，且未显著增加无害 prompt 的过度拒绝。混合训练在安全性与可模拟性之间取得最佳权衡。MMLU 准确率在所有设置下保持在基线 ±2 个百分点以内。

原文：Self-CTRL: Self-Consistency Training with Reinforcement Learning（arXiv:2606.18327v1，2026-06-16 提交，MIT CSAIL，5 位作者）
https://arxiv.org/abs/2606.18327

DreamReasoner-8B: Block-Size Curriculum Learning for Diffusion Reasoning Models（DreamReasoner-8B：面向扩散推理模型的块大小课程学习）

图1：DreamReasoner-8B 的核心主张——块扩散模型通过课程学习，在推理质量和解码效率之间取得了此前扩散模型难以企及的平衡。

背景：扩散语言模型（dLLM，即通过迭代去噪而非逐 token 自回归生成文本的模型）因支持并行解码而有望突破自回归模型的推理效率瓶颈。其中块扩散（block diffusion）通过将序列切分为块、块间自回归块内并行去噪，在连贯性和效率之间提供了灵活折中。但现有开源扩散推理模型在长链思维（CoT）推理上仍落后于自回归模型，且当块大小增大时性能急剧退化——这恰恰抵消了大块带来的并行加速优势。港大/北大团队追问：能否让扩散模型在大块下也能有效推理？

方法：核心创新是块大小课程学习（block-size curriculum learning）：从 Qwen3-8B-Base 初始化，先持续预训练为 DreamReasoner-8B-Base（160B token），然后先用小块（块大小=4）SFT 学习细粒度因果依赖和局部推理模式，再逐步过渡到混合粒度训练（块大小随机采样自 {4,8,16,32}）。此外，提出 RelaxedConfidence 解码策略：当某 token 周围已有足够多高置信度邻居时，降低其提交阈值，使连续高置信度 token 跨度更早并行解码。

结果与贡献：DreamReasoner-8B 在 AIME 2024/2025 和 LiveCodeBench 上达到与 Qwen3-8B-Thinking 竞争的性能，大幅超越同规模块扩散模型 TraDo-8B-Thinking 和更大规模的 SDAR-30B-A3B-Sci（LiveCodeBench pass@1 51.3% vs. 29.0%）。课程训练使模型在不同推理块大小（4→32）下保持稳定性能，而 SDAR 在超出训练块大小时性能急剧退化。RelaxedConfidence 在思考阶段和回答阶段分别带来 22.5% 和 54.5% 的 TPF（每前向传播生成 token 数）增益。论文声称这是首个与同规模自回归推理模型性能相当的开放块扩散推理模型。

原文：DreamReasoner-8B: Block-Size Curriculum Learning for Diffusion Reasoning Models（arXiv:2606.19257v1，2026-06-17 提交，HKU / Peking University，8 位作者）
https://arxiv.org/abs/2606.19257

Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation（Diffusion-Proof：超越自回归生成的形式化定理证明方案）

图1：Diffusion-Proof 的双模型协同架构——证明器负责全证明生成，修正器利用扩散模型的双向感知能力进行局部填充修正。

背景：形式化定理证明（如 Lean4 环境）要求模型在严格逻辑约束下生成证明，但自回归（AR）模型在长证明中面临两个根本缺陷：从左到右的逐 token 生成缺乏长程连贯性（long-range coherence），且天然无法利用后缀信息进行填充式修正（in-filling correction）。扩散语言模型（dLLM）通过迭代去噪生成文本块，天然具备双向上下文感知能力和更强的长程连贯性，但其在形式化数学中的应用此前几乎未被探索。UIUC/NVIDIA 团队首次尝试将 dLLM 引入这一领域。

方法：Diffusion-Proof 包含两个 7B 模型的协同训练与推理管线。dLLM-Prover-7B：从 Fast-dLLM-V2-7B 初始化，在 300k 条 Lean4 证明数据上以块大小 32 做 SFT，采用课程数据排序（按证明长度递增）。dLLM-Corrector-7B：在证明器基础上，将扩散块大小扩展到 512，用 128k 条含子目标分解的数据训练大块填充修正——将错误子目标证明替换为 256 token 的掩码序列，让模型利用前后双向信息生成修正。推理时，证明器先生成完整证明，若 Lean 验证失败但顶层子目标结构正确，则由修正器进行局部修正。

结果与贡献：Diffusion-Proof 在 MiniF2F-Test 上达到 50.00%（比同数据训练的 AR 基线 Qwen-2.5-Lean-SFT-7B 的 43.85% 高出 6.14 个百分点），在 ProofNet-Test 上达到 7.53%（基线 5.91%，+1.61 个百分点）。修正器单独贡献了 MiniF2F 上 4 道题的解答（+1.64%）。亮点：Diffusion-Proof 成功解决了一道 IMO 问题（imo_1962_p2），而更强的 DeepSeek-Prover-V2-7B（含 Long CoT 推理）在 pass@32 下未能解决该题。验证损失分析表明，微调后的 dLLM 和 AR 模型在因果注意力损失上几乎等价（Pearson 相关系数 0.9846），dLLM 的优势来自扩散生成自身的迭代精炼和双向信息利用。

原文：Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation（arXiv:2606.19315v1，2026-06-17 提交，UIUC / NVIDIA，5 位作者）
https://arxiv.org/abs/2606.19315

Upstream

6 月 18 日榜单第 1 名。为人类和 Agent 共同协作重新设计邮件收件箱。

Honestly

6 月 18 日榜单第 2 名。汇总 Reddit 与 TikTok 的真实用户反馈。

Jesse

6 月 18 日榜单第 3 名。搜索实时互联网中的公司和采购信号。

来源：Product Hunt 6 月 18 日榜单