) q6 E* c0 i2 k* s$ CTarun:我看过一两个,但没看过完整的合集。 ; L A- r$ w R* b* h9 |8 p / z& c& V: w: j9 l$ ?# ?$ NVlad:其实我觉得它们很美。而且,把 Lean 证明转换成自然语言,难度并不大,几乎可以机械化完成。) V; F* H7 W( D" `; ]8 l0 F$ H
3 {9 U9 v# ~3 c& F因为 Lean 的函数和定义都有描述,可以很容易地从高度形式化的细节,转换成更具描述性的英文叙述。我觉得这也是 Lean 相对以往形式化语言更容易使用的地方,这也是它不仅在 AI 领域受到欢迎,也在数学家中流行起来的原因。& }5 H2 u, }( o R. d! [7 Y% m
; A% D4 b/ \ D N另一方面,反过来就很难了。把非形式化的证明转化为形式化证明是非常耗费精力的工作。目前在英国帝国理工学院,教授 Kevin Buzzard 正在主导一个大型计划,要把费马大定理完全形式化。这是一个庞大的工程,需要数百名数学家、持续数年,才能手工完成。通过这种对比,你就能看出两者难度的差别。3 H4 q1 {9 l% [' o0 e) U/ Q; i+ R
2 c+ a* w8 H1 v6 ]! @ Tarun:我最后一个问题是:除了千禧年难题(Millennium Prize Problems),你希望 Aristotle 或它的后继模型去解决什么问题? 6 W1 r0 X d ^2 M" T# K( E& D9 x2 X
千禧年难题太显而易见了,比如黎曼猜想、P=NP 这些,大家都在讨论。但你有没有什么「个人的执念问题」?如果它被解决了,你会觉得「好,这就是我最大的成就」。3 ^3 D% k, l. N) k1 k6 d; E" t
/ y# z- W1 x5 c P$ B6 [ Vlad:好,那就不说黎曼猜想了。 & _! G9 S" ^6 J" m4 c, a. }+ y 7 Y. O# y% S8 @) p' j; @8 oTarun:对,那太显而易见了。 / ~) P6 c7 y- b- e$ A- u6 v( ?- I ' f/ m8 x! N+ `( a2 W4 xVlad:但其实我还是挺喜欢黎曼猜想的(笑)。如果换一个例子,我觉得做一个「善意版的 HAL 9000」会很酷。我很想打造一个航天器的逻辑核心和控制中心,当然前提是它不会像电影里那样失控、自己起飞。 5 l# D, ~ ~, {5 h$ w8 d2 Q9 v6 `' @& g6 M Haseeb:呃……你确定这是你想告诉大家的例子吗? + s$ |5 w, ]1 a. ?4 A; `, M0 e' u$ W* [' i' [ Vlad:(笑)对,我的意思是要一个可以形式化验证的航天器控制系统。一个真正「善意的 AI」。我们确实需要一个可靠的控制核心。我觉得最初的目标确实是分开的,但现在开始出现重叠。比如 智能合约验证。- A& N5 V& d: ]2 c3 H5 `. q6 M
/ m3 I; Q3 z$ ]- m
智能合约本质上是运行在 Solidity、Rust 等语言上的一段相对独立的代码。我们必须确保一些基本性质,比如合约不能停摆、不能出现「双重支付」等问题。因为一旦出错,可能导致数亿美元的损失,这已经有过惨痛案例。而目前,智能合约公司几乎只能依赖人工审计——花几十万甚至上百万美元,请外部公司逐行检查代码。: l5 M, ~- J8 [! X4 d4 w