[gizmo686]

> The key milestone will be moving away from the need to use specific formal / symbolic domains, and to generate a pretrained system that can generalize the skills learned from those domains.

You do not need to solve everything at once. This approach has the potential to revolution both math and programming by moving formal verification from being a niche tool into a regular part of every practitioners toolbox.

It also completely solves (within the domain it applies) one of the most fundamental problems of AI that the current round is calling "hallucinations"; however that solution only works because we have a non AI system to prove correctness.

At a high level, this approach is not really that new. Biochem has been using AI to help find candidate molecules, which are then verified by physical experimentation.

Combinatorical game AI has been using the AI as an input to old fasion monte carlo searches

[initplus]

>however that solution only works because we have a non AI system to prove correctness

But this is actually a really common scenario. Checking a solution for correctness is often much easier than actually finding a correct solution in the first place.

[empath-nirvana]

> however that solution only works because we have a non AI system to prove correctness.

I'm not sure why you are calling it non-AI. There's no reason why some AI system has to be some single neural network like GPT and not a hacked together conglomeration of a bunch of neural networks and symbolic logic systems. Like is it cheating to use a SAT solver? Is a SAT solver itself not artificial intelligence of a kind?

[cubefox]

In modern terminology, AI = machine learning model. The hand coded GOFAI from the past is just called software.

[lucubratory]

No, you can't just declare a word redefined when it is still in common usage in its correct meaning, which includes both GOFAI and deep learning/neural network approaches. AI is effect defined, not architecture defined.

[jvanderbot]

Moreover, it's not so recently that people began training networks to help make guesses for branch and bound type solvers.