LLM的自我对弈、AI生物学、形式化验证与更多 | YC论文俱乐部

cover

摘要

本期YC论文俱乐部由Francois Chollet的联合研究者Andrei主持，邀请四位研究者分享前沿AI论文及实践洞察。第一部分由Yas（斯坦福博士生）讲解ESMFold系列论文——Meta构建的蛋白质语言模型，展示从纯序列预测蛋白质结构的突破：在不需要手工特征（MSA）的情况下接近AlphaFold 3的性能，在抗体设计任务上甚至超越，并揭示了模型自发学会的生物层次结构。第二部分由Luke Bailey（剑桥博士生，师从Tatsu和Tangu）讲解"Scaling Self-Play with Self-Guidance"论文——将Alpha Zero式自我对弈应用于LLM后训练，发现标准自我对弈会产生无用的过度复杂问题，提出自我引导（Self-Guidance）机制使7B模型达到670B模型的解题能力。第三部分由Arnab Matei（Giga研究员）讲解StreamRAG——面向语音AI的流式检索增强生成，在用户说话的同时启动RAG管线以降低延迟。第四部分由Robert George（Caltech博士生）讲解Lean形式化验证——从定理证明到程序验证再到神经网络验证的全链路，以及他开发的LeanDoorch框架。最后由Luke Orthwine（Channel AI创始人）分享"像RTS游戏一样编程"的实战方法论——将代理式编程视为即时战略游戏，最大化并行度和APM（每分钟操作数）。

第一部分：AI for Biology——ESMFold与蛋白质语言模型

蛋白质折叠与AlphaFold的局限

Yas首先回顾了蛋白质结构预测的背景。AlphaFold是革命性的突破，但它的力量来自一个手工构建的特征——多序列比对（MSA，Multiple Sequence Alignment）。为了折叠一个蛋白质，AlphaFold需要找到该蛋白质的数百个进化亲缘体，将它们堆叠排列。这些共变模式编码了推断结构所需的信息。这是一种精美的领域工程——但也是"Bitter Lesson"（苦涩教训）所声称最终应该被淘汰的手工特征。

更重要的是，MSA构建既缓慢又昂贵，而且在最需要它的地方恰恰缺失——例如抗体设计任务。抗体的已知序列多样性相对于结构多样性而言极小，MSA提供的信息有限。

ESMFold：从序列到结构，无需MSA

Meta的ESMFold系列模型采用了完全不同的路径：抛弃MSA，直接将输入序列送入预训练的语言模型，用模型的表示（Per Residue Embeddings，每个残基的嵌入向量）作为结构预测器的输入。相同的目标、相同的输出，但不使用手工特征。

架构上一个有趣的创新：结构预测网络采用了循环模型（Looped Model），可以参数共享，并提供了一个调节推理时间计算（Inference Time Compute）的杠杆——通过增加循环次数来改进结构预测，无需重新训练或微调。这与测试时计算扩展（Test-Time Compute Scaling）和扩散模型中的采样步骤类似。

核心结果

在一般蛋白质-蛋白质复合物上，ESMFold 2仅用单序列（无MSA）就在DockQ通过率上距离使用MSA的AlphaFold 3仅约3个百分点。但在抗体应用上，ESMFold 2单序列以50%对47%的DockQ通过率超越了AlphaFold 3——抗体设计是药物开发者最关心的领域之一。生物学上这很好理解：抗体相对于结构的序列变异采样量远少于其他蛋白质类别。

Yas强调的结论是：MSA并未死亡，但手工特征只在数据丰富时有帮助，而药物设计师最需要它的地方往往数据匮乏。通用方法仍能从跨所有已知进化接触的预训练中获益良多。

机制可解释性：模型自发学会生物学

ESMFold最令人惊叹的发现来自机制可解释性（Mechanistic Interpretability）分析。研究者使用稀疏编码分析（Sparse Coding Analysis）——类似Anthropic在语言模型中使用的工具——来分解模型激活，寻找单语义激活方向（Mono-semantic Activating Directions）。

