6 ms·
As I have stated before, AI will win a fields medal before it can manage a McDonald's A difficult part was constructing a chess board on which to play math (Le
by vatsachak 5mo ago
As I have stated before, AI will win a fields medal before it can manage a McDonald's
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.
- soupspaces 5mo agoLee Sedol, Move 37 https://www.reddit.com/r/singularity/comments/1l0z5yk/the_moment_everything_changed_humans_reacting_to/ https://www.reddit.com/r/singularity/comments/1l0z5yk/the_mo... Edit: I wasn't necessarily disagreeing. But on second thought the chessboard in this math analogy is being built, not just played in. This Hardy quote comes to mind https://www.goodreads.com/quotes/902543-it-proof-by-contradiction-is-a-far-finer-gambit-than https://www.goodreads.com/quotes/902543-it-proof-by-contradi...
- vatsachak 5mo agoMy claim is that we haven't even witnessed the move 37 of math yet. I am claiming that math AI is going to get even better
- Lerc 5mo agoI disagree. It will be able to perform work deserving if a fields medal before it is capable of running a McDonalds. I think it will be running a McDonalds well before either of those things happen, and a fields medal long after both have happened.
- edbaskerville 5mo agoI just visited a McDonald's for the first time in a while. The self-order kiosk UI is quite bad. I think this is evidence in favor of the idea that an incompetent AI will soon be incompetently running a McDonald's.
- deleted 5mo ago[deleted]
- Silamoth 5mo agoOut of curiosity, what issue did you have with the McDonald’s self-order kiosk? I actually think McDonald’s has the best kiosk I’ve ever encountered. The little animation that plays when you add an item to your cart is a little annoying (but I think they’ve sped that up). But otherwise, it’s everything I’d want. It shows you all the items, tells you every ingredient, and lets you add or remove ingredients. I have a better experience ordering through the kiosk than I do talking to a cashier.
- ndiddy 5mo agoIt takes longer than ordering with a cashier, it keeps trying to upsell you, and it's always out of receipt paper because unsurprisingly the company that isn't willing to pay a person to take orders is also not willing to pay a person to maintain the kiosks.
- Silamoth 5mo agoHmm. I’ve never really had those issues. It’s also much faster and easier than ordering with a human. I guess it does try to upsell you, but humans often do, too. And to me, it’s worth it to just click “No” in exchange for the added convenience (mostly in getting my order right). 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.
- ryandrake 5mo ago> It’s also much faster and easier than ordering with a human. 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.
- c7b 5mo agoOne could hardly ask for a task better suited for LLMs than producing math in Lean. Running a restaurant is so much fuzzier, from the definition of what it even means to the relation of inputs to outputs and evaluating success.
- moron4hire 5mo agoI think Lerc is saying that LLMs will be pressed into service managing McDonald's restaurants long before they are actually capable of managing said restaurants successfully.
- vatsachak 5mo agoNot necessarily. Obviously playing Kasparov on the board requires more planning ability than managing a McDonald's but look at where chess bots are now. There's much more to being human than our "cognitive abilities"
- baq 5mo agoConjecture: the first AI to successfully manage a McDonald’s will be a Gemini.
- econ 5mo agoThey no longer have to limit themselves to forking software but can do a global Google Burgers in a single prompt. It will no doubt be a huge success before shut down.
- pamcake 5mo ago> Obviously playing Kasparov on the board requires more planning ability than managing a McDonald's 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.
- vatsachak 5mo agoThat's true. I should clarify by saying I meant that a human playing on par with Kasparov obviously has the planning ability to manage a McDonald's
- necovek 5mo agoBut that is also non-obvious. Even managing human employees — let alone customers — required a planning ability related to emotional intelligence that many a person with good pure logic ability simply lacks. 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.
- sigmoid10 5mo agoManaging a McDonalds is a question of integration and modalities at this point. I don't think anyone still doubts that these models lack the reasoning capability or world knowledge needed for the job. So it's less of a fundamental technical problem and more of a process engineering issue.
- throw-the-towel 5mo agoThe capability they lack is being able to be sued.
- pear01 5mo agoPolice officers are human. In the United States in the vast majority of cases you can't sue the police, only the community responsible for them. https://en.wikipedia.org/wiki/Qualified_immunity 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.
- nemomarx 5mo agoMcDonald's are franchises - you generally want to sue the local owner or threaten them in addition to the holding company. 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.
- lancekey 5mo ago25/75%. Plenty of stores are owned directly by McDonalds corp.
- logicchains 5mo ago
- forinti 5mo agoAI is already too old for that.
- Terr_ 5mo ago> manage a McDonald's 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. [0] https://en.wikipedia.org/wiki/Manna_(novel) https://en.wikipedia.org/wiki/Manna_(novel)
- kmeisthax 5mo agoCasual reminder that the author's proposed solution to the labor-automation dystopia is to invent a second identity-verification dystopia. Also casual reminder that the author wanted the death penalty to anyone over the age of 65.
- embedding-shape 5mo agoI was curious about this book but now you've absolutely sold me on it, sounds like I'm in for a ride!
- tomjakubowski 5mo agoAmazing bit of trivia that the founder of HowStuffWorks.com was named Marshall Brain.
- falcor84 5mo agoSeeing how it's hard to identify sarcasm on the internet, I'll just clarify that it of course is the same person - https://en.wikipedia.org/wiki/Marshall_Brain https://en.wikipedia.org/wiki/Marshall_Brain And I'll also link to the HN thread following his death a couple of years ago - https://news.ycombinator.com/item?id=42228759 https://news.ycombinator.com/item?id=42228759
- deleted 5mo ago[deleted]
- evenhash 5mo agoThe proof is not written in Lean, though. It’s written in English and requires validation by human experts to confirm that it’s not gibberish.
- vatsachak 5mo agoYeah, but I wouldn't be surprised if they train the model on verification assisted by Lean
- whimsicalism 5mo agothe only thing keeping the mcdonalds from happening will be political, likewise the same with fields medal
- trostaft 5mo ago> A difficult part was constructing a chess board on which to play math (Lean). Now it's just pattern recognition and computation. 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.
- vatsachak 5mo agoYeah, but I wouldn't be surprised if they train the model on verification assisted by Lean.
- trostaft 5mo agoArguing similarly to how stockfish, the chess engine, trains I would not be surprised if this is more common in the future. I don't know if they use any proof verification tools during their reinforcement learning procedure right now, as far as I know they've been focusing more on COT based strategies (w/o Lean). But I'm hardly an LLM expert, I don't know.
- vatsachak 5mo agoThey most definitely threw in rl with formal verification somewhere between GPT 4 and now. The models are better at not hallucinating. I don't think their IMO team are only show ponies...
- cma 5mo agoSame could be said for human mathematicians that learn from tools like Lean.
- ComplexSystems 5mo agoThat may be true for now, but it seems clear enough that letting the model use Lean in its internal reasoning process would be a great idea
- segmondy 5mo agoour local AI models are already capable of running McDonalds.
- hoppyhoppy2 5mo agoWhy aren't they doing so?
- ric2b 5mo agoNo they aren't, they can't even manage a vending machine.
- volkercraig 5mo ago> we'll see more specialized math AI resembling StockFish soon Heuristically weighted directed graphs? Wow amazing I'm sure nobody has done that before.
- vatsachak 5mo agoMy claim is that LLMs waste a lot of time training on all available data. 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
- red75prime 5mo agoIt has been tried. Lenat's Automated Mathematician, for example. The problem is that the system succumbs to combinatorial explosion, not knowing which directions are interesting/promising/productive. LLMs seem to pick up some kind of intuition from the data they are fed. The generated data might not have the needed "human touch" or whatever it is.
- vatsachak 5mo agoIt might just be that we didn't have enough compute till now. StockFish definitely has superior intuition
- red75prime 5mo agoStockFish amplifies weak "intuition" (heuristic and simple neural estimators) through extensive Alpha-Beta search made possible by the low(ish) branching factor of chess. It doesn't work for Go already (KataGo uses larger neural networks to guide search more efficiently). I doubt either will work for math where branching factor is even bigger and the success criteria (is the result interesting and so on) are not strictly defined.
- ori_b 5mo agoWe're automating art and science so that we can flip burgers. This future sucks.
- vatsachak 5mo agoMath is a very specialized subset of art and science more amenable to automation.
- ori_b 5mo agoThe first thing we automated passably was art, even before programming. Were you not paying attention? This future still sucks. The tech industry is making the world a worse place.
- amunozo 5mo agoCalling AI-generated images art is a stretch. Same thing with creative writing. It can make some low-cost illustrations and writing, but it is very far from decent art. Compare those results with their amazing coding or math capabilities.
- ori_b 5mo agohttps://www.astralcodexten.com/p/how-did-you-do-on-the-ai-art-turing https://www.astralcodexten.com/p/how-did-you-do-on-the-ai-ar... Two years old now, and as the cryptographers say, attacks only get better.
- amunozo 5mo agoThose are either copies or bad. I think the difference in quality and originality is huge, even if they can create plausible looking images in already invented styles.
- ori_b 5mo agoAnd yet, they're good enough to fool most people, which is what you're trying for if you're aiming to automate the production of art. The fact that we got there more than 2 years ago, before agentic coding was even barely useful, should give you an idea of where things are going.
- dyauspitr 5mo agoNonsense. Have you been watching the figure live stream? Or the Unitree video from yesterday with real time novel action generation? We’re less than a year away. If you can cook a burger, assemble a sandwich and clean up surfaces you’re all of the way there.
- KalMann 5mo agoI think your analogy is good but I don't believe modern LLMs use Lean or any lean-like structure in their proofs. At least recent open source ones like DeepSeek can do advanced math without it (maybe the most cutting edge ones are doing it I can't say).
- vatsachak 5mo agoThey are most likely using them in training. I doubt their IMO team are show ponies
- auggierose 5mo ago> A difficult part was constructing a chess board on which to play math 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.
- huflungdung 5mo ago[dead]
- fapjacks 5mo agoI dunno. Is AI less than forty years old?
- brikym 5mo agoHey ChatGPT, if a person spills hot McCoffee on themselves who is at fault?
- brookst 5mo agoWell, brikym, exactly how hot is this hot coffee? If it’s within normal expectations for coffee it is likely that person’s fault. If it is 210 degrees F, it is likely McDonald’s fault.
- energy123 5mo agoThe issue with this prediction is the gulf between problem-solving using known tools, versus creating new concepts for problems where existing tools aren't enough. 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.
- jeremyjh 5mo agoStockfish did not teach itself to play chess. You are probably thinking of Leela Chess Zero - an open re-implementation of AlphaZero - both were given nothing but the rules of chess and a board and played millions of games against themselves until they were the strongest engine available at the time. 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.
- xigoi 5mo ago> at one ply it has an ELO of around 2300, Stockfish is probably closer to 1800 Nitpick: it’s Elo, not ELO. The name comes from the inventor’s surname and is not an acronym.