A first step towards artificial general intelligence, and where it likely will take us instead

(Written as I am on the train to Bonn to take part in the "Prospects of Formal Mathematics" conference at the Hausdorff Institute for Mathematics )

Artificial General Intelligence is vaguely defined as the artificial intelligence milestone where the machines are better than most/all humans at most/all cognitive tasks. Inherent to considering this is the notion of singularity: if we get better at enough tasks, we should get better at getting better and we should eventually manage to launch runaway dynamics of increased intelligence. Some of those dynamics are expected by some to end up automating many jobs, which contributes to launching secondary speculative runaway dynamics of AI investments, quite likely unsustainable.

Theorem proving task

In this post I would like to consider a very specific task instead of AGI, the task of "proving a mathematical result", and to think about the dynamics it could launch. This task is highly relevant to an AGI discussion, for three complementary reasons, best considered in sequence:

• only a tiny percentage of the population is actually capable of performing this task;
• learning this task is recognized in many cognitive disciplines as broadly relevant to learning that discipline, in the sense that a first year mathematics course in engineering, biology, computer science, etc will often include "learning to prove" as part of the curriculum, as a proxy for the many reasonings this trainee will have to perform during their knowledge worker future;
• only an even smaller percentage of the population has a business model around theorem-proving (mostly mathematicians).

It turns out that AI is starting to have real success on the task of theorem proving:

• recently DeepMind released AlphaMath, capable of getting a Silver Medal in the International Mathematics Olympiad, a competition for high schoolers.
• many in the Lean community are building theorem formalizing and proving tools, sometimes used by Fields medalists to automate parts of their job (these mathematicians are even considering that their job is evolving in ways inconceivable 5 years ago!).

AI-for-math

This AI-for-math approach is making very quick progress, and we seem to be fast approaching a Kasparov-DeepBlue moment where machines surpass humans at theorem proving. The technical, knowledge and community seeds seem to be in place already for a humanity-wide level up on what humanity appreciates as cognitive in the math domain (akin to what happened with calculators). Also, unlike other fields, AI-for-math has the huge advantage that a proof is correct or false, and that this is easily verifiable by a computer. It's not subjective, which allows us to generate many proof attempts to then verify which attempts work. The challenge is instead in wisely generating proof attempt moves ("tactics" in Lean) in a search space that is very large (this is similar to the difficulty of building AlphaGo for Go when DeepBlue for chess had already "solved" chess for a while). So when we think we have made progress in proving a theorem, we can actually be sure to have done so. Generating proofs is not like generating artwork. Let's call this property of theorem proving Property V, for Verification.

This vision of runaway tooling helping mathematicians has been recently named "QED singularity" at another recent Bonn workshop in the same semester program: the runaway effect of improving our formal tools for formal theorem proving. Because our logical tools get automated we get better at producing logical tools to help automate ourselves.

Math-for-AI

This is great (and my motivation for attending the next workshop) but only half of the loop. Dual to AI-for-math there is also math-for-AI... What about all those knowledge workers that had to suffer through first year math proofs, never to use any of that skill ever again? If that skill was deemed relevant back then, could it still be relevant if performed by an artificial intelligence "intern"? I think so, but the discipline considered might not have Property V. There is a gap between formalizing the world and the actual world, usually called the "human element".

In other words, to give concrete examples, what about the following disciplines:

• math-for-AI-for-engineering, assisting humans in verifying that plans match formal specifications? Property V is there, but only after the building has collapsed. There is a surprising amount of subjectivity before that, for instance in understanding fully the ground underneath a building or the way a building will be used.
• math-for-AI-for-lawyers, assisting humans in building legal reasonings based on jurisprudence... law is not math, as many lawyers will proudly claim.
• math-for-AI-for-health, assisting humans/doctors in mapping all kinds of measurements about a body to the state of functional networks inside, and the impact of medication on those networks.

In my and hestia.ai 's viewpoint, the difference between AI-for-X and math-for-AI-for-X is specifically in the relaxation that needs to be applied to discipline X when you don't have Property V. It suggests a completely different way of reading a corpus from discipline X in order to leverage scarce relevant data, and knowing where to add "human element" feedback loops to encourage users to improve the system and its outputs.

We are currently working on such examples with various clients... stay tuned for showcases.

Our AGI future (?)

So... does this mean that hestia.ai is building AGI tools?

Well the systems we build will be better than any human at tasks currently performed by humans, but in ways that are not fundamentally different to the fact that:

• Casio calculators have replaced human calculators;
• most humans understand the task a calculator is supposed to perform for them;
• a small percentage of humans know how a calculator actually works;
• it's just a matter of putting the effort to understand how a calculator works (i.e. no black box needed).

Many competitors are building such systems as well, sometimes shamelessly proclaiming they are building AGI (but often without that last bullet point about the black box... instead in their narrative what they are building is magic to them and you should also accept that).

At the same time, a company that employs human calculators would go bankrupt fast. Hence we should expect to have gradual evolution of the economic landscape but also gradual reskilling of the workforce around the tools that are built. For the AGI standard of replacing most humans at most tasks, the humans are reskilling and the tasks are evolving: both baselines are changing in ways that make the AGI definition unattainable. On the other hand this humanity wide adaptation capacity is likely to outpace the capacity of VC funders to sustain the narrative that AI is magic and should remain a black box (worth considering: how many of your AI partners are sustainable financially? How many are making the effort to explain to you how they build it if you ask? hestia.ai is bootstrapped and always happy to explain to clients how AI systems work...).

Conclusion

AI is an evolution, not a revolution, at least for those at least willing to move now. Others might realize too late the baseline of productivity in their industry has risen fast. This future will be explored fastest in industrial applications of the tooling built to assist mathematicians.