> I suspect that the next big AI breakthrough will result at least in part from constraining LLM decisions with old AI approaches.

AFAIK bridging deductive and inductive AI has been understood as the trick for "AGI" for a long time, probably even before it was called AGI.

I really want this winter of deductive AI to be short. We need both sides and can't afford a long winter like the one inductive AI suffered.

FWIW when I first studied automatic theorem proving as a (high school) student in 2013, this was already widely discussed. They were trying to add neural networks inside the solvers, rather than current paradigm of a neural networks using theorem provers as tools. Presumably the history of logic + natural language computers would go back a lot further.