访谈/播客

沃顿商学院达梅克·戴维斯：为什么「上下文」是 AI 的下一个重大挑战

Wharton's Damek Davis on Why Context Is the Next Big Challenge in AI

访谈/播客🎤 达梅克·戴维斯 (Damek Davis)⏱ 14:43👁 NA

▶ 在 YouTube 观看

沃顿优化学者达梅克·戴维斯回顾自己从纯数学到机器学习的研究历程，并指出上下文长度、可验证性与不同领域的「真理标准」是当下 AI 面临的核心瓶颈。

核心要点

上下文（context）是当前 AI 最大的挑战之一：前沿模型约 100 万 token 的上下文窗口仍不够用，扩大并提升对长文档（如百页风格指南）的可靠利用，是他最想解决的问题。
在数学与科学中，「可验证性」是核心瓶颈：模型输出看起来很有说服力却未必正确，错误往往藏在「按标准论证」「显然可得」这类被一笔带过的地方。
不同学科有不同的「真理标准」——数学要求 100% 符合公理，物理、医学则依赖实验读数或随机对照试验，这决定了能给模型多强的反馈信号。
自动形式化（autoformalization）正在兴起：Harmonic 的 Aristotle、Axiom Math 等工具尝试用 Lean 等证明系统提供可编译、零错误的强反馈。
他个人的研究兴趣始于 2012 年一个计算机视觉演示，经计算机视觉转向纯数学的优化理论，因为「每次解机器学习问题都要解一个优化问题」。
他正在 Mathematica 中整理一批优化领域的常数/难题作为 AI 基准（benchmark），其中既有 Annals 级难题，也有像 AlphaEvolve 可能已能改进的较易问题。

分章详解

个人介绍与研究历程

戴维斯是宾夕法尼亚大学（沃顿）统计与数据科学系教授，从事优化、机器学习与「AI for math」研究，已任教约十年，拥有数学博士学位。
他在 UCLA 起步于纯数学（交换代数、代数几何），通过资格考后转向应用数学群组。
2012 年被一位计算机系教授的演示吸引（手机拍照后移动即可重新识别物体），在计算机视觉实验室工作约两年，正值深度学习革命早期（AlexNet 时代）。
第四年转回纯数学，跟随新入职教授研究优化理论——动因是他发现自己「解机器学习问题时不会解其中的优化问题」。

机器学习的发展节奏

机器学习概念可追溯到上世纪 50 年代，经历过多轮起落与热度变化。
真正「效果如此之好」的阶段很短，过去三四年「像坐火箭一样」突飞猛进。
技术成熟时间相对其他技术其实并不长，未来潜力仍只能推测。

核心挑战一：上下文（Context）

他认为上下文是巨大问题：前沿模型约 100 万 token，仍希望窗口更大以便注入更多信息、把模型「调教」成特定行为。
举例：他常给模型一份百页风格指南，模型能据此行动，但若上下文问题真正解决会好得多。
上下文不仅是「吸收更多信息」，也是「收窄、约束输出」的一种手段。
近一个月业界热议「递归语言模型（recursive language model）」：把 token 存进 Python 字符串、给模型 Python 终端权限，让其自行编辑上下文；但尚未在规模上得到验证。

核心挑战二：可验证性与自动形式化

判断输出是否正确是做任何科学/数学的巨大瓶颈：可以靠 Lean 编译无错来确认，也可以靠论证书写得「便于人脑快速核验」。
数学家擅长检查证明，但证明常写得很差；错误往往藏在「by a standard/trivial argument」这类被掩盖的难点处。
「LLM 作为裁判 / 解释者」能提供一些信号，但数学需要极强信号——近乎 100% 准确，或至少达到与同事在白板前讨论时那种可信度。
自动形式化代理正在出现：Harmonic Math 的 Aristotle 已公开可试，Axiom Math 有内部版本，OpenAI 据推测也在做。

