AI研究论文每日精选

像Lean这样的证明助手已经彻底改变了数学证明验证的方式，确保了高准确性和可靠性。尽管大型语言模型（LLMs）在数学推理方面表现出潜力，但它们在形式定理证明方面的进展受到训练数据的不足所限。为了解决这个问题，我们提出了一种方法，通过从高中和本科水平的数学竞赛问题中生成大量Lean 4证明数据。这种方法涉及将自然语言问题翻译成形式陈述，过滤掉低质量的陈述，并生成证明以创建合成数据。在对DeepSeekMath 7B模型在这个包含800万个带证明的形式陈述的合成数据集上进行微调后，我们的模型在Lean 4 miniF2F测试中以64个样本达到了46.3%的整体证明生成准确率，并在累计上达到了52%，超过了基准GPT-4的23.0%（64个样本）以及一种树搜索强化学习方法的41.0%。此外，我们的模型成功证明了Lean 4正式国际数学奥林匹克（FIMO）基准中的148个问题中的5个，而GPT-4则未能证明任何一个。这些结果展示了利用大规模合成数据提升LLMs中定理证明能力的潜力。合成数据集和模型都将提供以促进这一领域的进一步研究。

最近的研究提出了线性表示假设：即语言模型通过在激活空间中操作概念（“特征”）的一维表示来执行计算。相反，我们探讨了一些语言模型表示是否可能固有地是多维的。我们首先制定了对不可约多维特征的严格定义，该定义基于这些特征是否可以分解为独立或不共现的低维特征。受到这些定义的启发，我们设计了一种可扩展的方法，使用稀疏自动编码器自动发现GPT-2和Mistral 7B中的多维特征。这些自动发现的特征包括引人注目的可解释示例，例如代表星期几和每年月份的圆形特征。我们确定了在这些确切圆形特征用于解决涉及星期几和每年月份的模运算计算问题的任务。最后，我们通过对Mistral 7B和Llama 3 8B进行干预实验，提供证据表明这些圆形特征确实是这些任务中的计算基本单元，并通过将这些任务的隐藏状态分解为可解释的组件来发现进一步的圆形表示。

尽管扩散模型在视频生成和编辑方面取得了显著进展，但实现准确和局部化的视频编辑仍然是一个重大挑战。此外，大多数现有的视频编辑方法主要集中在改变视觉内容，对运动编辑的研究有限。在本文中，我们提出了一种新的尝试，即重新制作视频（ReVideo），与现有方法有所不同，它允许通过指定内容和运动来精确编辑特定区域的视频。通过修改第一帧来实现内容编辑，而基于轨迹的运动控制提供了直观的用户交互体验。ReVideo解决了涉及内容和运动控制之间耦合和训练不平衡的新任务。为了解决这个问题，我们制定了一个三阶段训练策略，逐渐从粗到细地解耦这两个方面。此外，我们提出了一个时空自适应融合模块，以在各种采样步骤和空间位置上整合内容和运动控制。大量实验证明，我们的ReVideo在几个准确的视频编辑应用上表现出色，即（1）在保持运动恒定的情况下局部更改视频内容，（2）保持内容不变并自定义新的运动轨迹，（3）修改内容和运动轨迹。我们的方法还可以无缝地将这些应用扩展到多区域编辑，无需特定训练，展示了其灵活性和稳健性。

在多模态大型语言模型（MLLMs）中，我们是否充分发挥了视觉编码器的潜力？最近MLLMs在多模态理解方面取得的出色表现引起了学术界和工业界的广泛关注。在当前MLLM的激烈竞争中，焦点似乎主要集中在语言方面。我们看到更大规模和更高质量的指导数据集的崛起，以及更大规模的LLMs的参与。然而，很少有注意力被引导到MLLMs利用的视觉信号上，通常被假定为由冻结的视觉编码器提取的最终高级特征。在本文中，我们介绍了密集连接器 - 一种简单、有效且即插即用的视觉-语言连接器，通过利用多层视觉特征显著增强了现有的MLLMs，而额外的计算开销很小。此外，我们的模型仅在图像上训练，展示了在视频理解方面显著的零样本能力。在各种视觉编码器、图像分辨率、训练数据集规模、LLMs的不同规模（2.7B->70B）以及MLLMs的不同架构（例如LLaVA和Mini-Gemini）上的实验结果验证了我们方法的多功能性和可扩展性，在19个图像和视频基准测试中实现了最先进的性能。我们希望这项工作能提供宝贵的经验，并为未来MLLM的发展提供基本模块。

