A difficult part was constructing a chess board on which to play math (Lean). Now it's just pattern recognition and computation.
LLMs are just the beginning, we'll see more specialized math AI resembling StockFish soon.
However, this was not verified in Lean. This was purely plain language in and out. I think, in many ways, this is a quite exciting demonstration of exactly the opposite of the point you're making. Verification comes in when you want to offload checking proofs to computers as well. As it stands, this proof was hand-verified by a group of mathematicians in the field.
This is the caliber of thinking in unimpaired AI bullishness.
Dystopia vibes from the fictional "Manna" management system [0] used at a hamburger franchise, which involved a lot of "reverse centaur" automation.
> At any given moment Manna had a list of things that it needed to do. There were orders coming in from the cash registers, so Manna directed employees to prepare those meals. There were also toilets to be scrubbed on a regular basis, floors to mop, tables to wipe, sidewalks to sweep, buns to defrost, inventory to rotate, windows to wash and so on. Manna kept track of the hundreds of tasks that needed to get done, and assigned each task to an employee one at a time. [...]
> At the end of the shift Manna always said the same thing. “You are done for today. Thank you for your help.” Then you took off your headset and put it back on the rack to recharge. The first few minutes off the headset were always disorienting — there had been this voice in your head telling you exactly what to do in minute detail for six or eight hours. You had to turn your brain back on to get out of the restaurant.
And I'll also link to the HN thread following his death a couple of years ago - https://news.ycombinator.com/item?id=42228759
I have had them run out of receipts, but it’s never mattered for me. If I’m dining in, the plastic number you carry to your table makes sure I get my food. And if I’m taking it to-go, they always find me anyways.
I'm not sure how that could be. I can walk up to the counter and say "Big Mac Large Fry Small Coke" faster than you can navigate the first screen of the kiosk, and a skilled counter worker can key that in and be done before I even get my credit card out.
Everybody would go through this workflow built for customization, and at McD they do not. This to me means they are not building for this usecase.
In what culture is it normal to just state your order without greeting or saying “please”? You also didn’t include the time taken squinting at the menu and trying to figure out what you can even order.
Other places optimize for this better by not having too many hand-overs between order and preparation.
If it's purely about the food, receiving it, consuming it, then sure, get the human out of the loop, interact with a machine. Ideally even the preparation is done by a machine. No human error or hair involved. Why even go there, let it be delivered to your home.
But these places are also about the experience of social connection. The bar keeper, the waiter, the chef. They are all involved in this experience and the actual food is "just" one component, one detail, albeit an important one. My favorite restaurants would be nothing without the people there.
It's similar with music. It's not just about the produced sound waves. The musician forms a social bond with the audience. Even when listening to a recording, my mind is re-living or at least imagining a live sitting, that connection with the musician. No machine generated music will ever be able to replace that.
Depends on what you're ordering and who the cashier is.
If your order is the happy path of no customizations of a combo with an experienced cashier, it can be done in seconds, for sure. "Medium #4 with a Diet Coke", pay, done.
But if you customize your burger or ordering a lot of items a la carte and you're dealing with a new cashier that has weak English skills, good fucking luck. You'll likely need to wait for them to figure out they need to call someone over to help, have to repeat your order, and you end up spending far more time.
> it keeps trying to upsell you
Yeah, I'll agree that's obnoxious, especially when it's trying to upsell you something that's already on your order. I ordered a combo. I don't need you to add another fry.
It seems designed to maximize how many screens they show you to make an order. Each one with a slight delay and animation.
At a drive through I can say “gimme a number one, medium, with a Coke Zero” and they give me my total. That’s the convenience the kiosk is up against.
At the kiosk there’s:
- A welcome screen you have to tap
- A “carry out or dine in” screen
- Always one other screen with a dumb question about apps or whatever, tap through
- A top level menu with a bunch of categories, burgers, drinks, sides, desserts, etc… I guess I want burgers? But it’s a combo, hmm. I guess I’ll figure out how to make it a meal. Tap burgers.
- Then another screen with burgers, in a different order than the drive through numbering, tap Big Mac
- Then another dedicated screen to shows you a picture of a Big Mac, with a bunch of customization options, which you have to scroll past and verify that it matches the defaults you expect, and at the bottom you can tap add
- Then another screen asking you if you want to make it a meal
- Then another screen asking the size
- Then another screen asking what to drink
- Then another screen that shows you the drink
- Then another screen for what size
Etc etc etc. Each of these screens takes a few seconds to display too, just slow enough to be infuriating.
In my mind the ideal kiosk is something where you get “the menu” (like what you see on the billboard in the drive through) with the usual big squares with a number on them and a picture of the meal. Tapping one puts it in a “drawer” section with my order in it, and each item in the drawer can have simple in-line edit controls for “size” and “what to drink”, with them showing up empty in a way that makes it obvious I need to fill in those answers before I can check out.
I should be able to tap one button for the combo number I want, another for the size, another for the drink, then checkout, all on one screen without long delays. If I don’t want a combo but want individual items, I can just scroll down a bit to look at the full menu. The order drawer stays where it is.
Or hell, just let me say “number one with a Coke” and have a very simple ASR and NL parser figure it out and put it in my pending order to edit.
Customizations can be behind a simple “customize” button on each item in my pending order. If I don’t have customizations I can just ignore it. What you get with no customizations is what you’d get if you just order it verbally to a human without specifying anything. The concept of “here’s how we typically make it, if you want anything different let us know” is a very deeply ingrained and familiar concept to restaurant patrons, and being forced to answer every little question even if you don’t care, adds up to a lot of frustration.
Fast food places came up with the combo numbering system to make ordering faster, and it was super convenient and fast, because there’s a financial incentive to get you through the drive through because you’re blocking other customers. But since they have several kiosks available, they seem to not care at all about the efficiency of the user interface, because it’s not a problem for them. But it’s still a problem for me, because I still want to order quickly, despite it not blocking other customers. It’s a huge step down from just saying “number one with a Coke”.
Most repeat customers use the app, which sports the digital equivalent of a loyalty program, and various coupons. And lets you save your 'usual' order with customizations etc. Plus the annoying push notifications for FreeFrydays or whatever. And upsells, new product launches, etc.
My recollection is that the kiosk is just a weak facsimile of the app. And wasn't terrible, but everyone's standards vary.
Which is why I will never reinstall their damned app.
Is there something wrong with their food in the USA?
There's much more to being human than our "cognitive abilities"
Not obvious and in fact I think the opposite is way more likely. Chess is well-defined and self-contained in a way that managing a restaurant with fleshy customers never will be.
Also, there will be hundreds of disparate tasks that are happening in parallel, and even humans still make up frameworks to discover most urgent/important work that needs to be done first.
Stockfish's neural net evaluation model was trained on millions of its positions with its own original algorithmic evaluation function (entirely developed by humans) and search tree. The result was a much smaller model than Leela's that requires little computation (not even a GPU), paired with its already extremely efficient search/pruning algorithms that made it stronger than Leela in competitive play. Leela's evaluation function is much stronger (at one ply it has an ELO of around 2300, Stockfish is probably closer to 1800), but it requires vastly more resources and those are always bounded in a match.
Humans haven't learned as much new information about chess from Stockfish as we have from Leela.
Nitpick: it’s Elo, not ELO. The name comes from the inventor’s surname and is not an acronym.
All AI proofs so far, including this one, are using existing tools in new ways, rather than inventing new tools. This is not surprising if you know how these models are trained. These existing tools are in distribution. New tools are not.
Problems worth of a Fields Medal likely require new tools to be invented. Thus it is not clear whether progress within the confines of the current paradigm is enough.
We could get this weird spiky situation where the AI is insanely superhuman at all problem solving, but completely incapable of coming up with a single new tool. It discovers everything there is to discover, subject to existing axioms and concepts.
Timothy Gowers gives some commentary on this in the attached PDF.
We have that chess board for quite a while now, over 40 years. And no, there is nothing special about Lean here, it is just herd mentality. Also, we don't know how much training with Lean helped this particular model.
https://en.wikipedia.org/wiki/Qualified_immunity
Assuming you can still sue McDonalds I am not sure if this is a problem in the robotic llm case. I'm also trying to imagine a case where you would want to sue the llm and not the company. Given robots/llm don't have free will I'm not sure the problem with qualified immunity making police unaccountable applies.
There already exist a lot of similar conventions in corporate law. Generally, a main advantage of incorporation is protecting the people making the decisions from personal lawsuits.
That only requires someone own the ai managed McDonald's though. so long as they can't avoid responsibility by pointing to the AI I don't see why you couldn't sue them.
Police are a monopoly; nobody has a choice about which police company to use. McDonalds are not a monopoly, and many customers would prefer to eat at competitors run by entities that could be sued or jailed if they did anything particularly egregious.
The same intuition applies if you walk into McDonald's and a person there mistreats you. You want that person held responsible.
But the LLM is not a person. What is there to even sue? It just seems like it would simply pass through to the corporate entity without the same tension of feeling like we let a human get away with something. Because there is no human, just a corporation and the robot servicing the place.
Put another way - if the LLM is not a person, what is the advantage of a personal lawsuit?
Just sue the McDonalds. Even in a case where the LLM is extremely misaligned and acts in a way where you might normally personally sue the McDonald's employee, I'm just not sure the human intuition about "holding someone accountable" would have its normal force because again - the LLM is not a person.
So given we already have the notions of incorporation and indemnification it doesn't make sense to say what is precluding LLMs from running McDonald's is they can't be sued. If McDonald's can still be sued, then not only is there no problem, there is very likely not even a change in the status quo.
The purpose of qualified immunity is for when an officer does something that turns out to be illegal but they were both told to by their superiors and did not think it was in violation at the time.
An officer making a choice to violate your rights would not be eligible for qualified immunity.
Excellent standards for people authorized by the state to run around with a badge and a gun in a free society. Your comment history on this is so unimpressive. Would you countenance the same excuses in anyone else? A man puts on his police uniform and suddenly you think he should be immune from civil prosecution because "my boss told me so" and "I didn't know"?
I wonder if you will make similar excuses for robo cop. Or if your principles merely extend to whatever human you can find in uniform willing to tolerate your friendship.
Plus, qualified immunity is only for civil precedings. Individual officers are still liable for any criminal actions they take. I see a lot of people say that some officer should be in jail and blame qualified immunity when those two things are not related at all.
I'm not arguing, at all, that police should be immune to prosecution individually. I'm trying to make the point that, if you are trying to hold police individually accountable for their _criminal_ actions, qualified immunity isn't the thing that's preventing that. There's a whole legal system and union/police culture that's responsible for that.
Qualified immunity is thrown around so much in contexts where it makes it clear that people don't understand what it means and gets used, as it was in your comment, as a bogey man that's to blame for all the times police get let off the hook for their misbehavior. All I'm trying to do when correcting you (and others) about qualified immunity is to both redirect your anger and effort into changing something that will actually make a difference and/or prevent you from spending the mental or physical energy chasing a dead end.
You seem to be arguing with yourself, not with me. If you are satisfied with a cop only facing criminal liability (often from the same prosecutors that rely on police to make other cases, among other issues as you pointed out) fine that is your prerogative. Don't file a civil case. But don't misrepresent my position. Criminal prosecution does not preclude civil, nor the other way around. Citizens should not face such hurdles to file civil suits, irrespective of whatever happens re a criminal case. Why is that so hard for you to understand? Surely your comprehend that one can be found liable both criminally and civilly in many cases. Or tried for both but subject to different penalties (including none) depending on how each goes. Why are your LEO buddies so special as to be largely exempt from the rules that govern the rest of us?
The fact your comment history is riddled with these continued misrepresentations on this topic while you claim to educate is simply galling. Have a good day, I don't think I can continue in good faith with someone who seems to predicate engagement on this topic with unfounded assumptions about others education on the issue. Your own comments on this topic indeed are indicative of a severe projection in this respect.
and LLM's are getting better at providing less of it
perhaps in the future the GPU-poor can go to McDonalds and get AI to solve their riddles by ordering an extra napkin with the solution written on.
https://www.anthropic.com/research/project-vend-1 https://www.wsj.com/tech/ai/anthropic-claude-ai-vending-mach...
(Two different examples of a similar idea)
Heuristically weighted directed graphs? Wow amazing I'm sure nobody has done that before.
Math is a sequence of formal rules applied to construct a proof tree. Therefore an AI trained on these rules could be far more efficient, and search far deeper into proof space
This future still sucks. The tech industry is making the world a worse place.
Two years old now, and as the cryptographers say, attacks only get better.
Or is your argument that AI is permanently doomed to not work?
What happened to art since?
We got artistic photography on top of paintings as well. It did not become widespread right away as people were mostly enamored by the simplicity of getting a realistic image first. But after that died away, people made art out of photography too.
Yes, those who did landscapes or portraits for hire were affected financially, but we ended up with more art, not less.
If I need to spell it out: genAI for image generation will also become an avenue for real artistic expression, as some pioneers are demonstrating, even if image generation is democratized, there will be a difference between art and non-art. It will also not kill conventional art either.
A tool is let to make a set of choices, but there is some control: you can prompt an AI to draw a white animal, a white bird or white swan — if you get a white horse with wings and a beak on any of the latter ones, we could say that AI is putting more thought, but at the moment, it wouldn't and we'd call it broken.
This is an insane take. Once again, does hiring someone on fiverr to draw for me make me an artist?