（本文阅读时间：7分钟）
自我进化实现Rust自动形式化证明
基于图模式的理解基准测试
IGOR: 通过学习统一的动作表示空间让机械臂模仿人类动作
自我进化实现Rust自动形式化证明
论文链接：
https://arxiv.org/pdf/2410.15756
形式化验证是通过数学方法来证明软件正确性的手段，它要求开发者用形式化语言写出软件系统需要满足的属性，再写出形式化的证明，用自动定理求解器去证明软件满足这些属性。高昂的人工成本使得开发者对使用这类方法望而却步，这也导致形式化证明的代码很少，即便是大语言模型，也由于缺乏训练数据难以生成这样的证明代码。
对此，微软亚洲研究院的研员们通过让大语言模型自我进化的方式，实现了 Rust 代码上的自动形式化证明。自我进化框架能够迭代式地合成更高质量的数据，并用于训练更强的能够生成形式化证明代码的模型。
具体来说，研究员们首先收集了大量适合于证明的 Rust 代码，将它们翻译成能够被证明的形式化语言 Verus，所有被 Verus 编译器通过的代码将被保留作为种子数据进行合成。接下来，用大模型自我进化的方式生成 Verus 规范，即代码需要满足的形式化属性，在每一轮进化中，前一轮生成的规范将用于训练一个新的、经过微调的开源模型，从而在下一轮微调中生成更多质量更高的规范。最后，为了获得能够通过验证的代码，模型还需要生成证明代码以证明上述规范能被满足。研究员们同样使用了自我进化的方式微调大模型，在这个过程中，所有合成的能被 Verus 验证的代码将会作为训练语料，同时，在生成过程中的错误代码会和它的错误信息一起，作为训练模型自我 debug 能力的语料。
图1：自我进化框架示意图
在由 Verus 专家构建的基准上，经过自我进化的开源模型在自动生成证明代码的任务上的 pass@10 通过率达到了70.50%，相较于未经训练时的17.27%有了巨大的飞跃。这一成果充分验证了本篇论文中提出的自我进化数据合成与微调框架的有效性。
大语言模型对于图模式（graph pattern）理解的基准测试
论文链接：
https://arxiv.org/pdf/2410.05298
目前，大量工作已经验证了大语言模型（LLMs）可以进行最基本的图推理任务，即 LLMs 可以找到两个节点之间的连接关系。图不仅仅可以通过点的连接关系表示特征，也可以通过带一定特征的子图表示，比如，图中是否含有三角形连接关系，分子图中是否含有苯环结构，社交图中是否含有星状结构。这些图模式在图挖掘以及图学习中非常重要。
在本篇论文中，研究员们测试了包括 GPT-4、GPT-4o 和 O1 在内的 7 种大语言模型在图模式识别中的能力，实验设计中包含了总共4大任务以及11种子任务。具体而言，研究员们考察了这些模型是否能够在每个图中使用子图定义和子图匹配的方法来识别图中的子图特征。此外，该测试还评估了模型在没有特定子图提示的情况下，总结图数据集的规律并预测其中的特征，以及这些特征与数据标签之间的关系。最后，研究员们在真实数据集上测试了大语言模型的图模式匹配能力及其图分类的效果。
表1：对不同类型的图模式表达方式进行测评
根据不同大语言模型在各类图模式任务中的表现，研究员们总结出了一些关于大语言模型在图模式任务上的重要发现。例如：1. 大语言模型具备基础的图模式理解能力，随着模型能力的提升（如 O1 模型），在某些任务中的预测性能会显著提高；2. 大语言模型可以利用先验知识增强图模式理解能力，并将这种能力扩展到真实数据集的分析；3. 大语言模型在图模式认知过程中可能会采用不同的算法或策略，这将影响模型的预测准确性。
这些发现为未来基于大语言模型的图模型开发以及提升其对复杂逻辑结构的理解，提供了重要指导。研究员们也将持续对相关问题进行更加深入的探索。
IGOR: 通过学习统一的动作表示空间让机械臂模仿人类动作
论文链接：
https://arxiv.org/pdf/2411.00785
项目链接：
https://aka.ms/project-igor
在训练具身智能领域的基础模型时，带有标签的高质量机器人数据是保证模型质量的关键，但直接采集机器人数据成本较高。考虑到互联网视频数据中展示了丰富的人类活动，包括人类是如何与现实世界中的各种物体进行交互的。那么，是否可以通过视频数据为人类和机器人学习一个统一的动作表示空间，以实现跨任务和智能体的知识迁移和下游任务效果的提升呢？基于这一出发点，研究员们提出了图像目标表示（IGOR，Image-Goal Representation）。
如何学到人类和机器人统一的动作表示？
IGOR 使用了潜在动作模型 LAM（Latent Action Model），将初始状态和目标状态之间的视觉变化压缩为低维向量，并通过最小化初始状态和动作向量对目标状态的重建损失进行训练。这样，具有相似视觉变化的图像状态会具有相似的动作向量，代表了它们在语义空间而非像素空间上的变化。
图2：IGOR 框架实例，包含了三个基础模型：Latent Action Model, Policy Model 和 World Model
通过 LAM，研究员们可以将互联网规模的视频数据转化为带有潜在动作标注的数据，大大扩展了具身智能基础模型能够使用的数据量。这个统一的潜在动作空间使研究员们能够在几乎任意由机器人和人类执行的任务上训练 Policy Model 和 World Model。通过结合 LAM 和 World Model，IGOR 成功地将一个视频中的物体运动“迁移”到了其他视频中。并且，这些动作实现了跨任务和跨智能体的迁移。也就是说，用人类的行为给机器人做演示，机器人也能做出正确的动作。如下图所示，LAM 得到的潜在动作表示可以同时实现跨任务（用手移动不同物体）和跨智能体（用手的移动指导机械臂的移动）的迁移。
图3：Latent Action 实现跨任务和智能体的迁移
IGOR 开辟了通过大量人类和机器人视频预训练学习动作表示并泛化到不同任务和智能体的新范式。通过从大量视频中学到的动作表示，IGOR 可以实现机器人轻松模仿人类动作，进而实现更通用的智能体。
你也许还想看：
