AI研究论文每日精选

我们介绍了 DeepSeek-Prover-V1.5，这是一个开源语言模型，专为在 Lean 4 中进行定理证明而设计，通过优化训练和推理过程对 DeepSeek-Prover-V1 进行了增强。该模型在 DeepSeekMath-Base 上进行了预训练，专门针对形式数学语言进行了优化，然后使用从 DeepSeek-Prover-V1 衍生的增强形式定理证明数据集进行监督微调。进一步的改进是通过来自证明助手反馈的强化学习（RLPAF）实现的。除了 DeepSeek-Prover-V1 的单次整个证明生成方法，我们提出了 RMaxTS，这是蒙特卡洛树搜索的一种变体，采用内在奖励驱动的探索策略来生成多样化的证明路径。DeepSeek-Prover-V1.5 显示出明显的改进，相对于 DeepSeek-Prover-V1，在高中水平的 miniF2F 基准测试集（63.5%）和本科水平的 ProofNet 基准测试集（25.3%）上取得了新的最先进结果。

大型语言模型（LLMs）取得了显著进展，然而，常见的学习范式将LLMs视为被动信息存储库，忽视了它们在主动学习和对齐方面的潜力。一些方法使用LLMs生成的合成数据来训练模型，探索主动对齐的可能性。然而，这些一次性对齐方法与人类的持续自动对齐之间仍存在巨大差距。在本文中，我们介绍了I-SHEEP，一种迭代自我增强范式。这种类似人类的范式使LLMs能够从零开始持续自我对齐。与本文中首次迭代的一次性对齐方法Dromedary sun2023principledriven相比，I-SHEEP可以显著增强Qwen和Llama模型的能力。在Qwen-1.5 72B模型的后续迭代中，I-SHEEP在Alpaca Eval中实现了最大相对改进78.2％，在MT Bench中为24.0％，在IFEval准确性上绝对增加了8.88％。此外，I-SHEEP在各种标准基准生成任务中超越了基准模型，在代码生成任务中平均提高了24.77％，在TrivialQA中为12.04％，在SQuAD中为20.29％。我们还根据实验结果提供了新的见解。我们的代码、数据集和模型可在https://anonymous.4open.science/r/I-SHEEP 上获取。

训练神经网络是一项庞大的工作，类似于将知识刻在石头上：一旦完成了这个过程，编辑网络中的知识几乎是不可能的，因为所有信息都分布在网络的权重中。我们在这里探讨了一个简单而引人注目的替代方案，即将深度神经网络的表征能力与数据库的灵活性相结合。将图像分类任务分解为图像相似度（从预训练嵌入中）和搜索（通过从知识数据库中快速检索最近邻）两部分，我们构建了一个简单而灵活的视觉记忆，具有以下关键能力：（1.）能够灵活地跨越各种规模添加数据：从单个样本到整个类别以及十亿级数据；（2.）通过遗忘和记忆修剪来删除数据的能力；（3.）一个可解释的决策机制，我们可以干预以控制其行为。综合来看，这些能力全面展示了显式视觉记忆的好处。我们希望这可能有助于探讨在深度视觉模型中应如何表示知识，超越了将其刻在“石头”权重中的方式。

数据集精炼或压缩的目标是将大规模训练数据集压缩成一个更小的合成数据集，使得神经网络在精炼和原始数据集上的训练性能相似。尽管训练样本数量可以大幅减少，但当前最先进的方法严重依赖于大量的软标签来实现令人满意的性能。因此，所需存储空间甚至可以与原始数据集相媲美，尤其是对于大规模数据集而言。为了解决这一问题，我们提出了一种新颖的轻标签框架，称为HeLlO，旨在实现有效的图像到标签投影器，通过这些投影器可以直接从合成图像在线生成合成标签。具体而言，为构建这样的投影器，我们利用开源基础模型中的先验知识，例如CLIP，并引入类似于LoRA的微调策略来缓解预训练模型和目标分布之间的差距，从而将用于生成软标签的原始模型精炼为一组低秩矩阵。此外，我们提出了一种有效的图像优化方法，进一步减少原始和精炼标签生成器之间的潜在误差。大量实验证明，仅需原始软标签完整集所需存储空间的约0.003%，我们就能在大规模数据集上实现与当前最先进的数据集精炼方法相媲美的性能。我们的代码将会提供。