潜在扩散模型（LDMs）的进展彻底改变了高分辨率图像生成，但是这些系统核心的自编码器的设计空间仍未得到充分探索。本文介绍了LiteVAE，这是一种用于LDMs的自编码器系列，利用2D离散小波变换来提高可伸缩性和计算效率，而不会牺牲输出质量。我们还研究了LiteVAE的训练方法和解码器架构，并提出了几项增强措施，改善了训练动态和重建质量。我们的基础LiteVAE模型在保持输出质量的同时，将编码器参数减少了六倍，从而实现更快的训练速度和更低的GPU内存需求，而我们更大的模型在所有评估指标（rFID、LPIPS、PSNR和SSIM）上均优于具有相似复杂性的VAEs。

在人工智能领域，加速大型语言模型（LLMs）的推理是一项重要挑战。本文介绍了分布式推理（DSI），这是一种全新的分布式推理算法，可以证明比推测推理（SI）[leviathan2023fast，chen2023accelerating，miao2023specinfer]和传统的自回归推理（非SI）更快。与其他SI算法类似，DSI适用于冻结的LLMs，无需训练或架构修改，并且保留目标分布。 之前关于SI的研究已经证明了实证加速（与非SI相比），但需要一个快速准确的草稿LLM。实际上，现成的LLMs通常没有足够快速和准确的匹配草稿。我们展示了一个差距：当使用较慢或不够准确的草稿时，SI比非SI更慢。我们通过证明DSI比SI和非SI更快，无论使用何种草稿，来弥合这一差距。通过协调目标和草稿的多个实例，DSI不仅比SI更快，而且支持无法通过SI加速的LLMs。 我们的模拟显示在现实环境中现成的LLMs加速：DSI比SI快1.29-1.92倍。

扩散模型在图像生成方面取得了巨大成功，其主干从U-Net逐渐演变为视觉Transformer。然而，Transformer的计算成本随着标记数量呈二次增长，这在处理高分辨率图像时带来了重大挑战。在这项工作中，我们提出了扩散曼巴（DiM），它将基于状态空间模型（SSM）的Mamba序列模型的高效性与扩散模型的表现力相结合，实现了高效的高分辨率图像合成。为了解决Mamba无法泛化到二维信号的挑战，我们进行了多方向扫描、在每行和每列末尾添加可学习的填充标记，以及轻量级局部特征增强等多项架构设计。我们的DiM架构实现了高分辨率图像的推理效率。此外，为了进一步提高DiM在高分辨率图像生成方面的训练效率，我们研究了“由弱到强”的训练策略，即在低分辨率图像（256x256）上预训练DiM，然后在高分辨率图像（512x512）上进行微调。我们进一步探索了无需训练的上采样策略，使模型能够生成更高分辨率的图像（例如1024x1024和1536x1536），而无需进一步微调。实验证明了我们DiM的有效性和高效性。

二阶训练方法比梯度下降具有更好的收敛性能，但由于计算开销大，在大规模训练中很少被实际使用。这可以被视为一种硬件限制（由数字计算机所施加）。在这里，我们展示了自然梯度下降（NGD），一种二阶方法，在使用适当的硬件时，每次迭代的计算复杂度可以与一阶方法相似。我们提出了一种新的混合数字-模拟算法，用于训练神经网络，在某些参数范围内等效于NGD，但避免了代价高昂的线性系统求解。我们的算法利用了模拟系统在平衡状态下的热力学特性，因此需要模拟热力学计算机。训练发生在混合数字-模拟循环中，在此过程中，在给定时间间隔内计算梯度和Fisher信息矩阵（或任何其他半正定曲率矩阵），同时模拟动态发生。我们通过数值方法展示了这种方法在分类任务和语言模型微调任务上优于最先进的数字一阶和二阶训练方法的优越性。

