Reason derives its strength in having a few primitives and creating new assertions through the transformation of symbols by following precise rules (which is how algorithms work).
In ML-based AIs, everything is imprecise and probabilistic, and this kind of generation gets its strength from building recognizable from utterly imprecise inputs and training - quite the opposite of how logic and reason evolve. Now, "classic" AI was a powerful way to derive new knowledge, and automatic theorem proving is a strong discipline; but the recent breakthroughs in AI are not directly applicable to classic techniques.
Do you know what machine-learning AIs could be good for? Generating "insight" in problem solvers for guiding the theorem demonstrations through the proof search space, trying to find the best sub-spaces to explore. If there's a way to create human-like general AI, it will likely combine both kinds of generation - the rational methods of symbolic logic and the "irrational" statistical methods of ML.
Work in progress for sure, though.
How so?
I'm no mathematician, but I don't see how these problem types are equivalent. Could you elaborate?
For a type theory we might want to reason about, there’s a diagram (in category theory) which represents the same semantic content. These diagrams turn out to have recurring and common structures.
You can represent those diagrams as adjacency matrices, where those structures have a particular “shape” in the entries. Which if you squint hard looks like an image completion problem, ie, finding missing part of the matrix which represents a proof.
I hadn't heard about it before, although I have some notions of both category theory and theorem proving.
And is your description of “complete and label the diagram” using image generation a thing that actually exists or something that has potential to be created? That could be a breakthrough in applying formal methods to real-world problems.
> And is your description of “complete and label the diagram” using image generation a thing that actually exists or something that has potential to be created?
Somewhere between — it’s a topic being researched, but results are very early (basically, just shapes and groups).
When you are in its bounds it seems magical, once you go outside it seems like a weak joke.
And many of the reasons it is bad outside its sweet spot are fundamental to how it works not a flaw that can be iterated away.
Can you elaborate?
It has a strong sense of what 1 object is. Ask it for a photo of a kitten and you get an jaw droppingly realistic photo of a kitten.
Ask it for a picture of 6 kittens and you get, well, whatever this is: https://labs.openai.com/s/PIZJe6GCfat9soN3WOV3eC9p
7 kittens, none well defined. Because the loss function it is optimising taps out once it has got "close" and close for a multiple object prompt is _a lot_ further away than for a single subject prompt (here is the 1 kitten version https://labs.openai.com/s/1aCOUxNT19kbMZZtEBG7CoFY - this is basically witchcraft it is so good, the group shot is a joke).
I suppose you could massively reduce the loss amount you are willing to accept but that doesn't guarantee dalle with optimise the correct part of the pictures - maybe I'd have just ended up with really, really good floors.
The other thing Dalle is bad at is backgrounds, and once again this is due to "optimising an error score". https://labs.openai.com/s/U1Vo2fxThuXmQZzIwLQ4g9Ai nothing about this is right. At a superficial glance it looks like the view over a city but it's a random splatching of building cutouts and when you look at the detail of the builds they are a blur of pixels that kind of approximate doors and windows but are nothing of the sort. They are super fuzzy and dream like. Because it's trying to generate an image that looks like a cityscape from its memory of Glasgow cityscapes. THere's no coherance because it's trying to covert random pixels into a cityscape not for buildings out of components that humans know go to makeup buildings.
Recall that it's stored a compressed version of TBs of images.
Now, your examples simply show some slight artifacts and lack of details on specific things. You're presenting remaining shortcomings on these metrics as "fundamental to how it works not a flaw that can be iterated away", when in fact they have mostly been iterated away over the past few years.
A larger corpus allows it to be more varied but it doesn't fix the fundamental limitations.
I'm hoping it's not as bad as Dall-E and Stable Diffusion - I've tried to use those to generate some generic product looking stock photos for a demo and it's spectacularly bad. The only context I see it get praised is fantasy style art - and that is visually appealing nonsense by definition.
If the code generated by copilot has the same "looks convincing but is fundamentally flawed" quality then it sounds like an insidious bug generator.
If you think of AI as a dial from sample(data) to mean(data), then as the dial is turned towards the mean() you get more "generic" results, but also more garbled ones.
Copilot is more like a search engine, having turned the dial more towards sample().
The real invention of the NN is simply to provide that dial in a trainable way.
The only change to the "state of the art" is the size of the weights, and how long they take to train. This "advancement" is no more impressive than google indexing more webpages.
There has been no step-change advancement in AI in, perhaps, 50 years. All we see today is a product of hardware, in GPU/CPUs able to compress TBs of data into c. 300GB of weights. And likewise, the internet to provide it and SSDs to hold it.
The "magic" of AI is no more the magic of wikipida, here: copilot is good only because million+ programmers made github good.
It's still little more than a fancy search.
> It's still little more than a fancy search.
I feel like the goalposts have been moved between your two comments. CoPilot is obviously not producing garbled nonsense, and it's also not just printing the top result from StackOverflow. It is producing code that references my variables, does the right thing 50% of the time, and usually compiles.
One of the nice little things is error messages- when I type `if (!foo) { throw ... ` CoPilot is able to complete a nicely formatted and descriptive error message from its understanding of my code. It's not garbled nonsense, and it's not just a search engine.
Does AI deserve the hype it sometimes gets? Not yet. But I think you're going to have to start digging a little deeper for your commentary.
Imagine if we were all self-replicating computers, and certain members of this silicon race began experimenting with making creatures with carbon macro-molecules to create organic intelligence, you could make the same claim in the other direction:
"There has been no step-change advancement in Organic Intelligence in, perhaps, 50 years. All we see today is a product of cell count, in neurotransmitter chemistry able to compress TBs of experiences into c. 300B neurons."
But I agree with you that everything they do seems intelligent because 'intelligence' was in the training data. Not much different from us, if you raise a human removed from society (take his intelligent training data away) he will not accomplish almost anything on his own.
People thought it might take centuries for a computer to defeat a top human in Go. Then deep learning showed up and a few years later it's the opposite.
A lot of the things deep learning methods are doing now are things no one had any idea how long research would take to achieve, or if they were even possible.
Personally, I think we are currently hitting some walls that might take a while to climb before we get to AGI, but I am very impressed at the recent progress.