“从70年的人工智能研究中可以得出的最重要教训是，”ACM A.M. 图灵奖得主理查德·S·萨顿在2019年一篇广为流传的文章《苦涩的教训》中写道，“那些利用计算能力的通用方法最终是最有效的，而且效果远远超过其他方法。”
萨顿认为：“研究人员试图利用他们对领域内的认知，但从长远来看，唯一重要的是利用计算能力。”他举例提到了计算机象棋和围棋、语音识别以及机器视觉。最近，随着GPU技术的发展，大规模语言模型（LLM）革命得以推进，GPU从一种小众的3D游戏加速器转变为人工智能的基础引擎。
然而，“利用计算能力的通用方法”的巨大成功掩盖了特定领域技术在自动化推理中的重大成就。那么，自动化推理究竟是什么呢？让我们回顾一下心理学家丹尼尔·卡尼曼在其著作《思考，快与慢》中提出的“系统1”和“系统2”概念。“系统1”反应迅速、自动化程度高，依靠直觉；而“系统2”则较为缓慢、需要经过深思熟虑，并运用分析能力（例如解决复杂数学问题）。机器学习主要依赖于“系统1”思维模式。但要实现“系统2”思维的机械化，我们必须首先实现推理的机械化。乔治·布尔在他的1847年著作《逻辑的数学分析》引言中写道：“本书的目的在于研究人类进行推理的基本原理，用微积分的符号语言表达这些原理，并在此基础上建立逻辑科学并发展其方法。”
布尔推理的机械化研究始于19世纪。德国代数学家恩斯特·施罗德在1895年写道：“理解任何前提的推论结果，或者至少找到获取这些结果的最快方法，我认为这是数学和逻辑学最崇高的目标之一。”20世纪50年代计算机普及后，逻辑学者们便开始了这项研究。
但布尔推理被证明是一个极具挑战性的问题。1971年，斯蒂芬·库克将布尔可满足性问题（SAT）确定为NP完全问题。是否存在多项式时间算法来求解这个问题是数学逻辑和理论计算机科学领域最重大的未解决问题之一。然而自20世纪50年代以来，逻辑学家和计算机科学家们却采取了萨顿所反对的方法，即“依赖他们对领域的认知”。每年都会举办SAT求解竞赛。
2001年，普林斯顿大学的沙拉德·马利克和他的学生们证明了数据结构和搜索启发式算法在CDCL求解中的关键作用，这些机制大幅减少了搜索空间，显著提升了求解速度。那时，SAT求解器的性能已经足够成熟，可以在工业领域得到应用。此外，马利克的“算法工程”方法成为了SAT求解领域的通用方法。加州大学伯克利分校的桑吉特·塞西亚指出，在21世纪的头十年里，即使使用相同的硬件，SAT求解器的性能也提升了近三个数量级。
生物通微信公众号
生物通新浪微博