最近的方法表明将扩散模型提炼为高效的一步生成器具有潜力。其中，分布匹配提炼（DMD）产生与其教师在分布上匹配的一步生成器，而不强制要求与其教师的采样轨迹一一对应。然而，为了确保稳定训练，DMD需要使用由教师通过多步确定性采样器生成的大量噪声图像对计算额外的回归损失。这对于大规模文本到图像合成来说成本高昂，并限制了学生模型的质量，使其与教师的原始采样路径过于密切相关。我们引入了DMD2，一组技术来解除这一限制并改进DMD训练。首先，我们消除了回归损失和昂贵数据集构建的需要。我们展示了由于虚假评论家未准确估计生成样本的分布而导致的不稳定性，并提出了双时间尺度更新规则作为补救措施。其次，我们将GAN损失整合到提炼过程中，区分生成样本和真实图像。这使我们能够在真实数据上训练学生模型，减轻了教师模型对真实评分估计的不完美，并提高了质量。最后，我们修改了训练过程以实现多步采样。我们在这种情况下确定并解决了训练-推断输入不匹配的问题，通过在训练时模拟推断时生成器的样本。综合而言，我们的改进在一步图像生成中设立了新的基准，ImageNet-64x64的FID得分为1.28，在零样本COCO 2014上为8.35，尽管推断成本减少了500倍，但超过了原始教师。此外，我们展示了我们的方法可以通过提炼SDXL生成百万像素图像，展示了在少步方法中出色的视觉质量。

近年来，随着逼真的生成结果和广泛的个性化应用，基于扩散的生成模型在视觉和音频生成领域引起了巨大关注。与文本到图像或文本到音频生成方面取得的相当大进展相比，音频到视觉或视觉到音频生成方面的研究进展相对较慢。最近的音频-视觉生成方法通常依赖于巨大的大型语言模型或可组合的扩散模型。本文并未设计另一个庞大的模型用于音频-视觉生成，而是展示了一种简单且轻量级的生成变压器，在多模态生成中尚未得到充分研究的情况下，可以在图像到音频生成上取得出色的结果。这个变压器在离散音频和视觉向量量化的GAN空间中运行，并以掩码去噪的方式进行训练。训练后，无需分类器指导即可进行现成部署，实现更好的性能，无需额外的训练或修改。由于变压器模型是模态对称的，因此也可以直接用于音频到图像生成和共同生成。在实验中，我们展示了我们的简单方法超越了最近的图像到音频生成方法。生成的音频样本可在以下链接找到：https://docs.google.com/presentation/d/1ZtC0SeblKkut4XJcRaDsSTuCRIXB3ypxmSi7HTY3IyQ

多模态大型语言模型（MLLMs）被普遍认为在探索人工通用智能（AGI）方面至关重要。MLLMs的核心在于其实现跨模态对齐的能力。为实现这一目标，当前MLLMs通常遵循两阶段训练范式：预训练阶段和指导微调阶段。尽管取得成功，但这些模型在对齐能力建模方面存在缺陷。首先，在预训练阶段，模型通常假设所有图像-文本对均匀对齐，但实际上不同图像-文本对之间的对齐程度是不一致的。其次，目前用于微调的指导中包含各种任务，不同任务的指导通常需要不同水平的对齐能力，但先前的MLLMs忽视了这些差异化的对齐需求。为解决这些问题，我们提出了一种新的多模态大型语言模型AlignGPT。在预训练阶段，我们不再将所有图像-文本对等同对待，而是为不同图像-文本对分配不同水平的对齐能力。然后，在指导微调阶段，我们自适应地结合这些不同水平的对齐能力，以满足不同指导的动态对齐需求。大量实验结果表明，我们的模型在12个基准测试上取得了竞争性能。

定制扩散模型以从用户提供的参考图像生成保持身份的图像是一个引人入胜的新问题。目前的方法通常需要在大量领域特定图像上进行训练，以实现身份保留，但在不同用例之间缺乏灵活性。为了解决这个问题，我们利用分类器引导，这是一种无需训练的技术，通过使用现有的分类器来引导扩散模型，实现个性化图像生成。我们的研究表明，基于最近的修正流框架，普通分类器引导在需要特殊分类器方面的主要限制可以通过简单的固定点解决方案来解决，从而允许使用现成的图像判别器进行灵活个性化。此外，基于参考流轨迹的求解过程被证明是稳定的，并具有收敛保证。所得方法在具有不同现成图像判别器的修正流上实现，为人脸、实时主体和某些对象提供了有利的个性化结果。代码可在https://github.com/feifeiobama/RectifID找到。