结果发现：仅从"填空"式预训练（MLM，Masked Language Model）中，模型的潜在空间自发分解为对应真实生物学概念的清晰特征，且组织为精美的层次结构——从单个氨基酸，到结构基序（Structural Motifs），到整个蛋白质结构域（Protein Domains），再到功能位点和蛋白质角色。这一切都不是有监督学习得到的。

一个具体例子：模型学会识别"亲核弯头"（Nucleophilic Elbow）——一种在多种不相关蛋白质中独立演化的催化域。模型在四种结构多样性极大、进化距离遥远的蛋白质中一致地识别出这个基序，说明它学到的是深层结构直觉，而非简单的序列记忆。

ESMFold团队还构建了迄今最大的蛋白质结构图谱——预测了超过10亿个蛋白质结构，按SAE空间表示排列，得到清晰的蛋白质空间家族图谱，包括CRISPR-Cas酶等已知重要家族——宛如蛋白质的"谷歌地图"。

逆向设计与药物发现

ESMFold的模型还被用于逆向设计（Inverse Design）——开发潜在的蛋白质药物，并在湿实验室中验证了多个与已知治疗靶点结合的蛋白质设计。例如PD-L1结合剂——PD-L1是免疫治疗中最重要的靶点之一，针对它的药物已帮助了大量此前无法治疗的癌症患者。如果能降低这类未来药物的开发成本，将产生巨大的人类影响。

对研究者的号召

Yas最后呼吁：生物学是做ML的绝佳领域——模型仍然很年轻，数据每年指数增长，且增长率本身也在加速。我们不是数据受限的——现在是进入这个领域的大好时机。

第二部分：LLM的自我对弈——Scaling Self-Play with Self-Guidance

当前LLM训练栈

Luke Bailey首先描述了当前大语言模型的训练流程：预训练（Pre-training）+ 后训练（Post-training）。值得注意的是，后训练中大规模长时间强化学习运行的计算量已经接近甚至超过了预训练。这些RL运行的方式是：收集大量任务（编程、数学、软件交互），让Agent在环境中采取行动，获得奖励，然后上加权好的rollout、下加权差的rollout进行训练。

Compressor 2的技术报告展示了清晰的缩放律：增加RL任务数量和计算量，下游性能可靠提升。但这意味着需要不断手动收集新的RL任务——当你需要持续扩展时，这会成为瓶颈。

自我对弈的核心思想

自我对弈（Self-Play）的核心问题是：如何自动生成新的RL任务，让模型训练并重复？

在传统RL中，有预定义的任务和环境。在自我对弈中，模型承担两个角色：生成RL任务的"猜想者"（Conjecturer）和解决任务的"求解者"（Solver），并且两者都被训练得更好。

Luke区分了两种自我对弈：

对称自我对弈（Symmetric Self-Play）：如AlphaGo——用旧版本模型作为对手，模型扮演相同的两个角色。
非对称自我对弈（Asymmetric Self-Play）：猜想者生成完整的RL任务（如编程题+单元测试），求解者尝试解决。

自我对弈的承诺是：原则上，学习没有上界。基于人类示范的模仿学习永远无法超越示范者；传统RL在所有环境都被解决或无法获得奖励时停止；但自我对弈可以持续生成新的学习信号，理论上永远提升。

标准自我对弈的问题：生成垃圾

Luke的实验揭示了标准自我对弈的严重问题。他们在3000道Lean形式化数学题上运行实验：标准RL渐近于约60%的正确率。加入标准自我对弈后，猜想者确实越来越好地生成了更多任务——但这些任务完全无用，自我对弈的表现与普通RL毫无差异。

原因何在？Luke展示了一个训练后期猜想者生成的问题——结论部分极其复杂、过度冗长、一团混乱。问题出在奖励函数：猜想者因为生成"难题"而获得奖励，但最简单的生成难题的方式就是制造人为的复杂性和混乱。这相当于让学生做一份三页长的高中微积分题——学生会犯小错误，但这个合成问题对学习数学毫无价值。

Self-Guided Self-Play：修复方案

Luke提出了SGS（Self-Guided Self-Play）算法，包含两个关键组件：

