6 d% q. J9 F/ }3 fVlad:我其实不太把自己看作是「加密行业的客户」。我认为 Robinhood 是非常活跃的参与者。就市场份额、交易量、收入而言,尤其在美国,我们已经是加密领域最大的公司之一。 6 E, e# }3 Q1 N% d, s ' [0 M" s8 P! Z ]+ ^$ e: [2 H, I我觉得过去缺失的,是 加密和传统金融体系几乎是两个割裂的世界,中间缺乏连接。稳定币是少数的反例,它们开始起到桥梁作用。但我的态度不是说「你们去修复它」,而是——我们自己就在场内努力改善,利用 Robinhood 的能力和优势,把这个连接点做好。, A, {6 R* Q8 e3 f8 h J
% b/ |$ ]' l, n6 ?5 z- f Robert:当然,这里也有时间因素。比如说,你们现在做了 Robinhood Chain 这个 L2,但也许你们几年前就想做了。: o) T8 g' ?. j f: q$ L1 Q8 T; a 6 e6 B/ c& c! y, U- V
我相信肯定有些事是你会想:「我真希望现在就能做」,但当时技术不够成熟、产品体验太差,或者流动性不足。甚至包括你们现在探索的 私募市场资产,或者 预测市场 的一些尝试。感觉就是,现在时机才刚刚成熟。那你觉得有哪些事,是你想做但还没到时候的?3 H9 N7 x7 W6 c- N; d! G
% y$ O" G8 [, t Vlad:我觉得现在有很多讨论围绕 AI Agent:未来这些 AI 会不会用加密货币彼此支付、完成交易? . Q/ `, ?0 b, J+ X% w% ?4 z. {0 I2 h: G2 J9 N
但除此之外,还有 现实世界的 AI,比如机器人、医疗设备等等。那这些现实世界的 AI Agent 未来会不会也用加密货币相互支付?那会是什么样子?我认为我们离这两种场景都只有一步之遥,再往前一步,就是 加密真正成为 Agentic Commerce 的工具。 ! |6 Q$ R7 Q6 N# I2 {( H, q% u ; c9 X$ ~) M5 D& H% M- WHaseeb:既然你提到了 AI,就顺便问一下:你还在做一个叫 Harmonic 的公司。如果我理解没错的话,你们正在构建一个基础模型,用 Lean 和定理证明(theorem proving)来验证数学,从而验证模型生成的答案,你作为 Robinhood 的 CEO,怎么还有时间做这件事?你在这家公司里参与到什么程度?为什么会选择做这个方向?0 F5 z0 W) t$ i u
' W. q4 f- D7 @- zVlad:我是 Harmonic 的董事长。这是一家和 Robinhood 完全独立的公司,我没有日常的运营角色,但我是创始人,也非常关心它。6 s/ U) ?3 V$ F9 q- S. K# d
) E2 d. ?0 ]) c6 T几周前,Harmonic 宣布我们的模型 Aristotle 在国际数学奥林匹克竞赛(IMO)上达到了金牌水平。大家可能知道,这是一项极其困难的数学考试。像 GPT-5、Grok 这样的现成大模型,在这种题目上通常连一道完整的题都解不出来,表现非常差。 ! q8 ~$ m& K! s4 b" G$ l. T! S& R# A8 n' v7 I5 B
问题有两个方面。一是这些题需要「灵光一闪」的创造力,如果找不到那个切入点,就完全解不出;二是它们通常需要 10 步以上的逻辑推理,只要其中一步错了,整个证明就错误,结果也就不对。9 [: r; f+ L: G+ y1 W( W7 h% ^$ W
2 M' z/ p" m2 g& Q7 ?
所以要同时具备创造力和逻辑严谨性。而且在这种场景下,AI 的「幻觉」问题会层层叠加。因此,这次结果是对我们技术的一个很好的验证。8 S7 D1 b7 ^& D% t. Z, e
* O* s' _( r. {事实上,我们是用形式化方式完成的。你刚才提到 Lean 定理证明器,我们确实用它来生成形式化证明。这意味着结果不需要人类手动验证,只要把它输入 Lean 内核,系统就会逐步检查每一步证明是否正确。, G4 H- P' {$ u
) {% V7 ?' N7 n. q* t. K
接下来你可能会问:这有什么应用场景?我们称之为「数学超级智能(mathematical superintelligence)」。 * T9 J/ h# x/ t3 n8 g8 h% U- ]) v: |% N2 U. P' b8 t- \" ]
它的意义在于,AI 不仅能生成答案,还能在非常高的标准下验证答案的正确性。想想现在 AI 已经在大量生成代码。高级软件工程师的工作,正在从「写代码」转变为「验证 AI 写的代码」。如果是前端 UI,还比较容易验证,你可以肉眼确认是否符合设计规范。但如果是后端系统,或者智能合约,尤其在失败可能导致数亿美元损失的场景下,人类必须严格验证。0 ^/ f7 J" `. [/ p' }1 l/ i8 W/ H( A
) U0 m2 s3 _* }1 X. f1 r4 A+ A这就创造了一个 形式化验证的市场。所以我们对这件事很兴奋。我认为它的应用不仅限于数学,还会扩展到所有软件,甚至硬件。3 `( y3 z$ t6 Y8 g
^5 a' n0 g, a2 ^) L2 p. {1 OHaseeb:所以你认为,这是一条更好的路径,能比像 Anthropic 那样的路线更快构建出「软件工程代理」。你觉得:以定理证明和数学作为基础,是实现真正 AGI 的必要前提。 . F* |9 x0 X2 L2 P0 X9 y/ U1 h. a: P; d Vlad:我认为这不仅是更好的路径,而且是不可避免的。因为在一个 AI 大量生成内容的世界里,这些产出已经多到人类根本看不完,我们需要一种新的方式来保证它们是正确的。! E$ {/ o) `$ ]# K, H
, y2 n2 q! f+ W这里有两点:我们必须确保结果是正确的;它甚至不需要用人类能直接读懂的语言来表达,因为人类已经不会逐行去看了。所以,整个底层逻辑会发生变化。问题变成:我们要怎样才能快速验证 AI 的结果是否符合预期,而不用一行一行去人工核对。; J: T P, S# P* v0 E5 t5 K& i
. y4 e+ } a7 n8 K( p/ j Tarun:我有两个相关的问题。第一个算是对形式化验证的一种美学批评。 # x; x, j+ T$ P3 F& U. O2 W' b" s6 r6 |
你当年从大学辍学,却深度参与数学研究,可能就是因为被某些证明的美感吸引了。对我来说也是一样——有些定理的证明简洁优雅,让人觉得极其美妙。而数学一直以来都有一种张力:形式化计算和美学直觉之间很难共存。 ( K. F2 `, L; n6 F1 Z 9 s* c+ C- x6 j# h& s D6 ^
Lean 生成的证明,可能会像「四色定理」的计算机证明一样——极其冗长、不美观,相比之下,人类的间接证明更优雅。你怎么看待这种情况?要如何保留数学的美感?- l' u) j5 _$ R( i- ?
N, {" v/ M! h1 i, w. E0 p7 GVlad:你看过 Aristotle 在 Lean 中生成的证明吗?: p* J) O2 g; R: D2 |
* r4 O7 E8 X5 i% U" Z1 Q& \ @Tarun:我看过一两个,但没看过完整的合集。 & x3 S# k! j( D, v3 w* j2 j7 } 2 m- p0 b' I9 T/ b9 J7 _Vlad:其实我觉得它们很美。而且,把 Lean 证明转换成自然语言,难度并不大,几乎可以机械化完成。5 H) u: f) ?) x. N8 J
, I( F7 @9 ~& q6 k5 m8 o% |$ g
因为 Lean 的函数和定义都有描述,可以很容易地从高度形式化的细节,转换成更具描述性的英文叙述。我觉得这也是 Lean 相对以往形式化语言更容易使用的地方,这也是它不仅在 AI 领域受到欢迎,也在数学家中流行起来的原因。 , P! Z+ E0 g9 ~# P, t, U5 F! e( q- R) S
另一方面,反过来就很难了。把非形式化的证明转化为形式化证明是非常耗费精力的工作。目前在英国帝国理工学院,教授 Kevin Buzzard 正在主导一个大型计划,要把费马大定理完全形式化。这是一个庞大的工程,需要数百名数学家、持续数年,才能手工完成。通过这种对比,你就能看出两者难度的差别。! W( I& n" C9 q M
) j8 `" q; S5 d4 W! n A0 w7 c Tarun:我最后一个问题是:除了千禧年难题(Millennium Prize Problems),你希望 Aristotle 或它的后继模型去解决什么问题?( z! _/ U! h; R2 p# x9 {) \ 9 b" t+ i: R+ R: v. h& ?
千禧年难题太显而易见了,比如黎曼猜想、P=NP 这些,大家都在讨论。但你有没有什么「个人的执念问题」?如果它被解决了,你会觉得「好,这就是我最大的成就」。/ c& I! k+ n/ G) A t5 z5 ?
; k: l" j1 k5 F2 x Vlad:好,那就不说黎曼猜想了。 " K* L* v8 a' I! o- X9 W' e$ n% P i9 M8 E7 B9 Y( P Tarun:对,那太显而易见了。, t/ e5 p$ k' ^1 l0 N. V$ U9 t
& W" x) L0 ?$ ]- f! O Vlad:但其实我还是挺喜欢黎曼猜想的(笑)。如果换一个例子,我觉得做一个「善意版的 HAL 9000」会很酷。我很想打造一个航天器的逻辑核心和控制中心,当然前提是它不会像电影里那样失控、自己起飞。 : L9 n' M% h) d! I5 u/ t% m ; X* u4 g) A& n4 m' G( GHaseeb:呃……你确定这是你想告诉大家的例子吗? ) Z5 n- P. w+ @" Y ! O4 m5 i3 G( F) D2 y4 A7 aVlad:(笑)对,我的意思是要一个可以形式化验证的航天器控制系统。一个真正「善意的 AI」。我们确实需要一个可靠的控制核心。我觉得最初的目标确实是分开的,但现在开始出现重叠。比如 智能合约验证。 2 l) _6 P5 Z+ r' e : w8 |: I: [% p4 X4 W' j4 n智能合约本质上是运行在 Solidity、Rust 等语言上的一段相对独立的代码。我们必须确保一些基本性质,比如合约不能停摆、不能出现「双重支付」等问题。因为一旦出错,可能导致数亿美元的损失,这已经有过惨痛案例。而目前,智能合约公司几乎只能依赖人工审计——花几十万甚至上百万美元,请外部公司逐行检查代码。1 n6 N4 L" `5 P0 s