大语言模型(LLMs)应该用什么语言编程？

大语言模型应该用强类型语言编写代码，还是需要一种全新的语言？

我们正处于软件开发的转折点。几十年来，编程语言的发展一直以人类开发人员为主要服务对象。我们优化了可读性、表达力和认知易用性——这些目标在由血肉之躯的工程师编写每一行代码时是合理的。但随着人工智能代理越来越多地接管编写软件的任务，我们不得不面对一个根本性问题：如果我们花了数十年时间完善编程语言，而这些语言完全不适合我们未来编写代码的新方式，该怎么办？

迹象已经显现。Python和JavaScript之所以主导了编程领域，并非因为它们能生成最健壮的软件，而是因为它们反映了人类解决问题的方式。它们的弱类型、容错特性使得初学者更容易上手。但是，当“开发人员”是一个没有认知限制(除了他们经过训练的几个结构良好的例子之外)的大语言模型时，这些对人类友好的设计决策看起来更像是一个错误，而不是一个特点。

大语言模型(LLMs)的弱类型语言与强类型语言

考虑我们目前如何处理AI代码生成。我们用自然语言(本身就是一种本质上模糊的媒介)提示模型，并要求它生成由人类设计以实现灵活且可解释性的语言代码。结果是双重模糊性：不精确的输入产生不精确的输出。这就像让某人将一首诗从一种语言翻译成另一种语言，然后奇怪为什么细微差别会丢失。

这比你想象的更重要。虽然 JavaScript 的松散类型系统可能帮助初级开发者快速实现功能，但它恰恰产生了那种使 AI 生成的代码不可预测的不确定性。当人类编写 if (user.id) 时，他们理解背后隐含的类型转换机制。当 AI 编写相同代码时，这种理解仅存在于训练过程中学习的统计模式中——这是一种远不如人类理解可靠的基础。

JavaScript 是世界上最受欢迎的编程语言，这更加剧了这种情况。主流的大语言模型(LLMs) 训练所使用的代码大部分可能是 JS 语言，这些代码来自网络上无数的示例存储库和 StackOverflow (🥲) 问题。人们已经清楚地认识到，基于旧版本/多个版本的流行库进行的大语言模型(LLMs)训练会对代码生成产生负面影响；对于语言本身来说，情况可能也是如此。

与此同时，Haskell 和 Erlang 等函数式语言提供了一个引人注目的替代框架。它们对不可变性、强类型和数学基础的强调，正是能够引导AI系统产生更可靠输出所需的约束条件。JavaScript说“边做边想”，而Haskell说“在运行前先证明它能工作”。对于AI系统而言，这种差异不仅是哲学层面的——更是实践层面的(稍后将详细讨论)。

Erlang 等语言内置的并发和分布式编程模型也与人工智能系统自然运作的方式高度契合。这些语言从底层设计上就旨在通过 组合与隔离 原则处理复杂性，而当复杂性由统计模型而非人类直觉管理时，这些原则的价值愈发凸显。尽管它们可能对人类编写者而言更具挑战性，但对于我们通过代理来强制执行这些原则而言，它们可能至关重要。

形式验证与数学证明代码

这让我们提出一个更激进的观点：形式验证。虽然大多数工程师熟悉单元测试——通过选择特定案例验证预期行为——形式验证则采用数学方法证明正确性。它不是检查代码在少数测试案例中是否正常工作，而是从理论上证明其在所有可能案例中均正确运行。

经典的正式验证示例涉及如此简单的任务：在数组中找到最大值。单元测试可能会检查几个不同的数组并确认函数返回正确答案。而正式验证会通过数学方法证明，该算法能够正确识别任何有效输入数组中的最大值，无论数组大小或内容如何。

这种严格程度传统上仅适用于关键任务系统——航空航天、医疗设备、金融基础设施等领域，因为这些系统中的故障不仅会造成不便，还可能导致灾难性后果。形式验证的工具链也反映了这一小众地位：像Dafny、SPARK Rocq和TLA+等语言仍主要用于研究领域，且在许多方面不适合日常软件开发(尽管我希望这种情况会改变)。

