There are a fair amount of formal reasoning systems out there for various structured reasoning tasks. LLMs may not be able to reason, but they can specify thing

There are a fair amount of formal reasoning systems out there for various structured reasoning tasks. LLMs may not be able to reason, but they can specify things to be reasoned about in Gallina or OWL DT or whatever and defer. I think folks seem to think AGI will be a single model, while if you look at our primary example of human intelligence it’s many models interconnected. There’s no reason for, say, LLMs to have the ability to play chess or solve differential equations or recall facts or reason formally. These already have excellent solutions that you might as well use. It’s interesting to see how far they can go in these areas, but I’m not holding my breath for an LLM to be able to out math mathematica.