5 ms·
Have you ever used Github CoPilot? It does a lot of useful work, automating away rote typing in programming. Have you tried Dall-E or Stable Diffusion? They mak
by woah 4y ago
Have you ever used Github CoPilot? It does a lot of useful work, automating away rote typing in programming. Have you tried Dall-E or Stable Diffusion? They make good looking images. This comment seems completely unmoored from where the state of the art is right now.
- TuringTest 4y agoMath follows a completely different approach with respect to how machine-learning AIs do their thing. 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.
- zmgsabst 4y agoAutomated theorem proving is the same problem as “complete and label the diagram”, which image generation is okay at. Work in progress for sure, though.
- NateEag 4y ago> Automated theorem proving is the same problem as “complete and label the diagram”, which image generation is okay at. How so? I'm no mathematician, but I don't see how these problem types are equivalent. Could you elaborate?
- zmgsabst 4y agoSure — the connecting topic is topos theory. 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.
- TuringTest 4y agoWho's using that topos theory, and is it well known in automated theorem proving? 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.
- zmgsabst 4y agoTopos theory is used by people researching foundations, eg Michael Shulman. > 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).
- mjburgess 4y agosure, but co-pilot is mostly just copying code (see, for example, the issue with it producing quake source code). 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.
- woah 4y ago> It's all just passable garbled nonesense that the reader (goes to lengths) to interept based on their prior knowledge, which is not expressed in the syntax of what these systems output. > 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.
- _justinfunk 4y agoAs someone who uses co-pilot daily - it often does print garbled nonsense (semantic nonsense, not syntactic nonsense - if you get my meaning).
- planetsprite 4y ago
- Marazan 4y agoDall-E produces good looking images within certain parameters. 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.
- stevenhuang 4y ago> fundamental to how it works not a flaw that can be iterated away. Can you elaborate?
- Marazan 4y agoDalle is trying to optimise a bunch of random pixels to meet the prompt. 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 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 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 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.
- civilized 4y agoI agree. It's possible to point out the clear limitations of current AI without being oblivious to the huge, indisputable advances that have occurred. 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.
- moonchrome 4y agoI haven't used copilot because I'm not sure I'm allowed, but I'll try it on a personal project eventually. 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.