在人工智能领域，合成充满运动且时间连贯的视频仍然是一个挑战，尤其是在处理较长时间跨度时。现有的文本到视频（T2V）模型通常采用空间交叉注意力进行文本控制，等效地引导不同帧的生成而无需特定于帧的文本引导。因此，模型理解提示中传达的时间逻辑并生成具有连贯运动的视频的能力受到限制。为了解决这一局限性，我们引入了FancyVideo，这是一种创新的视频生成器，通过精心设计的跨帧文本引导模块（CTGM）改进了现有的文本控制机制。具体而言，CTGM在交叉注意力的开始、中间和结尾分别整合了时间信息注入器（TII）、时间亲和度细化器（TAR）和时间特征增强器（TFB），以实现特定于帧的文本引导。首先，TII将来自潜在特征的特定于帧的信息注入到文本条件中，从而获得交叉帧文本条件。然后，TAR在时间维度上优化交叉帧文本条件与潜在特征之间的相关性矩阵。最后，TFB增强潜在特征的时间连贯性。包括定量和定性评估的大量实验证明了FancyVideo的有效性。我们的方法在EvalCrafter基准测试上实现了最先进的T2V生成结果，并促进了动态和连贯视频的合成。视频展示结果可在https://fancyvideo.github.io/ 上查看，我们将公开我们的代码和模型权重。

尽管语言模型（LMs）的许多能力随着训练预算的增加而提高，但规模对幻觉的影响尚未完全被理解。幻觉有许多形式，并且没有被普遍接受的定义。因此，我们专注于研究只有在训练集中完全正确答案出现的那些幻觉。为了充分控制训练数据内容，我们构建了基于知识图谱（KG）的数据集，并用它来训练一组规模逐渐增大的LMs。我们发现，对于固定的数据集，规模更大、训练时间更长的LMs产生的幻觉较少。然而，在训练数据的不到5%上产生幻觉需要比Hoffmann等人（2022年）报告的最佳模型规模大一个数量级，因此需要更多的计算资源。考虑到这种昂贵性，我们研究了幻觉检测器如何依赖规模。虽然我们发现检测器的规模提高了固定LMs输出的性能，但我们发现LM规模与其幻觉的可检测性之间存在反比关系。

尽管从头开始训练大型语言模型(LLMs)确实可以导致具有独特能力和优势的模型，但会产生巨大成本，并可能导致能力的冗余。知识融合旨在通过轻量级持续训练，将具有不同架构和能力的现有LLMs整合成一个更强大的LLM，从而减少昂贵的LLM开发需求。在这项工作中，我们提出了一个新的框架，用于通过两个主要阶段融合聊天LLMs的知识，最终形成FuseChat。首先，我们对具有不同结构和规模的源聊天LLMs进行成对知识融合，通过轻量级微调创建具有相同结构和大小的多个目标LLMs。在此过程中，引入了基于统计的标记对齐方法作为融合具有不同结构的LLMs的基石。其次，我们在参数空间内合并这些目标LLMs，提出了一种基于微调前后参数更新量大小确定合并系数的新方法。我们使用包括OpenChat-3.5-7B、Starling-LM-7B-alpha、NH2-SOLAR-10.7B、InternLM2-Chat-20B、Mixtral-8x7B-Instruct和Qwen-1.5-Chat-72B在内的六个知名聊天LLMs，实施并验证了FuseChat。在两个指令遵循基准测试AlpacaEval 2.0和MT-Bench上的实验结果表明，FuseChat-7B优于各种规模的基线模型。我们的模型甚至可以与更大的Mixtral-8x7B-Instruct相媲美，并在MT-Bench上接近GPT-3.5-Turbo-1106。我们的代码、模型权重和数据可在https://github.com/fanqiwan/FuseAI 上公开获取。

由于其在稠密模型上表现优异，混合专家（MoE）框架已成为大型语言模型中流行的架构。然而，在大规模情况下从头开始训练MoE是代价高昂的。现有方法通过独立预训练多个密集专家模型并使用它们来初始化MoE来缓解这一问题。这是通过使用专家的前馈网络（FFN）来初始化MoE的专家，同时合并其他参数来实现的。然而，这种方法仅限于将密集模型参数重用于仅限于FFN层，从而限制了将这些模型升级为MoE时的优势。我们提出了BAM（Branch-Attend-Mix），这是一种简单而有效的方法，可以解决这个缺点。BAM充分利用了专门的密集模型，不仅使用它们的FFN来初始化MoE层，还通过将专家的注意力参数完全初始化为Mixture of Attention（MoA）层的软变体来充分利用专家的注意力参数。我们探索了两种升级注意力参数的方法：1）从密集模型初始化单独的注意力专家，包括所有注意力参数，以获得最佳的模型性能；2）跨所有专家共享关键和值参数，以促进更好的推理效率。为了进一步提高效率，我们将并行注意力变换器架构应用到MoE中，这允许同时计算注意力专家和FFN专家。我们对范围从5.9亿到20亿参数的种子模型进行的实验表明，BAM在困惑度和下游任务性能方面均超过了基线，在相同的计算和数据约束条件下。