但随着人工智能代理开始编写更多代码，我认为这一领域将变得极为重要。问题不在于我们是否能承担形式验证的开销，而在于我们是否能承担_不进行形式验证_的风险。当人类编写代码时，我们可以依赖他们对上下文、意图和边界情况的理解。当人工智能编写代码时，我们需要更强大的——在这种情况下是数学上的——保证。

挑战在于速度和实用性。当前的正式验证方法对于现代开发所要求的快速迭代周期而言，速度太慢且过于繁琐。如果我们要要求人工智能代理证明他们编写的每个函数的正确性，那么这个过程需要在几秒钟内完成，而不是几分钟或几小时。

早期的研究正在探索大语言模型(LLMs)本身如何生成验证所需的定理和证明，但这些方法受到正式方法中高质量训练数据稀缺的限制。这是一个先有鸡还是先有蛋的问题：我们需要更多经过正式验证的代码来训练更好的验证模型，但我们需要更好的验证模型来使正式验证足够实用，以产生这些训练数据。

如果大语言模型(LLMs)需要一种全新的编程语言怎么办？

回到本文的最初问题，如果现有语言都不适合大语言模型生成代码怎么办？可能存在更根本的机会：创建专门为人工智能系统设计的编程语言。

从根本上讲，当前的人工智能代码生成方法效率极低。我们从自然语言(模糊的)开始，将其翻译成现有编程语言(仍存在一定模糊性)，然后编译成机器代码(最终明确无误)。这至少涉及三个编译阶段，每个阶段都可能引入错误和低效(还记得之前的诗歌类比吗)。

如果我们能简化这个流程呢？与其让AI系统在人类设计的语言约束下工作，我们不妨创建能更直接连接自然语言意图与机器执行的语言。

这方面的工作已经在进行了。我最近会见了一个来自麻省理工学院的团队，他们使用大语言模型(LLM)创造了一种全新的编程语言——在他们的项目之前，这种语言从未存在过。这种语言受到限制且专门化，但只需向他们的 AI 系统展示几个例子，它就能可靠地生成这种新语法中的代码。与传统语言生成的同等代码相比，结果更可预测、更可验证。

这不仅仅是一个理论上的练习。这种语言内置的限制可以强制执行使验证成为可能的正式属性。通过设计一种在语法层面上消除整个错误类别的语言，我们可以大大减轻验证负担，同时提高人工智能生成的代码的可靠性。

DSPy 和大语言模型(LLMs) 并不是黑匣子的想法

影响不仅限于我们用于最终代码生成的语言。像DSPy这样的项目正在探索自然语言是否真的是提示AI系统的正确接口。与其让模型解释自由形式的文本指令，DSPy提供结构化的编程接口，使我们能够更可靠地组合AI能力。

这代表了对人工智能系统思考方式的更广泛转变。与其将它们视为通过自然语言进行沟通的黑盒子，我们或许更应开发更结构化、程序化的接口，以减少模糊性并提高可预测性。

与传统软件开发之间的平行关系令人惊叹。早期程序员直接与机器码打交道，随后是汇编语言，再到越来越抽象的高级语言。每一层抽象都使编程对人类更易于访问，同时保持或提高了底层系统的可靠性。我们可能正接近人工智能领域的类似转折点，其中最有效的接口未必是最类似人类的。

展望未来

未来的编程语言很可能与当今的编程语言大不相同。它们将更注重数学严谨性而非人类可读性，更注重形式化保证而非灵活表达能力，更注重组合清晰性而非语法糖。这并非为了让编程变得更难——而是为了在编程者是人工智能(其核心优势与局限性与人类开发者截然不同)时，使编程更加可靠。

这一转变不会一蹴而就，也不会普遍适用。在某些场景下，人类友好的语言仍将是最佳选择。但随着人工智能代理在软件开发中扮演越来越核心的角色，我们使用的语言和工具必然会演变，以适应它们独特的能力和限制。

本文文字及图片出自 What language should LLMs program in?