Not just long context in general (that can be partially mitigated with RAG or even BM25/tf-idf search), but also nearly 100% factual accuracy on it, as I argued last week
Petropolitan
Karma: 141
https://simple-bench.com presents an example of a similar benchmark with tricky commonsense questions (such as counting ice cubes in a frying pan on the stove) also with a pretty similar leaderboard. It is sponsored by Weights & Biases and devised by an author of a good YouTube channel who presents quite a balanced view on the topic there and don’t appear to have a conflict of interest either. See https://www.reddit.com/r/LocalLLaMA/comments/1ezks7m/simple_bench_from_ai_explained_youtuber_really for independent opinions on this benchmark
Two months later I tried to try actually implementing a nontrivial conversion of a natural language mathematical argument to a fully formalized Lean proof in order to check if I was indeed underestimating it (TBH, I have never tried a proof assistant before).
So I took a difficult integral from a recent MathSE question I couldn’t solve analytically myself, had Gemini 2.5 Pro solve it 0-shot,[1] verified it numerically, set up a Lean environment in Google Colab and then asked if another instance of Gemini 2.5 could convert the solution into a proof. It told me that it is indeed hard:
This is not a trivial task. Here’s why:
Informal vs. Formal: My natural language explanation, while aiming for clarity, likely skipped steps, relied on implicit assumptions (like function continuity, differentiability, domain constraints), or used intuitive leaps that Lean demands be made explicit and rigorously justified using defined theorems and axioms.
Library Navigation: Finding the exact theorems in mathlib4 that correspond to each step (e.g., the correct version of integration by parts, substitution, limit theorems, properties of specific functions) requires familiarity with the library.
Side Conditions: Every theorem in Lean (like the chain rule or integration by parts) has precise side conditions (e.g., f is differentiable, g’ is continuous, the function is integrable). The natural language proof might not have explicitly stated or verified all of these, but the Lean proof must.
Calculations: Even seemingly simple algebraic manipulations or derivative calculations need to be carried out using Lean’s tactics (ring, linarith, simp, rw, etc.) or proven step-by-step.
Proof Structure & Tactics: Structuring the proof correctly in Lean and using the appropriate tactics (apply, exact, calc, by, etc.) to guide the prover is a skill in itself.
My Limitations: While I can generate code snippets, generating a complete, correct, and non-trivial formal proof interactively is currently beyond my capabilities. It often requires a human expert to guide the process, debug errors, and find the right lemmas.
<...>
It is highly unlikely that I can produce a complete, automatically verifiable Lean proof for a “tricky” integral directly from a natural language description. However, if you provide the details, I can attempt to sketch out the Lean concepts involved, which could be a starting point for someone (perhaps you in Colab, with time and learning) to build the actual proof.
Gemini and I weren’t able to set up mathlib4 in Lean 4 and I gave up on the task, but already by just looking on a solution Gemini listed the following problems[2] (I put it here as a screen capture instead of a proper collapsible section because I couldn’t figure out how to copypaste the formulas right):
To sum up, yes, I did underestimate the hardness of the task, it is certainly beyond the reach of current SOTA LLMs.
However, I believe that since this type of task is verifiable in silico and really very convenient for synthetic training data generation, Google folks behind AlphaGeometry are probably going to solve this problem in a year or two.
- ^
The fact that an LLM solved it 0-shot is notable in its own right BTW. Generally, I’ld estimate that Gemini 2.5 and o3-mini are able to solve most of the definite integrals posted in MathSE questions. It was very different at the beginning of this year!
- ^
I haven’t checked accuracy of all the generated details due to lack of competence and time but generally expect the outline to be broadly correct
Aren’t you supposed as a reviewer to first give the authors a chance to write a rebuttal and discuss it with them before making your criticism public?
One of non-obvious but very important skills which all LLM-based SWE agents currently lack is reliably knowing which subtasks of a task you have successfully solved and which you have not. I think https://www.answer.ai/posts/2025-01-08-devin.html is a good case in point.
We have absolutely seen a lot of progress on driving down hallucinations on longer and longer contexts with model scaling, they probably made the charts above possible in the first place. However, recent research (e. g., the NoLiMa benchmark from last month https://arxiv.org/html/2502.05167v1) demonstrates that effective context length falls far short of what is advertised. I assume it’s not just my personal experience but common knowledge among the practitioners that hallucinations become worse the more text you feed to an LLM.
If I’m not mistaken even with all the optimizations and “efficient” transformer attempts we are still stuck (since GPT-2 at least) with self-attention + KV-cache[1] which scale (at inference) linearly as long as you haven’t run out of memory and quadratically afterwards. Sure, MLA have just massively ramped up the context length at which the latter happens but it’s not unlimited, you won’t be able to cache, say, one day of work (especially since DRAM has not been scaling exponentially for years https://semianalysis.substack.com/p/the-memory-wall).
People certainly will come up with ways to optimize long-context performance further, but it doesn’t have to continue scaling in the same way it has since 2019.
- ^
Originally known as “past cache” after the tensor name apparently coined by Thomas Wolf for the transformers library in February 2019, see commit ffd6238. The invention has not been described in the literature AFAIK, and it’s entirely possible (maybe even likely) that closed-source implementations of earlier decoder-only transformers used the same trick before this
- LLM AGI will have memory, and memory changes alignment by (Apr 4, 2025, 2:59 PM; 73 points)
- 's comment on Surprising LLM reasoning failures make me think we still need qualitative breakthroughs for AGI by (Apr 17, 2025, 9:00 PM; 2 points)
- 's comment on Shortform by (Mar 26, 2025, 6:05 PM; 1 point)
- ^
To be honest, what I originally implied is that these founders develop their products with low-quality code, as cheap and dirty as they can, and without any long-term planning about further development
Perhaps says more about Y Combinator nowadays rather than about LLM coding
Aristotle has argued (and I support his view) in the beginning of the Book II of the Nicomachean Ethics that virtues are just like skills, they are acquired in life by practice and imitation of others. Perhaps not a coincidence that a philosophical article on the topic used “Reinforcement” in one of its subheadings. I also attach a 7-minute video for those who prefer a voice explanation:
For this reason, practice ethical behavior even with LLMs and you will enjoy doing the same with people
Another example is that going from the first in-principle demonstration of chain-of-thought to o1 took two years
The correct date for the first demonstration of CoT is actually ~July 2020, soon after the GPT-3 release, see the related work review here: https://ar5iv.labs.arxiv.org/html/2102.07350
When general readers see “empirical data bottlenecks” they expect something like a couple times better resolution or several times higher energy. But when physicists mention “wildly beyond limitations” they mean orders of magnitude more!
I looked up the actual numbers:
in this particular case we need to approach the Planck energy, which is eV, Wolfram Alpha readily suggests it’s ~540 kWh, 0.6 of energy use of a standard clothes dryer or 1.3 of energy in a typical lightning bolt; I also calculated it’s about 1.2 of the muzzle energy of the heaviest artillery piece in history, the 800-mm Schwerer Gustav;
LHC works in the eV range; 14 TeV, according to WA, can be compared to about an order of magnitude above the kinetic energy of a flying mosquito;
the highest energy observed in cosmic rays is eV or 50 J; for comparison, air and paintball guns muzzle energy is around 10 J while nail guns start from around 90 J.
So in this case we are looking at the difference between an unsafely powerful paintball marker and the most powerful artillery weapon humanity ever made (TBH I didn’t expect this last week, which is why I wrote “near-future”)
On the other hand, frontier math (pun intended) is much worse financed than biomedicine because most of the PhD-level math has barely any practical applications worth spending many manhours of high-IQ mathematicians (which often makes them switch career, you know). So, I would argue, if productivity of math postdocs when armed with future LLMs raises by, let’s say, an order of magnitude, they will be able to attack more laborious problems.
Not that I expect it to make much difference to the general populace or even the scientific community at large though
general relativity and quantum mechanics are unified with a new mathematical frame
The problem is not to invent a new mathematical frame, there are plenty already. The problem is we don’t have any experimental data whatsoever to choose between them because quantum gravity effects are expected to be relevant at energy scales wildly beyond current or near-future technological limitations. This has led to a situation where quantum gravity research has become largely detached from experimental physics, and AI can do nothing about that. Sabine Hossenfelder has made quite a few explainers (sometime quite angry ones) about it
The third scenario doesn’t actually require any replication of CUDA: if Amazon, Apple, AMD and other companies making ASICs commoditize inference but Nvidia retains its moat in training, with inference scaling and algorithmic efficiency improvements the training will inevitably become a much smaller portion of the market
It’s a bit separate topic and not what was discussed in this thread previously but I will try to answer.
I assume because Nvidia’s moat is in CUDA and chips with high RAM bandwidth optimized specifically for training while competition in inference (where the weights are static) software and hardware is already higher, and going to be even higher still by the time DeepSeek’s optimizations become a de-facto industry standard and induce some additional demand
I don’t think the second point is anyhow relevant here while the first one is worded so that it might imply something on the scale of “AI assistant convinces a mentally unstable person to kill their partner and themselves”—not something that would be perceived as a warning shot by the public IMHO (have you heard there were at least two alleged suicides driven by GPT-J 6B? The public doesn’t seem to bother https://www.vice.com/en/article/man-dies-by-suicide-after-talking-with-ai-chatbot-widow-says/ https://www.nytimes.com/2024/10/23/technology/characterai-lawsuit-teen-suicide.html).
I believe that dozens of people killed by misaligned AI in a single incident will be enough smoke in the room https://www.lesswrong.com/posts/5okDRahtDewnWfFmz/seeing-the-smoke for the metaphorical fire alarm to go off. What to do after that is a complicated political topic: for example, French voters has always believed that nuclear accidents look small in comparison to the benefits of the nuclear energy while Italian and German ones hold the opposite opinion. The sociology data available, AFAIK, generally indicates that people in many societies have certain fears regarding possible AI takeover and is quite unlikely to freak out less than it did after Chernobyl, but that’s hard to predict
This is a scenario I have been thinking for perhaps about three years. However you made an implicit assumption I wish was explicit: there is no warning shot.
I believe that with such a slow takeoff there is a very high probability of an AI alignment failure causing significant loss of life already at the TAI stage and that would significantly change the dynamics
This seems to be the line of thinking behind the market reaction which has puzzled many people in the ML space. Everyone’s favorite response to this thesis has been to invoke the Jevons paradox https://www.lesswrong.com/posts/HBcWPz82NLfHPot2y/jevon-s-paradox-and-economic-intuitions. You can check https://www.lesswrong.com/posts/hRxGrJJq6ifL4jRGa/deepseek-panic-at-the-app-store or listen to this less technical explanation from Bloomberg:
Basically, the mistake in your analogy is that demand for the drug is limited and quite inelastic while the demand for AI (or basically most kinds of software) is quite elastic and potentially unlimited.
I absolutely agree with the comparison of o3 at ARC-AGI/FrontierMath to brute forcing, but with algorithmic efficiency improvements that million dollar per run is expected to gradually decrease, first becoming competitive with highly skilled human labor and then perhaps even overcompeting it. The timelines depend a lot on when (if ever) these improvements plateau. The industry doesn’t expect it to happen soon, cf. D. Amodei’s comments on their speed actually accelerating https://www.lesswrong.com/posts/BkzeJZCuCyrQrEMAi/dario-amodei-on-deepseek-and-export-controls
Even if LMMs (you know, LLMs sensu stricto can’t teach kids read and write) are able to do all primary work of teachers, some humans will have to oversee the process because as soon as a dispute between a student and an AI teacher arises, e. g., about grades or because of the child not willing to study, parents will inherently distrust AI and require a qualified human teacher intervention.
Also, since richer parents are already paying for more pleasant education experience in private schools (often but not always organized according to Montessori method), I believe that if jobs and daycare really become the focus of middle education taxpayers would gladly agree to move the school system into more enjoyable and perhaps gamified direction. Most likely some workers for whom a teacher wouldn’t be a really appropriate term anymore (pedagogues?) will look after the kids and also oversee the AI teaching process to some extent
Math proofs are math proofs, whether they are in plain English or in Lean. Contemporary LLMs are very good at translation, not just between high-resource human languages but also between programming languages (transpiling), from code to human (documentation) and even from algorithms in scientific papers to code. Thus I wouldn’t expect formalizing math proofs to be a hard problem in 2025.
However I generally agree with your line of thinking. As wassname wrote above (it’s been quite obvious for some time but they link to a quantitative analysis), good in-silico verifiers are indeed crucial for inference-time scaling. But for the most of real-life tasks there’s either no decent, objective verifiers in principle (e. g., nobody knows right answers to counterfactual economics or history questions) or there are very severe trade-offs in verifier accuracy and time/cost (think of wet lab life sciences: what’s the point of getting hundreds of AI predictions a day for cheap if one needs many months and much more money to verify them?)
Isn’t Polymarket already anonymous?