## 正式推理与大型语言模型：摘要 这次Hacker News讨论的核心是“形式语言”——机器可以精确解释的语言。最初，形式语言被定义为自然语言的模型，但到了1930年代末，对其“形式”的理解转变为“机械化”，这与可计算性理论的兴起相吻合。即使是不可判定的语言也被认为是形式语言，定义为符号序列的集合。 对话探讨了将其应用于现代大型语言模型。虽然大型语言模型在编码方面表现出色，但在逻辑方面却存在困难。一种提出的解决方案是使用大型语言模型将自然语言翻译成形式语言，然后利用逻辑引擎进行可验证的转换，最后再翻译回来。然而，挑战依然存在：目前大型语言模型在形式化方面的表现不如人类，而初始和最终的翻译步骤容易出错。 像使用Prolog作为中间步骤等替代方案正在获得关注，还有将大型语言模型生成的代码与严格的验证方法（如静态分析）相结合的方法。推荐Math Academy和Art of Problem Solving等资源，以建立数学和逻辑的基础知识。最终目标是弥合大型语言模型的编码能力与强大、可验证的推理之间的差距。