当规范完成错误时：形式化和测量 大语言模型 中的跳跃

大语言模型（LLM）是否可以执行从证据到新公理系统的溯因跳跃（通常称为跳跃），最近引起了相当多的争论。一个突出的观点认为，LLM 在结构上无法实现这种跳跃，而最近的研究对其机制和经验证据提出了质疑。争论仍然存在的主要原因之一是难以精确地定义跳跃以对其进行测试。在本文中，我们尝试通过四个步骤对跳跃进行正式描述，并测量第二步。这些步骤询问部分数据的默认完成是什么，当约束排除它时，新结构是否与后来的观察一致，以及连续跳跃如何复合。我们将 \emph{jump instance} 定义为有限扩展问题，其约束排除了 Kan 扩展给出的规范完成，并留下一个正确的完成以进行重命名。在此设置中，具有规范默认值的模型通过在约束下生成正确的完成来执行第二步。我们评估了三个认证系列的十四种型号。在所有运行中，规范完成在 $13{,}300$ 约束答案中返回一次。几个校准模型也能可靠地给出正确的完成结果，包括三个 API 模型，它们解决了 162 美元主链试验中的 159 美元问题，表明它们可以跳到这一步。我们进一步将第三步和第四步正式化，其实证评估仍有待未来的工作。我们希望我们的工作能够为未来的全面跳跃的形式化和衡量铺平道路。论文代码可在https://github.com/EEthanShi/kan-jump-test获取。