数学家陶哲轩在形式证明帮助下发现论文中错误

2023-10-29 10:20

本文主要是介绍数学家陶哲轩在形式证明帮助下发现论文中错误,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

数学家陶哲轩在Lean4形式化证明时发现已发表论文中的错误:

陶哲轩在用Lean4发现了一个小错误:论文论证中出现的表达式 12logn-1n-k-1 在 n=3,k=2 的情况下实际上是发散的。幸运的是,这个问题只影响到较小的 n 值,对于 n≥8 的情况,整体论证仍然成立,更小的 n 值可以用更粗糙的方法处理。陶哲轩将添加一个脚注,承认之前版本的论证略有错误,这是在 Lean 中通过形式化发现的。

他在本月初开始在 GPT4 的帮助下学习 Lean4:

使用 Lean4 等形式化证明系统来验证数学证明、捕捉错误和提高严谨性的问题。

陶哲轩利用Lean发现了他最近一篇论文中的一个小错误。交互式定理证明器允许通过逐步证明语句来探索思想,而战术语言等工具则有助于实现常规步骤的自动化。

目前正在开展一些工作,将语言模型与证明助手连接起来,帮助提出策略建议,并有可能找到证明,不过这仍然具有挑战性。

形式化有助于解决历史上由于定义的细微差别而产生的问题。随着时间的推移,形式化的程度可能会提高,从而有助于扩展现有成果和发现。

对于想要简单了解 Lean4 的人来说,自然数游戏非常棒: https: //adam.math.hhu.de/#/g/hhu-adam/NNG4

Lean4 与 TLA+ 或 Alloy 有何不同?
Lamport 的 TLA+更多地是为试图设计系统、写下规格并推理事物如何动态运行的软件人员而设计的。
用于创建形式规范,围绕状态机中的程序行为。TLA+ 以清晰的方式让人有抽象概念。

Lean4 主要用于写下数学证明,而很少用于软件(尽管根据库里-霍华德对应关系,数学证明和程序具有等价性,因此界限有点模糊)。有“mathlib”,它就像一个经过正式验证的数学标准库,人们可以在新的证明中做出贡献和使用。
最近批准了一项多年的努力,开始在Lean4 中形式化费马大定理的证明.

Lean 4 的一个很酷的事情是它也是一种编程语言,使用与证明相同的语法,使您可以轻松地考虑证明您编写的程序的正确性属性。Lean 4 的大部分内容及其策略都是用 Lean 4 编写的(尽管此时几乎所有代码都没有任何相关的证明)。
Leo de Moura 也希望将 Lean 4 用于软件验证。

都打算发展为通用编程语言。

形式验证好处
形式验证几乎是消除 bug 的灵丹妙药,即使它不是 100%(没有什么是)。

它在消除错误方面肯定比模糊的哲学立场要好得多。哲学上会说:“默认情况下使事情安全”(这是什么意思?)或“当你处于糟糕的状态时中止”(你怎么知道你处于“糟糕的状态”) “状态?

形式验证减少了软件开发的艺术性,编程不再是一种手工艺,不再是手工作坊了。

https://www.jdon.com/69361.html

这篇关于数学家陶哲轩在形式证明帮助下发现论文中错误的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/299987

相关文章

AI hospital 论文Idea

一、Benchmarking Large Language Models on Communicative Medical Coaching: A Dataset and a Novel System论文地址含代码 大多数现有模型和工具主要迎合以患者为中心的服务。这项工作深入探讨了LLMs在提高医疗专业人员的沟通能力。目标是构建一个模拟实践环境,人类医生(即医学学习者)可以在其中与患者代理进行医学

论文翻译:arxiv-2024 Benchmark Data Contamination of Large Language Models: A Survey

Benchmark Data Contamination of Large Language Models: A Survey https://arxiv.org/abs/2406.04244 大规模语言模型的基准数据污染:一项综述 文章目录 大规模语言模型的基准数据污染:一项综述摘要1 引言 摘要 大规模语言模型(LLMs),如GPT-4、Claude-3和Gemini的快

论文阅读笔记: Segment Anything

