Why I'm still bearish on LLMs after Navier-Stokes
https://dank.systems/posts/2026-09-15-ai-bear.html📌 Navier-Stokes 之後,為何我仍看空 LLM 的自動化敘事
TL;DR:作者主張數學證明是 agentic AI 的「最佳案例」,絕大多數知識工作因缺乏嚴謹規格而無法照搬這套成功模式。
當 LLM 攻克 Navier-Stokes 這類頂級數學難題時,很容易讓人以為「取代大部分知識工作者」的敘事已近在眼前。但在 Hacker News 上獲得 437 點、569 則留言的一篇長文裡,作者 jaykru 提出了相反的論點:這些頭條案例恰恰是最不具代表性的特例。
🤔 前沿實驗室的估值,建立在一個尚未成立的假設上
作者開門見山地指出核心主張:前沿實驗室的市場定價,是根據「已經或即將產出可大規模取代知識工作者的全自動系統」這個敘事,但當前的前沿模型,即便面對最簡單的任務,仍需要大量人工監督與護欄(guardrail)。作者認為,那些被 Navier-Stokes 證明、FreeBSD RCE 漏洞挖掘、HuggingFace 事件等頭條案例迷惑的人,只要看看軟體公司仍持續聘用「後段班」工程師(即便這些人在各種 benchmark 上的表現遠不如模型),就能發現真實的自動化程度遠不如宣傳。
🧩 數學證明是「最佳案例」,而非常態
文章的核心論證是:Navier-Stokes 這類純數學陳述,是 agentic AI 能發揮作用的最理想情境,因為定理陳述本身就已經是一份嚴謹的規格(specification),經過數學社群數十年的審查,而且用 Lean 這類定理證明器來驗證時,幾乎不可能被「reward hack」(儘管作者也承認,過去確實出現過 soundness bug 讓 LLM 用漏洞矇混過關的案例)。
但作者強調,絕大多數的知識工作並不長這樣。多數任務不存在這種「一次寫好規格、後續持續照著實作」的模式,嚴謹的正式規格往往需要在實作過程中不斷與非正式規格的發現互相修正、演化。
📊 規格撰寫的成本,可能遠高於直接動手做
文章舉了硬體工程作為案例:典型的 CPU 專案,規格與驗證工程師的人數,往往是設計工程師的三倍,某些專案甚至達到 5:1 的比例。作者的論點是:當任務不具備現成的嚴謹規格時,撰寫規格本身就是一門高度專業化的技能,而「同時懂領域知識、又懂如何寫規格」的人才極其稀少,導致規格撰寫的人力成本,可能遠超過直接以非正式方式實作的成本。
作者也提到,人工審查(human review)雖是規格之外的替代方案,但既無法應付 LLM 產出的巨量內容,審查本身也高度容易被規避,並舉出 xz backdoor 與 Linux 核心的「UMN 偽善提交」事件作為例證,說明即便是專業人工審查也不是萬靈丹。
💡 哪些公司能真正用得上全自動 LLM agent?
作者將能夠接受全自動 LLM 的公司歸納為三類:能廉價承受失敗的公司(如原本就會僱用實習生、或做快速原型的團隊)、只需要處理一小組有明確護欄的重複性任務的公司(如客服對話、受控環境中的重複性勞動),以及本來就必須承擔嚴謹規格與驗證成本的產業(如晶片設計、藥物開發)。作者認為前兩類公司對推理能力的要求其實不高,反而更適合用便宜的開源模型在本地端運行;第三類公司雖可能仍用前沿模型,但作者也質疑,這類任務是否真的無法用如 DeepSeek V4.1 Flash 這類更便宜的模型完成。
⚠️ 作者自陳的立場與侷限
需要留意的是,這篇文章本質上是一篇論戰性質強烈的個人觀點文,而非研究論文,其中援引的案例(如「春季 2026 熱潮」中開源小模型重現 Mythos CVE)也未附上具體數據佐證,讀者應將其視為一種產業觀察與批判性假說,而非嚴謹的實證結論。
🎯 實務啟示
對正在評估是否導入 agentic AI 到生產流程的工程團隊,這篇文章提供了一個實用的篩選框架:先問自己的任務是否具備清晰規格、是否能承受失敗成本、或是否已經具備嚴謹驗證流程的組織文化。如果都不符合,那麼「全自動 agent 取代人力」的路徑,可能比想像中遙遠得多。
🔗 來源
- 標題:Why I’m still bearish on LLMs after Navier-Stokes
- 作者/機構:jaykru(Hacker News,437 points,569 comments)
- 連結:https://dank.systems/posts/2026-09-15-ai-bear.html
#LLM #AIAgents #AIAutomation #FormalVerification #SoftwareEngineering #AICritique #RewardHacking #TheoremProving #AIHype #KnowledgeWork
原始資料 Hacker News · 收集於 2026-09-16
摘要原文
why i'm still bearish on LLMs after navier-stokes Why I'm still bearish on LLMs after Navier-Stokes orthography mode: based | cringe cringe mode is provided with AI assistance, switch to based mode if you prefer artisanal tokens. [ thank you to claude fable 5.1, holden saberhagen, gabriel kammer, andres erbsen, alice mckean, and tristan wylde-larue for comments on this post ] i'll begin with a few theses for the reader to chew on: the frontier labs are priced according to the narrative that they have produced or will in the very near future produce a fully automated drop-in replacement for most knowledge workers, but current frontier models need laborious oversight and guardrails on even the simplest tasks. one misled by the headline shows of force (navier-stokes, freebsd RCEs, the huggingface incident) and frontier lab rhetoric into believing meaningful autonomy has been achieved need only look at the software firms continuing to employ and hire bottom quartile software engineers who would score far below the models they supervise on the benchmarks du jour. the models generalize well only on tasks within a small neighborhood of the specific tasks they've been trained on, and even then with severe caveats. the frontier labs have developed a general recipe to teach models almost any specific task enjoying clearly defined levels of task performance; many tasks are covered in the training data; but even small perturbations within a covered class of task result in outright failure or reward hacking. the present problem of reward hacking can be solved only by rigorous specification by domain experts. the time of domain experts is expensive. rigorous specification is itself a skill, demanding its own expertise outside of a given problem domain. even many skilled software engineers are bad at it. for the vast majority of domains, the intersection of domain experts and specification experts is ludicrously small. the labor costs of rigorous specification can greatly exceed that of direct implementation of an informal specification. the hardware engineering world presents a great case study on this, where a typical CPU project anecdotally has about three times as many specification and validation engineers as design engineers and a 5:1 ratio is not unheard of . even worse, many tasks don't admit a convenient spec-and-forget regime where you write a specification once and continuously implement against it: rigorous formal specifications frequently evolve in conversation with insights derived from discoveries made while implementing according to the informal specification. for tasks that enjoy high level one-and-done specifications (say an executable ISA specification for a family of CPU architectures) the costs of verification against such high level specifications are insurmountable with current technology, necessitating the use of lower level specifications that are both more expensive to construct and far more fragile to design flux. navier-stokes and statements in pure mathematics like it are the absolute best case scenario for agentic work against rigorous specification. the theorem statement itself is already a rigorous specification. it has undergone decades of auditing by the mathematical community and its rendering in lean is a straightforward translation defined in terms of battle-tested mathematical objects from mathlib. the verifier, the lean theorem prover, has been extensively audited and specifically designed to avoid the types of unsoundness that would make it vulnerable to reward hacks. even lean and theorem provers like it are not invulnerable: soundness bugs have allowed LLMs to launder bogus proofs through the proof kernel before and it is not improbable that more such bugs exist. this is the rosiest setup; the vast majority of human knowledge work does not look like this. i'll comment below on the few areas of knowledge work that do resemble pure mathematics in this respect. the best alternative to rigorous specification is human review. human review doesn't scale well to the volumes of output produced by language models. to make matters worse, even expert human review is extremely vulnerable to reward hacking: consider the xz backdoor and the infamous UMN hypocrite commits that landed in linux. if human review remains a critical part of the agentic production loop, the pace of production is necessarily bottlenecked by factors like the limits of human time and attention; it is a total non-starter for the country full of geniuses in a datacenter frontier lab CEOs would have you believe is perpetually just a few more months out. taken together, it appears that for most domains LLMs will continue to look like a cracked intern: quick and effective in the hands of an adult but not given run of the place. most firms will not be able to adopt fully autonomous AI, not for problems of skill issue or lagging technology diffusion but rather for structural reasons seemingly endemic to current architectures. the classes of firms that can accept the use of fully autonomous LLMs are few, by my count just three: those who can accept failure cheaply: firms that would otherwise hire interns, firms involved in rapid prototyping work, etc. those who need done a small set of narrowly defined tasks with existing clear guardrails: repetitive physical labor in a controlled environment, call center and customer service chat work, etc. those that can accept or already do by nature the costs of rigorous specification and validation: chip design, drug discovery, and other domains where failure on deployment is an existential concern. the first two classes are price sensitive and arguably don't need the jump in reasoning quality you see going from cheap to frontier models. most of these firms will be best served by open models running on cheap hardware, perhaps even locally at the site of use. for the first and third classes, the type of fuzzy combinatorial search that has produced headline results in mathematics and security research seems more sensitive to agentic swarm width than reasoning capacity: see small open models reproducing the mythos CVEs that drove the spring 2026 hype cycle. if that is indeed true, there is even greater reason to use cheap open models that enable you to run the same workload with wider swarms. the third class of firms might still use frontier models, though it's not totally clear that their work couldn't be done with cheap models like deepseek v4.1 flash, and the swarm width advantage i hypothesized above gives them all the more reason to push for cheaper models. another interesting property of firms of this class is that they are generally very secretive about their IP and probably aren't overjoyed about shipping it all to anthropic and openai even with supposed agreements to not train on user data . now, you might propose that even if the frontier labs are cooked, the data center full of brainlets scenario drives just as much AI compute as an artificial superintelligence scenario. the difference is that the data center full of geniuses is self-driving and limited only by how much compute it can consume while the brainlet swarms will be heavily bottlenecked by their human orchestrators. my personal bet is that the blast radius will go far beyond the frontier labs. [ Thank you to Claude Fable 5.1, Holden Saberhagen, Gabriel Kammer, Andres Erbsen, Alice McKean, and Tristan Wylde-LaRue for comments on this post ] I'll begin with a few theses for the reader to chew on: The frontier labs are priced according to the narrative that they have produced or will in the very near future produce a fully automated drop-in replacement for most knowledge workers, but current frontier models need laborious oversight and guardrails on even the simplest tasks. (437 points, 569 comments on Hacker News)
由 claude-code/sonnet 自動生成