基于目标问题的锚定：对于每一道未能解决的目标问题，让猜想者生成一道相关的合成问题——将合成数据分布锚定在"好的"问题分布上。
引导者（Guide）评分：模型承担第三个角色——判断者，评估合成问题与目标问题的相关性以及是否过度复杂。猜想者的奖励变为：求解难度 × 引导者评分。

结果

使用7B参数模型，投入8倍计算量进行自我对弈后，7B模型达到了670B模型（大8倍以上的兄弟模型）的pass@1解题能力。但遗憾的是，性能仍未达到100%——问题远未完全解决。

Luke坦承：自我对弈并未像在围棋中那样实现"永远提升"——在实践中，模型仍然会停滞。这是未来工作的核心方向。

第三部分：StreamRAG——面向语音AI的流式检索增强生成

语音AI的延迟挑战

Arnab Matei（Giga研究员）讲解了语音AI场景下RAG面临的特殊挑战。传统RAG流程是：用户问完问题→启动RAG管线→检索相关文档→LLM生成回答。但在语音场景中，如果用户问完问题后Agent需要10秒才回复，这完全不是自然的对话体验。

核心想法：在用户说话时就开始RAG

这篇Meta论文的核心洞察是：不必等用户说完再启动RAG管线，而是在用户说话的同时就开始分析和检索。例如，用户说"今天天气怎么样，我要决定是否出门"——核心问题在话语的前半段，后半段可能是冗余的。

两种方法

固定间隔流式RAG（Fixed Interval Streaming RAG）：将音频分成固定块，每个块到达后运行RAG。关键问题是如何判断中间查询是否足够——论文的方案是比较中间查询和完整查询的初始检索路径是否匹配，如果匹配则提前执行完整管线。
模型触发的流式RAG：微调一个模型来决定每个新块到达时是否需要生成新的查询——避免在每个块上都运行RAG的计算浪费。基于已有块的查询质量，判断是否已经拥有足够的检索材料。

结果

论文在RAG基准测试上（转换为音频）显示：合成数据集延迟降低约0.5秒，人类语音数据集延迟降低约1.5秒，准确率与标准RAG基本持平。

Arnab强调，他的重点不是论文的具体方法，而是指出这个方向存在大量未解决的问题：如何在用户说话的同时判断哪部分足够启动检索？除了检索路径匹配，还有哪些方法？这些小问题一旦突破，能在生产环境中带来巨大收益。

第四部分：Lean与形式化验证——验证智能的新时代

从非形式化到形式化数学

Robert George（Caltech博士生）从近期的突破切入：DeepMind在2024年IMO获得金牌，OpenAI声称解决了80年的Erdős问题，DeepMind最新工作在循环中使用形式化验证——我们正在进入"验证智能"（Verified Intelligence）的新时代。

非形式化数学（Informal Math）非常灵活——教授可以用"QED"或"威慑式证明"跳过步骤。但形式化世界要求完全显式——而Lean正是为此设计的语言。

Lean的特性

不可欺骗：你无法欺骗定理证明器（Theorem Prover）
可扩展：不仅有前沿实验室推动，全球社区也在贡献数据
统一：证明与程序统一，支持元编程、宏、自定义自动化
函数式编程语言：Lean不仅是定理证明器，也是函数式编程语言
外部绑定：通过FFI（Foreign Function Interface）可调用CUDA等外部库

Mathlib（Lean的数学库）是最大的形式化数学知识库，涵盖拓扑学到代数几何，至少百万行高质量数学。

形式化突破的时间线

2020年：GPT-f（OpenAI）——首个用于自动定理证明的生成式语言模型
MiniF2F基准上的进展呈指数增长
2024年IMO：DeepMind获金牌（未使用Lean），OpenAI解决方案中包含类Lean的DSL，中国团队的STM Prover也获金牌
近期：Harmonic AI的Aristotle在Putnam中解决所有12道题；MathInc的Fields Medal工作；Google DeepMind的最新成果

超越数学：程序验证与科学

Robert强调，形式化验证的应用远不止数学：

