构建基于大语言模型的推理工具的当前做法是非正式的——我们可以做得更好

越来越多的人对通过将传统符号算法与大语言模型（LLM）结合来构建软件验证器、合成器等自动推理（AR）工具感到兴奋。不幸的是，当前构建此类神经符号 AR 系统的做法是一种非正式的编程模型，既没有传统符号算法的强有力保证，也没有神经网络与符号推理深度同步，以释放 LLM 推理的潜能。我提出神经符号迁移系统作为一种原则性计算模型，可支撑构建神经符号 AR 工具的基础设施。在此模型中，符号状态与直觉配对，状态转换并行地在符号和直觉上操作。我论证为何这种新范式能够在保持符号算法强有力保证的同时，扩展逻辑推理的规模，而我所提出的计算模型可在逻辑编程语言中实现。