每天听简报，了解最新科技、AI、软件资讯
一份针对 OpenAI 流体方程证明的预印本指出，Lean 代码通过检查，并不能保证它忠实对应文字版论证。Lean 是机械检查数学证明的工具。十月六日，三位研究者举例说，文字稿的一项估计，只要求额外四阶导数，所引用的代码却要求五阶，条件更强。他们还展示，模型能把错误的文字论证改成另一份正确证明，然后通过检查。因此，检查成功不能倒过来给原来的每一步推理背书。作者明确声明，没有据此判定 OpenAI 的文字证明错误；他们质疑的是两种版本之间的对应关系。
进度保存在本设备 · 登录同步