Comment by marojejian | Hacker News Reader

Comment by marojejian | Hacker News Reader

Though this particular model doesn't sound generalizable, the neuro-symbolic approach seems very promising to me:

- linking the (increasingly powerful) "system 1" tools that are most of current ML with more structured "system 2" tools, like logical proof generation, which can plan and and check the veracity / value of output. - System 2 chugs along 'till it gets stuck, then system 1 jumps in to provide an intuitive guess on what part of state space to check next. - Here they leveraged the ability to generate proofs by computer to create a data set of 100m proofs, enabling scalable self-supervised learning. Seem to me the symbolic domains are well formed to allow such generation of data, which while low value in each instance, might allow valuable pre-training in aggregate.

Putting these elements together is an approach that could get us quite far.

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.

> 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

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

>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.

> 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?

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

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.

This I suspect is the closest chance to reaching some flavor of AGI

Reply on news.ycombinator.com