Hacker News Reader

Comment by jdmoreira | Hacker News Reader

Sounds like something really simple to define and grasp. What's wrong with, for example:

"A software that beats most humans on most cognitive tasks".

People make it harder than it needs to he IMO

We've had computers that beat humans in differential equations, automated theorems, arithmetic, aiming a gun and more in the 1970s.

Even search was considered an AI before Google, but today is just a thing computers are and always have been faster than humans at. Even before ChatGPT, lawyers relied upon computers to double-check citations.

Even in programming, I expect that compilers and IDEs check for the most common errors.

I could beat the differential equations AI at aiming a gun so badly

That's why it's Artificial *General* Intelligence.

We knew 30 years ago that computer can beat human in the field it was engineered for.

But AGI is good at anything you throw at it, including building a better AI. Now give it agency and that's a recipe for a disaster.

We still don't beat humans in e.g. LeanDojo, to my understanding. But we also haven't yet thrown the state of the art in graph attention technology at doing the core task of in-context learning (consider the entire explored (partial-)proof "tree" for deciding what tactic with which premises (if the tactic takes an AST/expression argument, like "use that definition/equivalence there as a rewrite rule on the current goal at this node in the proof tree") to apply next at which node in the (partial-)proof tree) in the interactive theorem proving situation, let alone with reinforcement learning that uses the attention structures to funnel back information on what things in dead branches had responsibility for the decisions that made the non-dead branches.

Because the RL agent should happily use the theorem prover as a "calculator", and only get "charged" for how much the ML inference and the actual cheap calculator execution really cost. Exploration in-context is what humans also do, and immensely powerful. Similar to, when programming, testing some expressions to figure out edge-cases before incorporating them into a large function/algorithm that has poor observability.

So far, machines still mostly do the task of "computing" in theorem proving for us, rather than show some proper intelligence. It's damming that LeanDojo got so high marks without reinforcement learning. They pretty much just dumped prover context state during a run through the entire matlib "standard" library and handed it to two transformers, one for embedding premises and one encoder-decoder fed with the current state and as many premises as the encoder context fits after the state, generating/sampling a few tactics to apply. No freedom of where in the proof tree to apply the next tactic, no awareness of any such side-branches.

The stronger version of this definition is "capable of meeting or beating human experts at all tasks".

If and when there exists software close to this capability, I think all reasonable people would agree that AGI has been accomplished.

Including the ability to construct a better version of said software.

Reply on news.ycombinator.com