通过奇克谱层次评估大语言模型的形式推理能力

大语言模型（LLM）的形式推理能力对于推进自动化软件工程至关重要。然而，现有针对LLM的基准缺乏基于计算和复杂度的系统评估，致使我们仍不了解其形式推理能力是否能把握由计算理论定义的形式语言的结构化、层次化复杂性。为此，我们引入ChomskyBench，一个通过奇克谱层次系统评估LLM的基准。不同于以往使用神经网络向量分类的方法，ChomskyBench是首次结合完整奇克谱层次覆盖、通过自然语言实现过程轨迹评估和确定性符号可验证性。ChomskyBench包含一套全面的语言识别与生成任务，旨在测试各层次的能力。大量实验表明，性能呈清晰的层次化分布，与谱层次的复杂性程度呈相关性。我们的分析揭示，任务难度显著影响推理长度和性能。进一步地，我们发现尽管更大的模型和先进的推理方法提供了显著的相对提升，但面临严重的效率障碍：实现实际可靠性需要昂贵的计算成本，揭示当前限制源于效率而非绝对能力上限。时间复杂性分析进一步表明，LLM在这些形式任务方面的效率显著低于传统算法程序。这些结果描绘了当前LLM的实际限制，凸显了传统软件工具的必不可少性，并为开发更强大的形式推理能力的未来LLM提供了指导。