It is well known that human reasoning, after evolving for at least several thousand years, has gradually transformed from natural language reasoning to formal reasoning. In modern science, a significant indicator of a discipline's maturity is whether its main theories can be formalized (or axiomatized, mathematized). At the inception of AI, research on reasoning was primarily based on formal reasoning, which surprisingly achieved remarkable success early on. For instance, programs developed by Newell, Simon and Shaw in 1956, as well as Wang in 1960, proved almost all theorems in "Principia Mathematica" by Whitehead and Russell. Nowadays, state-of-the-art symbolic SAT solvers have become so sophisticated that attempting to achieve SAT solving via machine learning approaches cannot compete with them (Daniel Selsam et al. ICLR 2019, Learning a SAT Solver from Single-Bit Supervision):
As we stressed early on, as an end-to-end SAT solver the trained NeuroSAT system discussed in this paper is still vastly less reliable than the state-of-the-art. We concede that we see no obvious path to beating existing SAT solvers.
Given this, I'm wondering why we overlook the achievements of traditional symbolic reasoning and invest so much effort into implementing natural language reasoning within large language models. What are the advantages of natural language reasoning over formal reasoning?