斯坦福大学研究人员提出人工智能框架来实现和验证复杂的算法

Parsol是由斯坦福大学的一组研究人员创建的AI框架，它使用大型语言模型（LLM）推理将自然语言中的分层函数描述转换为代码中的实现。此外，研究人员认为，Parcel可用于机器人规划和定理证明。

正如InfoQ已经介绍的那样，许多LLM已经可用于将程序的文本描述转换为代码，例如OpenAI Codex，开源PolyCoder，GitHub Copilot和其他基于GPT-3的模型。

Parcel试图通过镜像人类程序员用来生成复杂程序的模式来超越LLM已经提供的代码，即“分解抽象计划，直到它可以自动解决”，研究人员在他们的论文中解释说。

Parcel背后的一般思想如下：人类或LLM使用Parcel语言来描述任务如何在子任务中分解，称为强连接组件（SCC）。然后，Parcel编译器使用代码LLM和约束求解器来实现每个SCC。最后，将实现的 SCC 组合回执行原始任务的程序。

LLMs只需几个例子就可以生成Parsol，并且他们的解决方案优于APPS数据集中竞争级问题的先前工作，包括AlphaCode和两者（组合）。而且，两个版本的法典。

Parcel编译器接受要实现的函数的自然语言描述和一组必须满足的约束，例如单元测试的集合。给定此输入，将提示代码LLM为每个函数生成实现并组合它们，直到找到满足约束的函数。

这是如何描述康威生命game的一部分的示例，包括一个约束，指示函数在使用输入调用时应返回一个整数：([[1, 0], [0, 1]], 0, 0)

count_living_neighbors(grid, i, j): count the number of living neighbors of the cell at the index (i, j)

type_fn_output(fn, args): returns the type of the output of a function called with args
count_living_neighbors, ([[1, 0], [0, 1]], 0, 0) -> int

Parcel最简单的情况是所有函数都有约束，并且没有一个是递归的。

在这种情况下，[...]调用图中没有任何循环，我们可以首先实现叶函数，然后是它们的父函数，依此类推，直到程序实现。

递归和没有约束的函数使事情变得更加困难。在这种情况下，重组 SCC 的复杂性随着最大 SCC 的大小呈指数级增长。为了使重组易于处理，Parcel考虑了其定义相互依赖的函数集，并假设它们之间的状态性不会干扰依赖断言，以便能够找到满足所有约束的集合。

Parcel提供正确程序的一个关键步骤是分解。事实上，如果一个函数描述太复杂，研究人员说，LLM用来将其转换为代码的代码就无法正确地做到这一点。在这种情况下，解决方案将进一步将复杂函数分解为更简单的函数。

与此相关，代码LLM生成的代码质量通常可能与输出语言有很大差异，训练数据中代表性不足的语言表现更差。

研究人员说，虽然Parcel已被证明能够实现稳健的算法推理，但仍有许多问题悬而未决，并且有很多机会可以扩展和改进框架。