大模型日报（8月8日学术篇）

我们希望能够搭建一个AI学习社群，让大家能够学习到最前沿的知识，大家共建一个更好的社区生态。

「奇绩大模型日报」知识库现已登陆飞书官方社区：

https://www.feishu.cn/community/article/wiki?id=7355065047338450972

点击「订阅社区精选」，即可在飞书每日收到《大模型日报》每日最新推送

如果想和我们空间站日报读者和创作团队有更多交流，欢迎扫码。

欢迎大家一起交流！

学习

miniCTX：使用（长）背景进行神经定理证明

我们介绍了miniCTX，该测试模型证明需要新定义、引理或其他上下文信息的形式数学定理的能力，这些信息在训练过程中没有观察到。miniCTX包含了从真实Lean项目和教科书中获取的定理，每个定理都与可能跨越成千上万个token的上下文相关联。模型的任务是在访问定理存储库中的代码的情况下证明一个定理，该存储库包含有利或需要证明的上下文。作为miniCTX的基线，我们引入了file-tuning，一个简单的配方，用于训练模型生成基于前一个文件内容的证明步骤。与仅在状态上进行微调的传统神经定理证明方法相比，文件调整大大优于。此外，我们的文件调整模型在标准miniF2F基准测试中提高了性能，实现了33.61%的通过率，这是1.3B参数模型的最新技术水平。除了miniCTX，我们还提供ntp-toolkit，用于自动提取和注释定理证明数据，使得很容易将新项目添加到miniCTX中，以确保在训练过程中不会看到上下文。miniCTX为评估神经定理证明器提供了具有挑战性和现实主义的视角。

http://arxiv.org/abs/2408.03350v1

EXAONE 3.0 7.8B 指令调整的大语言模型

我们介绍了LG AI Research开发的大语言模型（LLMs）家族中的第一个开放模型EXAONE 3.0 instruction-tuned language model。我们公开发布了7.8B instruction-tuned模型，以促进开放研究和创新。通过对各种公共和内部基准测试的广泛评估，EXAONE 3.0在指令跟踪能力上表现出高度竞争力，与其他类似规模的最新开放模型相比。我们的比较分析显示，EXAONE 3.0在韩语方面表现出色，同时在一般任务和复杂推理方面实现了引人注目的性能。凭借其强大的实用性和双语能力，我们希望EXAONE继续为专家人工智能的进步做出贡献。我们的EXAONE 3.0 instruction-tuned模型可在https://huggingface.co/LGAI-EXAONE/EXAONE-3.0-7.8B-Instruct获取。

http://arxiv.org/abs/2408.03541v1

1.5-Pints技术报告：几天内的预训练，而非几个月 — 你的语言模型在优质数据上蓬勃发展

本文提出了一种高效的计算方法来预先训练一种语言模型——“1.5-Pints”，仅用时9天，在作为指导性助手方面胜过最先进的模型。基于MT-Bench（一个模拟人类判断的基准），1.5-Pints胜过了苹果的OpenELM和微软的Phi。通过精心策划的预训练数据集，包含了570亿个token，并使用自动化工作流程和人工审查相结合。数据集的选择重点放在了被认为是解释性和“教科书般”的内容上，以帮助模型进行推理和逻辑推断，最终使其作为强大而多功能的AI模型。在模型架构方面，我们采用了修改后的Mistral tokenizer，以及用于更广泛兼容性的Llama-2 架构。在训练方面，我们采用了StableLM、TinyLlama和Huggingface Zephyr使用的方法。1.5-Pints模型表明，通过专注于LLM训练中数据质量而不是数量，我们可以显著减少所需的训练时间和资源。我们相信这种方法不仅将使预训练更具有可访问性，而且还将减少我们的碳足迹。我们的研究发现和资源是开源的，旨在促进该领域的进一步发展。1.5-Pints模型有两个版本：2K和16K上下文窗口。

http://arxiv.org/abs/2408.03506v1

EnJa: 大型语言模型上的集成破解

摘要：随着大语言模型（LLMs）越来越多地被部署在安全关键应用中，它们对潜在破解的脆弱性 – 恶意提示可能会使LLMs的安全机制失效 -引起了越来越多的研究关注。本文介绍了集成提示级和标记级破解的概念，提出了一种新颖的EnJa攻击，以隐藏有害指令并提高攻击成功率，通过模板连接器将两种破解攻击相连，评估了EnJa对多个已对齐模型的有效性，并表明它实现了最先进的攻击成功率，查询更少，比任何单独的破解都更加强大。