优化基准与不同领域的「真理标准」

他在 Mathematica 中策划一批优化常数/难题作为 AI 基准，包含 KLS 猜想等定义某一领域多年的硬问题。
Google 的 AlphaEvolve（auto evolve）已能优化证明中的常数，得到很紧的界；他推测这类问题属于其清单中较易的，会持续看到进展。
「真理」的概念因学科而异：数学最强（须 100% 符合公理）；物理分理论（接近数学）与实验（依赖精确仪器读数）；医学常依赖随机对照试验。
引用 Ben Recht 关于青霉素的例子：效果显著到根本无需试验；并提出「临床试验的价值与所需样本量成反比」——需要成千上万样本才看出的效果通常很小。
每个领域都有某种「准确与否」的反馈可喂给模型，但都不如数学反馈那样强。

关键引述

“上下文是个巨大的问题。如果能解决上下文问题，我就能放进更多信息、把模型调教成我想要的样子——这是我最想解决的第一件事。”— 达梅克·戴维斯 (Damek Davis)

“那些难的论证常被一句「按标准论证」「显然可得」一笔带过——而错误恰恰通常就藏在那里。”— 达梅克·戴维斯 (Damek Davis)

“模型的输出被设计得看起来可信、用来说服你（Designed to look plausible and to persuade you），但未必正确。”— 达梅克·戴维斯 (Damek Davis)

“真理的概念在每个学科里都不一样：数学里它最强，必须 100% 正确、符合我们的公理。”— 达梅克·戴维斯 (Damek Davis)

术语 / 人物

达梅克·戴维斯 (Damek Davis) — 宾夕法尼亚大学沃顿商学院统计与数据科学系副教授，UCLA 数学博士，曾任康奈尔大学 ORIE 教授，研究优化、机器学习与 AI for math，获斯隆研究奖、NSF CAREER 奖等。

上下文窗口 (Context window) — 模型一次能读入并可靠处理的 token（约等于词）数量；前沿模型约 100 万 token。

递归语言模型 (Recursive language model) — 近期被讨论的思路：将上下文存为 Python 字符串、给模型 Python 终端权限，让其自行编辑上下文，以突破固定窗口限制。

自动形式化 (Autoformalization) — 把自然语言数学陈述/证明自动翻译成 Lean 等形式化语言以便机器验证，代表工具有 Harmonic 的 Aristotle、Axiom Math 内部系统。

Lean — 交互式定理证明器/形式化数学语言，编译通过即代表证明无逻辑错误，可为 AI 提供强反馈信号。

AlphaEvolve（auto evolve） — Google 的进化式优化软件，可优化证明中的常数等，已得到非常紧的界。

LLM 作为裁判 (LLM as a judge) — 用大模型评判/解释另一个模型的输出，可提供信号，但对数学这类需近 100% 准确的场景信号不够强。

KLS 猜想 (KLS conjecture) — 凸几何/优化中长期未解的著名难题，被列为基准中的硬问题，近来可能接近被解决。

背景补充

达梅克·戴维斯（Damek Davis）是宾夕法尼亚大学沃顿商学院统计与数据科学系副教授，并任统计学双硕士项目联合学术主任。他 2015 年获 UCLA 数学博士（导师 Wotao Yin 与 Stefano Soatto），曾任康奈尔大学 ORIE 教授，研究聚焦优化、机器学习与 AI for math。他获得过斯隆研究奖、NSF CAREER 奖、SIAM 优化方向最佳论文奖及 INFORMS 优化学会青年研究者奖，并担任《Mathematical Programming》《Foundations of Computational Mathematics》副编辑。本视频为他在 SAIR（科学与 AI 研究基金会）启动活动上的现场访谈。

适合谁看

关注 AI for math、形式化证明、优化研究的学者与学生，以及希望了解大模型上下文长度、可验证性与跨学科「真理标准」等前沿瓶颈的从业者。