文章目录 Segment Anything摘要引言任务模型数据引擎数据集负责任的人工智能 Segment Anything Model图像编码器提示编码器mask解码器解决歧义损失和训练 Segment Anything 论文地址: https://arxiv.org/abs/2304.02643 代码地址:https://github.com/facebookresear

论文翻译:ICLR-2024 PROVING TEST SET CONTAMINATION IN BLACK BOX LANGUAGE MODELS

PROVING TEST SET CONTAMINATION IN BLACK BOX LANGUAGE MODELS https://openreview.net/forum?id=KS8mIvetg2 验证测试集污染在黑盒语言模型中 文章目录 验证测试集污染在黑盒语言模型中摘要1 引言 摘要 大型语言模型是在大量互联网数据上训练的,这引发了人们的担忧和猜测,即它们可能已

PDF 软件如何帮助您编辑、转换和保护文件。

如何找到最好的 PDF 编辑器。 无论您是在为您的企业寻找更高效的 PDF 解决方案,还是尝试组织和编辑主文档,PDF 编辑器都可以在一个地方提供您需要的所有工具。市面上有很多 PDF 编辑器 — 在决定哪个最适合您时,请考虑这些因素。 1. 确定您的 PDF 文档软件需求。 不同的 PDF 文档软件程序可以具有不同的功能,因此在决定哪个是最适合您的 PDF 软件之前,请花点时间评估您的

OmniGlue论文详解(特征匹配)

OmniGlue论文详解(特征匹配) 摘要1. 引言2. 相关工作2.1. 广义局部特征匹配2.2. 稀疏可学习匹配2.3. 半稠密可学习匹配2.4. 与其他图像表示匹配 3. OmniGlue3.1. 模型概述3.2. OmniGlue 细节3.2.1. 特征提取3.2.2. 利用DINOv2构建图形。3.2.3. 信息传播与新的指导3.2.4. 匹配层和损失函数3.2.5. 与Super

BERT 论文逐段精读【论文精读】

BERT: 近 3 年 NLP 最火 CV: 大数据集上的训练好的 NN 模型,提升 CV 任务的性能 —— ImageNet 的 CNN 模型 NLP: BERT 简化了 NLP 任务的训练,提升了 NLP 任务的性能 BERT 如何站在巨人的肩膀上的?使用了哪些 NLP 已有的技术和思想?哪些是 BERT 的创新? 1标题 + 作者 BERT: Pre-trainin

【经验交流】修复系统事件查看器启动不能时出现的4201错误

方法1,取得『%SystemRoot%\LogFiles』文件夹和『%SystemRoot%\System32\wbem』文件夹的权限(包括这两个文件夹的所有子文件夹的权限),简单点说,就是使你当前的帐户拥有这两个文件夹以及它们的子文件夹的绝对控制权限。这是最简单的方法,不少老外说,这样一弄,倒是解决了问题。不过对我的系统,没用; 方法2,以不带网络的安全模式启动,运行命令行,输入“ne

[论文笔记]LLM.int8(): 8-bit Matrix Multiplication for Transformers at Scale

引言 今天带来第一篇量化论文LLM.int8(): 8-bit Matrix Multiplication for Transformers at Scale笔记。 为了简单,下文中以翻译的口吻记录,比如替换"作者"为"我们"。 大语言模型已被广泛采用,但推理时需要大量的GPU内存。我们开发了一种Int8矩阵乘法的过程,用于Transformer中的前馈和注意力投影层,这可以将推理所需

【微服务】Ribbon(负载均衡,服务调用)+ OpenFeign(服务发现,远程调用)【详解】

文章目录 1.Ribbon(负载均衡,服务调用)1.1问题引出1.2 Ribbon负载均衡1.3 RestTemplate整合Ribbon1.4 指定Ribbon负载均衡策略1.4.1 配置文件1.4.2 配置类1.4.3 定义Ribbon客户端配置1.4.4 自定义负载均衡策略 2.OpenFeign面向接口的服务调用(服务发现,远程调用)2.1 OpenFeign的使用2.1 .1创建