每日精选AI研究论文及翻译
我们提出了位置插值（PI），它扩展了基于RoPE预训练LLM（如LLaMA模型）的上下文窗口大小，最多可达32768，而只需进行最少的微调（在1000步内），同时在需要长上下文的各种任务上展现出强大的实证结果，包括密码检索、语言建模以及从LLaMA 7B到65B的长文档摘要。与此同时，通过位置插值扩展的模型在其原始上下文窗口内的任务上相对保持了质量。为实现这一目标，位置插值线性地将输入位置索引进行缩放，以匹配原始上下文窗口大小，而不是超出训练过的上下文长度进行外推，这可能导致灾难性高的注意力分数，完全破坏自注意力机制。我们的理论研究表明，插值的上限至少比外推小600倍，进一步展示了其稳定性。通过位置插值扩展的模型保留其原始架构，并且可以重复使用大多数现有的优化和基础设施。
大型语言模型（LLMs）已显示出在使用诸如Lean之类的证明助手证明形式定理方面具有潜力。然而，由于私有代码、数据和大量计算需求，现有方法难以复制或构建。这给定理证明机器学习方法的研究带来了实质性障碍。本文通过引入LeanDojo消除了这些障碍：这是一个开源的Lean游乐场，包括工具包、数据、模型和基准。LeanDojo从Lean中提取数据，并允许以编程方式与证明环境进行交互。它包含对证明中前提的细粒度注释，为前提选择提供了宝贵的数据：这是定理证明中的一个关键瓶颈。利用这些数据，我们开发了ReProver（检索增强证明器）：这是第一个基于LLM的证明器，通过检索从庞大的数学库中选择前提。它成本低廉，只需一周的GPU训练时间。我们的检索器利用LeanDojo的程序分析能力来识别可访问的前提和困难的负例，从而使检索更加有效。此外，我们构建了一个新的基准，包括从Lean数学库中提取的96,962个定理和证明。它具有具有挑战性的数据拆分，要求证明器能够推广到依赖于在训练中从未使用过的新前提的定理。我们使用这个基准进行训练和评估，实验结果显示了ReProver相对于无检索基线和GPT-4的有效性。因此，我们提供了第一组无专有数据集的开源LLM定理证明器，并根据宽松的MIT许可发布，以促进进一步研究。
最近的研究CLIPA提出了一个逆比例尺度定律，用于CLIP训练 -- 即使用更大的图像/文本编码器，可以应用更短的图像/文本令牌序列长度进行训练。这一发现使我们能够使用大大减少的计算量来训练高性能的CLIP模型。在这项工作的基础上，我们在此介绍了具有两个关键贡献的CLIPA-v2。从技术上讲，我们发现这一逆比例尺度定律在微调阶段也适用，可以进一步减少计算需求。从经验上看，我们在规模上探索了CLIPA，将实验扩展到H/14模型，训练中观察到约130亿个图像-文本对。 我们的结果令人振奋 -- 仅分配10000美元的预算，我们的CLIP模型实现了令人印象深刻的零样本ImageNet准确率达到81.1%，超过了之前最佳的CLIP模型（来自OpenCLIP，80.1%）1.0%，同时将计算成本降低了约39倍。此外，再投资4000美元，我们可以进一步将零样本ImageNet准确率提升至81.8%。我们的代码和模型可在https://github.com/UCSC-VLAA/CLIPA 上找到。
相机姿态估计是一个长期存在的计算机视觉问题，迄今通常依赖于传统方法，如手工制作的关键点匹配、RANSAC 和捆绑调整。在本文中，我们提出在概率扩散框架内制定运动结构（SfM）问题，建模给定输入图像时相机姿态的条件分布。这种对一个古老问题的新颖观点具有几个优点。 (i) 扩散框架的性质反映了捆绑调整的迭代过程。 (ii) 该公式允许无缝集成来自极线几何的几何约束。 (iii) 它在典型的困难场景中表现出色，如稀疏视图和宽基线。 (iv) 该方法可以预测任意数量图像的内参和外参。我们证明了我们的 PoseDiffusion 方法在两个真实世界数据集上明显优于经典 SfM 流水线和学习方法。最后，观察到我们的方法可以在不经过进一步训练的情况下在数据集之间进行泛化。项目页面：https://posediffusion.github.io/
在语音社区中，解开言语话语中不相关信息是一个关键的研究课题。不同的与语音相关的任务侧重于提取不同的语音表示，同时最小化其他不相关信息的影响。我们提出了一个大规模语音语料库，以促进语音表示解缠的研究。3D-Speaker 包含超过 10,000 位说话者，每位说话者同时被多个设备录制，这些设备位于不同的距离，有些说话者还会说多种方言。多维音频数据的受控组合产生了一个多样化的语音表示纠缠矩阵，从而激发了解开它们的有趣方法。3D-Speaker 的多领域特性还使其成为评估大型通用语音模型、实验跨领域学习和自监督学习方法的合适资源。https://3dspeaker.github.io/
当今计算机视觉中许多像素级密集预测任务，如深度估计和语义分割，都依赖于预训练的图像表示。因此，策划有效的预训练数据集至关重要。不幸的是，有效的预训练数据集通常是那些仅使用模拟环境中的带注释的3D网格、点云和摄像机参数策划的多视角场景。我们提出了一种数据集策划机制，不需要任何注释。我们挖掘了两个数据集：MIMIC-1M 包含来自开源视频数据集和合成3D环境的130万多视角图像对，MIMIC-3M 包含310万多视角图像对。我们训练了多个自监督模型，采用不同的遮罩图像建模目标，展示了以下发现：在多个下游任务中，包括深度估计、语义分割、表面法线和姿态估计，使用 MIMIC-3M 训练的表示优于使用注释挖掘的表示。它们还优于被冻结的表示，并且当下游训练数据有限时，表现也更好。更大的数据集（MIMIC-3M）显著提高了性能，这是令人鼓舞的，因为我们的策划方法可以任意扩展以生成更大的数据集。MIMIC 代码、数据集和预训练模型已在 https://github.com/RAIVNLab/MIMIC 开源。
在上下文学习（ICL）中，通过在推断时简单展示少量示例，可以提高语言模型在各种自然语言处理任务上的性能。ICL能力为何出现尚不为人所了解，因为模型从未专门接受过此类示范训练。与探索ICL背后的隐含机制的先前工作不同，我们通过调查预训练数据来研究ICL。具体而言，我们首先采用迭代的基于梯度的方法，找到支持ICL的预训练数据的一个小子集。我们观察到，对这个小子集进行持续的预训练显著提高了模型的ICL能力，最多可提高18%。然后，我们将支持子集与预训练数据的随机子集进行对比，并发现：（1）支持ICL的预训练数据与下游任务的领域相关性并不更高。 （2）支持ICL的预训练数据中包含更多罕见的、长尾的标记。 （3）支持ICL的预训练数据是具有挑战性的示例，其中来自长距离上下文的信息增益低于平均水平，表明学习如何整合困难的长距离上下文有助于ICL。我们的工作通过分析实例级别的预训练数据，迈出了理解ICL的第一步。我们的见解有潜力通过积极指导未来预训练数据的构建来增强语言模型的ICL能力。
大型语言模型现在被调整以符合其创建者的目标，即“有益且无害”。这些模型应该对用户的问题作出有益回应，但拒绝回答可能造成伤害的请求。然而，对抗性用户可以构建输入以规避对齐尝试。在这项工作中，我们研究这些模型在与构建最坏情况输入（对抗性示例）的对抗用户交互时，保持对齐的程度。这些输入旨在导致模型发出本应被禁止的有害内容。我们展示现有基于自然语言处理的优化攻击不足以可靠地攻击对齐的文本模型：即使当前的基于自然语言处理的攻击失败，我们也可以通过蛮力找到对抗性输入。因此，当前攻击的失败不应被视为对齐的文本模型在对抗性输入下仍然保持对齐的证据。 然而，大规模机器学习模型的最新趋势是多模态模型，允许用户提供影响生成文本的图像。我们展示这些模型很容易受到攻击，即通过对输入图像进行对抗性扰动诱使其执行任意不对齐的行为。我们推测，改进的自然语言处理攻击可能会展示出对仅文本模型具有相同级别的对抗性控制。
我们研究了transformer处理两个挑战的能力：学习基本整数算术和推广到比训练中看到的更长序列。我们发现相对位置嵌入使简单任务的长度推广成为可能，比如加法：在5位数上训练的模型可以执行15位数的求和。然而，这种方法在乘法上失败，我们提出了训练集引导：向训练集中添加一些（10到50个）长序列。我们展示了引导可以使在5位数乘以3位数的乘法上训练的模型推广到35乘以3的示例。我们还展示了模型可以为不同的推广长度进行引导，并且引导样本大小随训练集大小的对数变化。最后，我们讨论了引导在算术之外的潜在应用。