陶哲轩上手Copilot:不可思议,它能从定理名字猜出我想要的方向

尝鲜 GPT-4 之后,陶哲轩又用上了 Github Copilot。这一次,他的试用场景是学习 Lean 言语并利用其形式化数学定理。对于大模型来说,形式化的定理证实也算一种挑战。形式化证实本质上是一种计算机程序,但与 C 或 Python 中的传统程序不同,证实的正确性可以用证实助手(比如 Lean 言语)来考证。定理证实是代码生成的一种特殊形式,在评估上非常严格,没有让模型产生幻觉的空间。而陶哲轩提到的定理,来自 10 月 9 日的一篇论文:论文中的这个证实只有不到一页,但陶哲轩的形式化证实使用了 200

尝鲜 GPT-4 之后,陶哲轩又用上了 Github Copilot。

这一次,他的试用场景是学习 Lean 言语并利用其形式化数学定理。

陶哲轩上手Copilot:不可思议,它能从定理名字猜出我想要的方向

对于大模型来说,形式化的定理证实也算一种挑战。形式化证实本质上是一种计算机程序,但与 C++ 或 Python 中的传统程序不同,证实的正确性可以用证实助手(比如 Lean 言语)来考证。定理证实是代码生成的一种特殊形式,在评估上非常严格,没有让模型产生幻觉的空间。

而陶哲轩提到的定理,来自 10 月 9 日的一篇论文:

陶哲轩上手Copilot:不可思议,它能从定理名字猜出我想要的方向

论文中的这个证实只有不到一页,但陶哲轩的形式化证实使用了 200 行 Lean 言语。

举例来说,在论文中,陶哲轩只是断言对于肆意 a>0 的情况,陶哲轩上手Copilot:不可思议,它能从定理名字猜出我想要的方向在实数上是凸的,因为这是一个常规的微积分练习,然后调用了 Jensen 不等式,但写出所有细节用了大约 50 行代码。

陶哲轩表示,Github copilot 能够正确预测各种例行考证的多行代码,并从定理的名字等线索中推断出他想要的方向,这种能力是「不可思议」的。

Lean 的「重写」策略是不可或缺的,它可以通过有针对性的替换来修改漫长的假设或目标,无需完整地键入表达式就能对其举行操作。

「在用 LaTeX 撰写证实时,我经常粗略地模拟这种方法,将我要处理的漫长表达式从一行剪切粘贴到下一行,然后举行有针对性的编辑,但这有时会导致错字在文档中多行传播,因此能以自动和可考证的方式举行重写是件好事。」

论文中还提到一个不等式,即对于肆意的 k, l, n,满足 陶哲轩上手Copilot:不可思议,它能从定理名字猜出我想要的方向,则

陶哲轩上手Copilot:不可思议,它能从定理名字猜出我想要的方向陶哲轩表示下一个目标就是建立该不等式的简单版本,即论文中的不等式 (1.8):

陶哲轩上手Copilot:不可思议,它能从定理名字猜出我想要的方向

这部分的证实主要还是利用微积分的知识,但有一个难点是需要使用渐近符号。陶哲轩表示后续的论证虽然会很耗时,但并不是特别困难。

陶哲轩上手Copilot:不可思议,它能从定理名字猜出我想要的方向

但目前的工具仍有一些局限性,例如,重写涉及绑定变量(如数列中的求和变量)的表达式并不总是很容易完成。他期待着有一天,人们可以简单地要求自然言语 LLM 举行此类转换……

参考链接:https://mathstodon.xyz/@tao/111271244206606941

给TA打赏
共{{data.count}}人
人已打赏
理论

数学逻辑和计算机程序代码之间的深层联系:互为镜像

2023-10-23 15:31:00

理论

生成的份子几乎 100% 有效,用于逆向份子安排的带领集中模型

2023-10-24 11:26:00

0 条回复 A文章作者 M管理员
    暂无讨论,说说你的看法吧
个人中心
今日签到
有新私信 私信列表
搜索