Lean & GPT | 构建自己的 GPT

发表于 更新于 分类于 阅读次数： 字数： 1.3k 时间 ≈ 5 分钟
OpenAI 发布了 GPTs，允许用户在 ChatGPT 上通过对话构建自己的 GPT。我第一时间也做了测试，并尝试了两个任务，构建 LEAN 形式定理生成器，以及增强 ChatTool 使用体验的工具。

前些天(11.10) OpenAI 发布了 GPTs，允许用户在 ChatGPT 上通过对话构建自己的 GPT。我第一时间也做了测试，并尝试了两个任务，构建 LEAN 形式定理生成器，以及增强 ChatTool 使用体验的工具。

对于 OpenAI 的这类更新，LEAN 形式化社区也有帖子跟进，这里收集了一些讨论，以及自己的尝试。

相关论坛帖子：
Kevin Buzzard: make your own GPT
Jesse Michael Han: The personal AI proof engineer

GPTs

第一个链接是社区大佬 Kevin Buzzard 开的帖子：

Lots of people on Twitter going on about this new “make your own language model” feature which OpenAI just demoed a day or so ago. What happens if you attempt to make an algebraic geometry chatbot e.g. by uploading a ton of stuff from the Stacks Project? Presumably these things are still hallucinating left right and centre? Is there really any breakthrough here or is it just about OpenAI enabling users to fine tune a model?

第一眼我也感觉这可能是个大的 breakthrough。我日常用 ChatGPT 写代码时，会先人工搜索代码关联的文档，贴在问题前边，这样子能提高生成内容的准确性。但使用 GPTs 发现它并没有充分利用文档来消除幻觉，至少从目前的尝试来看是这样，它看起来仍像是概念性的产品，也可能使用姿势不对。

当前，OpenAI 这次更新增加的内容包括：

  1. gpt-4-1106-preview 更新知识库到 2023.04，支持 128k 上下文窗口，推理速度更快，价格降低 2~3 倍
  2. gpt-4-vision-preview 开放多模态 API
  3. 增加了 assistant API，与 Agent 相关，支持调用工具， CodeInterpreter 以及文档检索
    20231114094116
  4. 开放了用户自定义 GPT 的功能，且后续将开放商店，允许用户分享自己的 GPT

关于上下文窗口，帖子下有人提到了前两周开源的一个工作 YaRN：

Yeah! 128K iirc
You could also try https://www.reddit.com/r/LocalLLaMA/comments/166je92/llama2_with_128k_context_length_thanks_to_yarn/
There’s a 128K version of Mistral 7B as well: https://github.com/jquesnelle/yarn#mistral and Code Llama natively supports 100K.

YaRN 的论文和 GitHub 仓库：

仓库开源了的两个模型：llama 和 Mistral。如下图，Yarn-Llama-2 在 100k+ 上下文的情况下，保持了较低的 PPL。

20231114010527

此外 Meta 的 code-llama 本身也支持 100k+ token。

GPTs 使用方法

GPTs 功能需开通 GPT plus 才能用。点击左侧 Explore，在右边找到创建 GPT 的入口。

20231114094927

聊天页面分成两个部分，左边通过对话提出需求，构建 GPT；右边是直接的生产环境。

20231114094851

左侧 create 与 GPT 对话，它通过引导用户提出需求，根据需求生成和更新 instructions。等价地，可以在 configure 页面直接编辑需求。

通过 configure 可以看到它更新的内容：

  • 用 DALL·E 生成头像 logo
  • 生成 Description 和 instructions
  • 生成提问模板
  • 提供上传文件的选项，用于知识库检索
  • 提供调用工具的能力：CodeInterpreter，网页浏览，DALL·E 以及用户自定义 API

20231114095657

OpenAI 更新的这些模块都能找到开源平替。但它将这些模块整合在一起，且提供一个简单易用的使用平台，试图进一步抢占市场。当然，也有好的一面，它提供的用法可以模仿借鉴，并用开源模型构建替代版。。。

AI Engineer

Jesse Michael Han

Today, we announced our plans to build the personal AI proof engineer for Lean, in partnership with the Lean FRO.
https://morph.so/blog/the-personal-ai-proof-engineer/
The personal AI proof engineer will know mathlib and the relevant mathematical literature better than you do. It will be able to explain mathlib’s APIs in natural language and make it 100x easier for novices to ramp up and become productive. It will stay up to date on the latest changes, PRs, branches, and forum discussions. It will be accessible from the web, mobile, and the IDE. Within the IDE, it will offer advice, suggest relevant lemmas, and automate proof search.

这个帖子涉及两个团队，Morph Lab 和 Lean FRO，共同目的是构建数学领域，特别是形式化领域的 AI 工程师（AI proof engineer)。

浅浅搜了下，这两个团队都和伦敦帝国理工大学相关，也就是 Kevin Buzzard 大佬所在的学校。Morph Lab 的目标是 “bring the personal AI domain expert to everyone”。Lean PRO 则致力于推进形式数学的变革，解决 Lean 证明助手关于可扩展性、可用性和证明自动化的挑战。

该团队开源了 Morph Prover v0 7B 模型，首个面向 LEAN 用户的使用对话数据训练的开源模型。

该模型由 Nous Research 以及由 Sanmi Koyejo 教授领导的 Stanford Trustworthy AI Research (STAIR) 小组共同训练的。Morph Prover v0 7B 是对 Mistral 进行微调的聊天模型，训练数据来自 Zulip、Mathlib、GitHub、数学教科书等。在自动形式化方面达到了新的SOTA。它采用专有的合成数据管道进行训练，使用由 Morph Code Index 生成的代码数据。

注：MCI 是 VsCode 拓展 Rift的一部分，支持通过对话界面直接操作和修改源码（有空尝试一下）。

简单来说，这个团队意在开发面向 LEAN 的 AI SWE(Software Engineer)，且很快会提出一个支持交互使用的免费版。

关联的链接：