by zhiyang | 2025-04-12 05:31:03+00:00
Decision procedures, a subset of automated reasoning and consequently logical AI, are dominated by SAT and SMT solvers.

This is a comment/response to: https://news.ycombinator.com/item?id=38770869

Between the late 1990s (thanks to the development of the GRASP SAT solver by Prof. João Marques Silva at the University of Michigan) and the early 2010s, performance of SAT solvers improved by 7 orders of magnitude.

Reference: https://en.wikipedia.org/wiki/GRASP_(SAT_solver)

Arguably, Prof. Armin Biere published on the SAT museum about how SAT solvers have collectively kept improving till date.

The advent of using the NVIDIA CUDA platform for NVIDIA's GPU platform enabled GPGPU computing to be plausible/feasible shortly. This lead to what Dr. Sara Hooker calls the "hardware lottery" [Hooker2021].

Reference: [Hooker2021] Sara Hooker, "The Hardware Lottery," Communications of the ACM, Vol. 64, No. 12, December, 2021, ACM Media, New York, NY, pages 58-65. DOI: https://dx.doi.org/10.1145/3467017.

This swung the semiconductor and IT industries back towards domain-specific computing, preferably via domain-specific hardware/software co-design, since the performance speedup of general-purpose processor architectures and general-purpose compilers have slowed down to about 5% by the 2010s.

We ran out of low-hanging fruits and cannot easily address their associated challenges, such as: the impending doom of Moore's law; memory wall (even though the seminal paper is from the 1990s, it was addressed by the computer architecture textbook co-authors Prof./Dr. John L. Hennessy and Prof./Dr. David A. Patterson in the first edition in 1990); the end of Dennard scaling or the power wall; the instruction-level parallelism (ILP) wall - think Amdahl's law; dark silicon - limits the number of operating cores in a many-core processor; and (hardware) accelerator wall.

This lead to inadvertent success stories like AlexNet, which sparked a rapidly growing resurgent interest in statistical/probabilistic machine learning, especially with deep learning.

When people recognize that statistical/probabilistic machine learning is too primal, and needs to be complemented or augmented with logical reasoning, they address what people in that thread talked about.

However, they missed out on the huge boom in SAT solver performance, which lead to significant interest in modern SMT solvers. Their performance boom in the early 21st century lead to multiple applications, like VLSI/embedded model checking (improving performance by a lot). Unfortunately, crafting state-of-the-art SMT solvers by the late 2000s has become considerably challenging.

Naturally, when start-ups involving deep learning and deep learning hardware accelerators are taking off in terms of valuation and getting acquired for a lot of money, and professors and Ph.D. students are being poached by companies, not just corporate research labs, why work on something so much harder, like SMT solvers.

Thanks to the work of Prof. Vijay Ganesh (now at Georgia Tech) and others, there has been work on integrating SMT solver and related technology with deep learning, including verifying deep neural networks.

Then-Prof. Pedro Domingos had looked at "unifying logical and statistical AI".

So, this is not new, like symbolic-numeric approaches for machine learning. People usually hate learning material needed to understand SMT solvers or other decision procedures, the graph computing aspects of symbolic approaches, or the differential equations and linear algebra aspects of numerical approaches. Hence, it is hard to get people to synthesize them well. However, when we throw enough money at funding such research projects, and valuing start-ups based on their research deliverables, more Ph.D. students and graduates will work on this topic.