本文介绍了PeriodWave-Turbo，一种通过对抗流匹配优化实现高保真和高效波形生成模型。最近，条件流匹配（CFM）生成模型已成功应用于波形生成任务，利用单一向量场估计目标进行训练。尽管这些模型能够生成高保真波形信号，但与基于GAN的模型相比，它们需要更多的ODE步骤，后者只需要单一生成步骤。此外，由于嘈杂的向量场估计导致生成的样本通常缺乏高频信息，无法确保高频重现。为解决这一限制，我们通过引入固定步长生成器修改增强了预训练的CFM生成模型。我们利用重构损失和对抗反馈来加速高保真波形生成。通过对抗流匹配优化，只需1,000步微调即可在各种客观指标上实现最先进的性能。此外，我们将推理速度从16步显著降低至2或4步。此外，通过将PeriodWave的骨干网络参数从29M扩展到70M以提高泛化能力，PeriodWave-Turbo实现了前所未有的性能，在LibriTTS数据集上的语音质量感知评估（PESQ）得分为4.454。音频样本、源代码和检查点将在https://github.com/sh-lee-prml/PeriodWave 上提供。

人机对话提供了一个窥视用户真实场景、行为和需求的窗口，因此对于模型开发和研究而言是宝贵的资源。尽管盈利公司通过其模型的API收集用户数据，将其用于内部改进自己的模型，但开源社区和研究界却落后于此。 我们介绍了ShareLM集合，这是一个包含与大型语言模型的人类对话的统一集合，以及其附带的插件，这是一个用于自愿贡献用户与模型对话的Web扩展。在少数平台分享他们的聊天记录的情况下，ShareLM插件增加了这一功能，从而允许用户从大多数平台分享对话。该插件允许用户对他们的对话进行评分，无论是在对话还是回复级别，并且在离开用户本地存储之前，用户可以删除他们希望保持私密的对话。我们将插件对话作为ShareLM集合的一部分发布，并呼吁在开放式人机数据领域加大社区努力。 代码、插件和数据均可获得。

最近，新颖视角合成（NVS）和三维生成取得了显著进展。然而，这些工作主要集中在有限的类别或合成的三维资产上，这些资产不利于推广到具有挑战性的野外场景，并且无法直接用于二维合成。此外，这些方法严重依赖摄像机姿势，限制了它们在现实世界中的应用。为了克服这些问题，我们提出了MVInpainter，将三维编辑重新构建为多视角二维修补任务。具体而言，MVInpainter通过参考引导部分修补多视角图像，而不是难以从头开始生成完全新颖的视角，这在处理野外NVS的困难程度上大大简化了，并利用未掩盖的线索而不是显式的姿势条件。为了确保跨视图一致性，MVInpainter通过来自运动组件的视频先验和来自连接的参考键和值注意力的外观引导进行增强。此外，MVInpainter还结合了槽注意力，以从未掩盖区域聚合高级光流特征，以控制摄像机移动，并实现无姿势的训练和推断。在面向对象和前向数据集上进行了充分的场景级实验，验证了MVInpainter的有效性，包括多视角对象去除、合成、插入和替换等多样化任务。项目页面为https://ewrfcas.github.io/MVInpainter/。

评估大型语言模型（LLMs）的能力通常具有挑战性，部分原因在于很难找到它们在训练过程中未接触过的任务。我们为了应对这一挑战迈出了一步，转向一个新任务：专注于符号图形程序，这是一种流行的图形内容表示形式，可以以过程方式生成视觉数据。LLMs在程序合成方面显示出令人兴奋的潜力，但它们是否理解符号图形程序呢？与传统程序不同，符号图形程序可以转换为图形内容。在这里，我们通过LLMs回答与图形内容相关的问题的能力来表征它们对符号程序的理解。这个任务具有挑战性，因为仅通过符号程序很难回答这些问题，但通过人类实验验证，从相应的图形内容回答这些问题将会很容易。为了理解符号程序，LLMs可能需要具备想象对应图形内容的能力，而无需直接访问渲染的视觉内容。我们利用这个任务来评估LLMs，创建了一个用于语义理解符号图形程序的大型基准。这个基准是通过程序-图形对应构建的，因此需要较少的人力。我们在我们的基准上评估当前的LLMs，以阐明它们从程序推理视觉场景的能力的初步评估。我们发现这个任务可以区分现有的LLMs和被认为在推理方面表现良好的模型。最后，我们引入了符号指令调整（SIT）来改善这种能力。具体来说，我们使用符号程序生成的问题和图像查询GPT4-o。这些数据然后用于微调LLMs。我们还发现SIT数据可以提高LLMs的一般指令遵循能力。