程序验证（Program Verification）：Bug代价极其高昂，是一个万亿美元级的问题。LLM可以写代码，但能证明代码正确吗？他介绍了自己的工作Bridge——使用Lean作为函数式编程语言来引导LLM证明代码正确性。Max Tegmark提出的"从宽泛编码到可验证编码"（From Wide Coding to Verified Coding）的转向将是更优的方向。
AI for Science：科学研究的可重复性（Reproducibility）问题。

LeanDoorch：用Lean写神经网络

Robert介绍了他开发的LeanDoorch——首个在Lean中编写神经网络的统一框架：

类PyTorch风格的张量系统，所有内容编译到共享中间表示
验证浮点运算（Verified Floating-Point Arithmetic）
神经网络验证——如认证鲁棒性（Certified Robustness）
证明Flash Attention在规格层面等价于标准Attention
证明无位置编码时Attention机制的排列不变性
在Lean中原生训练了一个GPT-2风格模型（基于Karpathy的实现）
形式化了Thinking Machine Lab关于"温度为零时的非确定性"的博客——从LLM推理到GPU级别的CUDA内核验证，证明了微小浮点运算差异可能翻转最终argmax

Robert展望了一个代码和科学都能被形式化验证的未来，其中人们正在构建的大量基础设施将成为关键基石。

第五部分：像RTS游戏一样编程——代理式编程的实战方法论

从棋类到即时战略

Luke Orthwine（Channel AI创始人）提出了一个全新比喻：传统编程像下棋——线性、可预测、单线程；而代理式编程（Agentic Programming）像即时战略游戏（RTS，Real-Time Strategy）——你需要同时管理经济、生产、作战，没有单一维度的完美能带来胜利。

核心工具与方法

Git Worktree：在多台机器上并行开发，每个Worktree独立编译、互不干扰。结合任务管理软件和可移植的工作流，使工作可以在不同环境间自由迁移。
编排者Agent：通常由Claude运行，从想法到开工只需最少的按键——就像在RTS中点击小队到地图某处，稍后再回来处理。
Worker Agent：每个Worker都被指示尽可能推进到PR（Pull Request）——不严格遵循规格（因为规格往往是错的），可以做出假设（可以后续纠正）。前端开发中，Worker自动启动本地开发服务器、运行测试，让人类只需打开浏览器标签即可验证。
Dangerously Skip Permissions：尽可能在沙箱中运行跳过权限模式——需要频繁反馈的Agent运行效率极低。
知识库（Knowledge Base）：结构化的、互相链接的Wiki风格文档——比代码更便宜地传递上下文。每次完成工作后，将经验和纠正反馈回知识库，使未来的Agent更高效。

RTS原则在编程中的应用

宏观优先，微观必要时（Macro by Default, Micro When It Counts）：你不能靠微操几个单位赢得RTS——你需要不断生产单位、扩张经济。编程也是如此：如果只在一件事情上深度投入，你会浪费大量并行机会。
高可见性：像RTS中的小地图一样，始终监控所有Agent的进度——可以快速跳转到关键位置审计和纠正。Agent会犯错、会走偏，早期发现和纠偏节省大量时间。
音频提示：Luke将每个Agent的终端会话映射到不同Warcraft/Starcraft单位——用颜色编码、主题区分、播放实际游戏音效。这让他不需要阅读标签页就能立即知道哪个Agent需要关注。
APM追踪（Actions Per Minute）：他们构建了内部APM追踪器——不是追踪人类点击，而是追踪Agent的tool calls per minute。目标是在每个时间尺度（分钟、小时、天、周）上最大化这个数字。Luke引用RTS游戏的观察：高APM不是获胜的充分条件，但低APM绝对无法成为顶级玩家。

关键结果

Channel AI采用这套方法论后，每位工程师每月的PR数量增长了3.5倍。在全员采用Agent式工作流后，单月又增长了60%。

核心理念：满足即可

Luke引用经济学概念"满足即可"（Satisficing）——做到足够好但不追求完美。即使Agent做得比你差、比你慢，让它做仍然比你自己做更好——因为你的注意力可以同时监督多个Agent。并行处理不同规模的工单，永不浪费你的认知带宽。

"你不会变得更聪明，但你可以训练自己像RTS职业选手一样行事——在那个领域中，什么才是最优的？我如何学会那些方法？像RTS职业选手一样编程。"