我们将多模态Transformer扩展，以包括3D摄像机运动作为视频生成任务的条件信号。生成式视频模型变得越来越强大，因此研究重点放在控制这些模型输出的方法上。我们建议通过在生成的视频上附加虚拟3D摄像机控制，将三维摄像机运动的编码作为生成视频过程中的条件，以此改进生成式视频方法。结果表明，我们能够（1）成功控制视频生成过程中的摄像机，从单个帧和摄像机信号开始，并且（2）我们展示了使用传统计算机视觉方法验证生成的3D摄像机路径的准确性。

我们研究了将图像生成模型适应不同数据集的任务，而无需微调。为此，我们引入了Semantica，一种基于图像的扩散模型，能够根据条件图像的语义生成图像。Semantica仅在网络规模的图像对上进行训练，即接收来自网页的随机图像作为条件输入，并对同一网页中的另一随机图像进行建模。我们的实验突显了预训练图像编码器的表达能力以及在实现高质量图像生成中必须进行基于语义的数据过滤。一旦训练完成，它可以通过简单地使用该数据集中的图像作为输入，自适应地生成新图像。我们研究了Semantica在ImageNet、LSUN教堂、LSUN卧室和SUN397上的迁移特性。

神经辐射场（NeRFs）通常难以重建和渲染高度反光的物体，其外观随视角变化迅速而变化。最近的研究改进了NeRF渲染远处环境光照的详细反光外观的能力，但无法合成较近内容的一致反射。此外，这些技术依赖于大型计算昂贵的神经网络来建模出射辐射，严重限制了优化和渲染速度。我们提出了一种基于光线追踪的方法来解决这些问题：我们的模型不是查询昂贵的神经网络以获取沿着每个摄像机光线的点的出射视角相关辐射，而是从这些点投射反射光线，并通过NeRF表示跟踪这些光线，以渲染特征向量，然后使用一个小型廉价网络将其解码为颜色。我们证明了我们的模型在合成包含有光亮物体的场景的视图合成方面优于先前的方法，并且是唯一能够在真实场景中合成逼真的反光外观和反射的现有NeRF方法，同时需要与当前最先进的视图合成模型相当的优化时间。

对于诸如闪亮金属或光泽油漆等具有镜面特性的物体进行新视角合成仍然是一个重大挑战。不仅需要考虑光泽外观，还需要全局照明效果，包括环境中其他物体的反射，这些都是忠实再现场景所必需的关键组成部分。在本文中，我们提出了神经方向编码（NDE），这是一种基于视角的外观编码，用于呈现具有镜面特性的物体的神经辐射场（NeRF）。NDE将基于特征网格的空间编码概念转移到角度域，显著提高了对高频角信号建模的能力。与先前仅使用角度输入的编码函数不同，我们还锥追踪空间特征，以获得空间变化的方向编码，从而解决了具有挑战性的互反射效应。对合成和真实数据集的大量实验表明，具有NDE的NeRF模型（1）在镜面物体视角合成方面优于现有技术水平，（2）能够通过小型网络实现快速（实时）推断。项目网页和源代码可在以下网址找到：https://lwwu2.github.io/nde/。

本文介绍了一种低成本、高真实性的双向远程呈现系统Tele-Aloha，旨在应用于点对点通信场景。与先前的系统相比，Tele-Aloha仅利用四个稀疏的RGB摄像头、一个消费级GPU和一个自动立体屏幕，实现了高分辨率（2048x2048）、实时性（30 fps）、低延迟（小于150毫秒）和稳健的远程通信。作为Tele-Aloha的核心，我们提出了一种高效的新颖视角合成算法，用于上半身。首先，我们设计了一个级联视差估计器，用于获取稳健的几何线索。此外，引入了通过高斯飞溅实现的神经光栅化器，用于将潜在特征投影到目标视角并将其解码为降低分辨率。此外，鉴于高质量的捕获数据，我们利用加权混合机制将解码图像精炼到2K的最终分辨率。利用世界领先的自动立体显示和低延迟的虹膜跟踪，用户能够体验到强烈的三维感，即使没有任何可穿戴的头戴显示设备。总的来说，我们的远程呈现系统在真实实验中展示了共存感，激发了下一代通信技术的发展。