不确定性的困惑与NP理论分享 http://blog.sciencenet.cn/u/liuyu2205 平常心是道

博文

译文:计算机是否准备好了解决这个棘手的数学问题?- 考拉兹猜想(Collatz conjecture)

已有 3032 次阅读 2022-4-29 06:03 |个人分类:解读哥德尔不完全性定理|系统分类:科研笔记

计算机是否准备好了解决这个棘手的数学问题?- Siobhan Robert


据说,考拉兹猜想(Collatz conjecture)是由德国数学家考拉兹(Lothar Collatz)在20世纪30年代首次提出的,它提供了一个生成数列的方法或算法:给定一个正整数,如果是偶数,则将其除以 2;如果是奇数,则将其乘以3再加1;然后不断重复。该猜想断言,此数列将以1结束(然后在421之间循环)。

例如,5 产生一个 6 项的数列:

5, 16, 8, 4, 2, 1


27 产生一个 111 项的数列,在到达 1 之前上下波动,最大值达到 9232


40产生一个简短的数列:

40, 20, 10, 5, 16, 8, 4, 2, 1

到目前为止,从1到接近3000亿亿的正整数已被计算机验证最终达到了1

大多数研究者认为考拉兹猜想是真的,它吸引了众多的数学家和非数学家,但没有人能提出证明。20世纪80年代初,匈牙利数学家Paul Erdős宣称,数学还没有准备好解决这样的问题


"他可能是对的,"Heule说。对Heule来说,考拉兹猜想的诱惑力并不在于实现突破,而在于推动自动推理技术的发展。在与考拉兹猜想缠斗了五年之后,Heule和他的合作者Scott AaronsonEmre Yolcu最近在arXiv预印平台上发表了一篇论文,他们在论文中写道:尽管我们没能成功证明考拉兹猜想,但我们认为,本文的观点提供了一种有趣的新方法。


这是一个高贵的失败 德克萨斯大学奥斯汀分校的计算机科学家Aaronson说,说它失败,是因为他们没能成功证明这个猜想,说它高贵,是因为他们在另一种意义上取得了进展。Heule认为,这是确定人类还是计算机更擅长证明此类问题的一个起点。

把数学译为计算


对于许多数学问题,计算机是没有希望的,因为它们没有机会接触到历史上积累的大量数学作品。但有时计算机在人类无望的地方表现出色,告诉计算机问题答案是什么样子的给它一个目标和一个定义明确的搜索空间然后通过蛮力搜索,计算机可能会找到答案。虽然计算结果是否相当于对数学经典的有意义的补充是一个争论的问题。传统的观点是,只有人类的创造力和直觉,通过概念和想法,才能扩展数学的范围,而通过计算取得的进展往往被视为工程。

从某种意义上说,计算机和Collatz猜想是完美的搭配。首先,正如卡内基梅隆大学的逻辑学家和哲学教授Jeremy Avigad所指出的那样,迭代算法的概念是计算机科学的基础—Collatz数列正是迭代算法的一个例子,根据确定的规则一步步进行。同样,显示一个过程的终止是计算机科学中的一个常见问题。Avigad说:计算机科学家通常想知道他们的算法是否终止,也就是说,返回一个答案Heule和他的合作者正在利用这一技术来解决Collatz猜想,这实际上只是一个终止问题。

Heule的专长是使用一种叫做 "SAT求解器 "的计算工具--或者说是可满足性求解器,这是一种计算机程序,用于确定在一组约束条件下是否存在一个公式或问题的解决方案。但关键是,在数学挑战的情况下,SAT求解器首先需要将问题翻译成或表示成计算机能够理解的术语。正如Heule的博士生Yolcu所说,表述很重要,非常重要


机会渺茫,但值得一试


Heule第一次提到用SAT求解器来解决Collatz问题时,Aaronson想,这根本不可能成功,但是他很快就相信这是值得一试的,因为Heule看到了改变这个老问题的微妙方法,这可能会使它变得灵活起来。他注意到有一个计算机科学家团体正在使用SAT求解器成功地为一种被称为重写系统的抽象计算表示法找到终止证明。这是个漫长的过程,但他向Aaronson建议,将Collatz猜想转化为一个重写系统可能会使Collatz的终止证明成为可能(Aaronson以前曾帮助将黎曼假设转化为一个计算系统,将其编码在一个小型图灵机中)。那天晚上,Aaronson设计了这个系统。 他说:这就像一个家庭作业,一个有趣的练习

Aaronson的系统用11条规则抓住了Collatz问题。如果研究者以任何顺序应用这11条规则,能够得到这个类似系统的终止证明,这将证明Collatz猜想是真的。


Heule尝试用最先进的工具来证明重写系统的终止,但没有成功虽然这是意料之中的事情,但也令人失望。Heule说: “这些工具是针对可以在一分钟内解决的问题而优化的,而解决Collatz的任何方法都可能需要几天甚至几年的计算。这激励Heule他们进一步打磨计算方法,并运用他们自己的工具来把Collatz猜想转换为 SAT 问题。


Aaronson认为,只要去掉11条规则中的一条,就能留下一个类似Collatz”的系统,解决这个系统要容易得多,这是对更大目标的试金石。他提出了一个人机对战的挑战:第一个用10条规则解决所有子系统的人获胜。Aaronson手动,HeuleSAT求解器:他将系统编码为一个可满足性问题用另一个巧妙的表示层,将系统翻译成计算机语言中的变量,这些变量可以是01,然后让他的SAT求解器在内核上运行,寻找终止的证据。


他俩都成功证明该系统按照 10 条规则的可变集具有终止性。有时,这对人和程序来说都是一项微不足道的工作。Heule的自动化方法最多花费24小时。Aaronson的纯人工方式需要大量的脑力劳动,需要几个小时甚至一天的时间一套10条规则他从未成功证明,尽管他坚信他可以通过更多努力来证明。Aaronson说: “从字面上看,我是在和一个终结者作战, 至少是一个终止定理证明者。


此后,YolcuSAT求解器进行了微调,校准了该工具以更好地适应Collatz问题的性质。这些技巧使一切都变得不同,加快了10条规则子系统的终止证明,并将运行时间减少到秒级。

Aaronson表示:剩下的最主要的问题是,11 条规则的完整集怎么处理?如果试着用这个系统跑 11 条规则,那它会无休止地跑下去。我们或许不该对此表示震惊,毕竟这是Collatz问题。

Heule看来,自动化推理的大多数研究对需要大量计算的问题视而不见。但基于他之前的突破,他相信这些问题是可以解决的。其他人已经把Collatz改造成了一个重写系统,但是,只有配合极强的算力大规模运用经过微调的 SAT 求解器才有可能求得证明。

到目前为止,Heule使用了大约5000个内核(为计算机提供动力的处理单元;消费者计算机有48个内核)来运行Collatz调查。作为一名亚马逊学者,他得到了亚马逊网络服务的公开邀请,可以使用实际上是无限的资源多达一百万个内核。但他不愿意使用明显更多的资源。

他说: “我希望有一些迹象表明,这是一个现实的尝试。否则,Heule觉得他是在浪费资源和信任, “我不需要100%的信心,但我真的希望有一些证据表明有一个合理的机会,它将会成功

促成转变


"密歇根大学的数学家Jeffrey Lagarias说: »这种自动化方法的好处是,你可以打开电脑,然后等待。他研究Collatz猜想大约50年了,并成为知识的守护者,汇编了注释书目,并编辑了一本关于这个主题的书,终极挑战。对于Lagarias来说,自动化方法让他想起了普林斯顿数学家John Horton Conway2013年发表的一篇论文,他认为Collatz问题可能属于一类难以捉摸的问题,即真实且不可判定,但同时又不能证明为不可判定,正如Conway所指出的,“……甚至可能是它们不可证明的断言本身也不可证明,以此循环往复。 ”

Lagarias表示:如果 Conway是对的,那不管自动化的方法还是手动,Collatz猜想都是无法证明的,并且我们永远不会知道确切的答案。


可以说,最接近的人是加州大学洛杉矶分校的数学家Terence Tao。在2019年,陶氏证明了Collatz猜想对于几乎所有的数都几乎真实的(几乎依赖于两个不同的技术定义,但还是根据普通的英语含义)。

陶氏认为,人类对Collatz猜想的证明将比计算机证明更有数学意义了解它的原因。他说:但是,让一个重大的未解决的问题落到一个自动验证器上,可能会给数学家在工作中使用计算机辅助的方式带来革命性的转变。对于这样一个难以解决的问题,我们将采取任何我们能得到的见解。 ”

然而,Heule和他的合作者真正追求的是这样一种情况使用这种方法,解决这个问题计算机在人类失败的地方取得成功,或者反之亦然,在这一点上,我们不知道这些技术是否比人类的手工操作强得多,或者人类是否能做计算机不能做的事情Heule说,我们想知道的是,人类或计算机在解决此类问题方面谁更胜一筹。 ”

为此,让我们看看谁先解决了Collatz 猜想。

原文:

https://www.technologyreview.com/2021/07/02/1027475/computers-ready-solve-this-notorious-math-problem/

Are computers ready to solve this notoriously unwieldy math problem?

By Siobhan Roberts
July 2, 2021



First proposed (according to some accounts) in the 1930s by the German mathematician Lothar Collatz, this number theory problem provides a recipe, or algorithm, for generating a numerical sequence: Start with any positive integer. If the number is even, divide by two. If the number is odd, multiply by three and add one. And then do the same, again and again. The conjecture asserts that the sequence will always end up at 1 (and then continually cycle through 4, 2, 1).

The number 5, for instance, generates only six terms:

5, 16, 8, 4, 2, 1

The number 27 cycles through 111 terms, oscillating up and down—at its height reaching 9,232—before eventually landing at 1.

The number 40 generates another brief sequence

40, 20, 10, 5, 16, 8, 4, 2, 1

To date, the conjecture has been checked by computer for all starting values up to nearly 300 billion billion and every number eventually reaches 1.

Most researchers believe the conjecture is true. It has enticed multitudes of mathematicians and non-mathematicians alike, but nobody has produced a proof. In the early 1980s, the Hungarian mathematician Paul Erdős declared: “Mathematics is not yet ready for such problems.”

“And he’s probably right,” says Heule. For Heule, Collatz’s allure isn’t so much the prospect of a breakthrough as it is advancing automated reasoning techniques. After tinkering with it for five years, Heule and his collaborators, Scott Aaronson and Emre Yolcu, recently posted a paper on the arXiv preprint server. “Although we do not succeed in proving the Collatz conjecture,” they write, “we believe that the ideas here represent an interesting new approach.”


“It’s a noble failure,” says Aaronson, a computer scientist at the University of Texas at Austin. A failure because they didn’t prove the conjecture. Noble because they made progress in another sense: Heule views it as a starting point in determining whether humans or computers are better at proving such problems.

For many math problems, computers are hopeless, since they don’t have access to the vast oeuvre of mathematics amassed through history. But sometimes computers excel where humans are hopeless. Tell a computer what a solution looks like—give it a target and a well-defined search space—and then with brute force the computer might find it. Though it’s a matter of debate whether computational results amount to meaningful additions to the mathematical canon. The traditional view is that only human creativity and intuition, via concepts and ideas, extend the reach of mathematics, whereas advancements via computing are often dismissed as engineering.

In a sense, the computer and the Collatz conjecture are a perfect match. For one, as Jeremy Avigad, a logician and professor of philosophy at Carnegie Mellon notes, the notion of an iterative algorithm is at the foundation of computer science—and Collatz sequences are an example of an iterative algorithm, proceeding step-by-step according to a deterministic rule. Similarly, showing that a process terminates is a common problem in computer science. “Computer scientists generally want to know that their algorithms terminate, which is to say, that they always return an answer,” Avigad says. Heule and his collaborators are leveraging that technology in tackling the Collatz conjecture, which is really just a termination problem.


Heule’s expertise is with a computational tool called a “SAT solver”—or a “satisfiability” solver, a computer program that determines whether there is a solution for a formula or problem given a set of constraints. Though crucially, in the case of a mathematical challenge, a SAT solver first needs the problem translated, or represented, in terms that the computer understands. And as Yolcu, a PhD student with Heule, puts it: “Representation matters, a lot.”


A longshot, but worth a try


When Heule first mentioned tackling Collatz with a SAT solver, Aaronson thought, “There is no way in hell this is going to work.” But he was easily convinced it was worth a try, since Heule saw subtle ways to transform this old problem that might make it pliable. He’d noticed that a community of computer scientists were using SAT solvers to successfully find termination proofs for an abstract representation of computation called a “rewrite system.” It was a longshot, but he suggested to Aaronson that transforming the Collatz conjecture into a rewrite system might make it possible to get a termination proof for Collatz (Aaronson had previously helped transform the Riemann hypothesis into a computational system, encoding it in a small Turing machine). That evening, Aaronson designed the system. “It was like a homework assignment, a fun exercise,” he says.

Aaronson’s system captured the Collatz problem with 11 rules. If the researchers could get a termination proof for this analogous system, applying those 11 rules in any order, that would prove the Collatz conjecture true.


Heule tried with state-of-the-art tools for proving the termination of rewrite systems, which didn’t work—it was disappointing if not so surprising. “These tools are optimized for problems that can be solved in a minute, while any approach to solve Collatz likely requires days if not years of computation,” says Heule. This provided motivation to hone their approach and implement their own tools to transform the rewrite problem into a SAT problem.


Aaronson figured it would be much easier to solve the system minus one of the 11 rules—leaving a “Collatz-like” system, a litmus test for the larger goal. He issued a human-versus-computer challenge: The first to solve all subsystems with 10 rules wins. Aaronson tried by hand. Heule tried by SAT solver: He encoded the system as a satisfiability problem—with yet another clever layer of representation, translating the system into the computer’s lingo of variables that can be either 0s and 1s—and then let his SAT solver run on the cores, searching for evidence of termination.


They both succeeded in proving that the system terminates with the various sets of 10 rules. Sometimes it was a trivial undertaking, for both the human and the program. Heule’s automated approach took at most 24 hours. Aaronson’s approach required significant intellectual effort, taking a few hours or even a day—one set of 10 rules he never managed to prove, though he firmly believes he could have, with more effort. “In a very literal sense I was battling a Terminator,” Aaronson says—“at least a termination theorem prover.”


Yolcu has since fine-tuned the SAT solver, calibrating the tool to better fit the nature of the Collatz problem. These tricks made all the difference—speeding up the termination proofs for the 10-rule subsystems and reducing runtimes to mere seconds.

“The main question that remains,” says Aaronson, “is, What about the full set of 11? You try running the system on the full set and it just runs forever, which maybe shouldn’t shock us, because that is the Collatz problem.”

As Heule sees it, most research in automated reasoning has a blind eye for problems that require lots of computation. But based on his previous breakthroughs he believes these problems can be solved. Others have transformed Collatz as a rewrite system, but it’s the strategy of wielding a fine-tuned SAT solver at scale with formidable compute power that might gain traction toward a proof.

So far, Heule has run the Collatz investigation using about 5,000 cores (the processing units powering computers; consumer computers have four or eight cores). As an Amazon Scholar, he has an open invitation from Amazon Web Services to access “practically unlimited” resources—as many as one million cores. But he’s reluctant to use significantly more.

“I want some indication that this is a realistic attempt,” he says. Otherwise, Heule feels he’d be wasting resources and trust. “I don't need 100% confidence, but I really would like to have some evidence that there’s a reasonable chance that it’s going to succeed.”

Supercharging a transformation


“The beauty of this automated method is that you can turn on the computer, and wait,” says the mathematician Jeffrey Lagarias, of the University of Michigan. He’s toyed with Collatz for about fifty years and become keeper of the knowledge, compiling annotated bibliographies and editing a book on the subject, “The Ultimate Challenge.” For Lagarias, the automated approach brought to mind a 2013 paper by the Princeton mathematician John Horton Conway, who mused that the Collatz problem might be among an elusive class of problems that are true and “undecidable”—but at once not provably undecidable. As Conway noted: “… it might even be that the assertion that they are not provable is not itself provable, and so on.”

“If Conway is right,” Lagarias says, “there will be no proof, automated or not, and we will never know the answer.”


The human who’s arguably come closest is the mathematician Terence Tao, at the University of California, Los Angeles. In 2019 Tao proved the Collatz conjecture is “almost” true for “almost” all numbers (“almost” relies on two different technical definitions, nonetheless according with the plain English meaning).

Tao believes a human proof of the conjecture would be more mathematically meaningful—getting at the why of it— than a computer proof. “But having a major unsolved problem fall to an automated prover could supercharge a revolutionary transformation in how mathematicians use computer assistance in their work,” he says. “With a problem as intractable as this, we will take whatever insights we can get.”

What Heule and his collaborators are really after, however, is a scenario such that—using this approach, with this problem—the computer succeeds where the human fails, or vice versa. “At this point, we don’t know whether these techniques are much stronger than what humans can do by hand or not, or whether humans can do things that the computer can’t do,” Heule says.  “What we want to know is whether humans or computers are better at solving such problems.”

To that end, let’s see who solves the Collatz conjecture first.




https://wap.sciencenet.cn/blog-2322490-1336124.html

上一篇:参访第戎古城 - 林风眠来法国之初的求学之地
下一篇:重读哥德尔1931年论文的第一章 - 什么是“不可判定问题”?
收藏 IP: 88.125.78.*| 热度|

3 刘钢 尤明庆 杨正瓴

该博文允许注册用户评论 请点击登录 评论 (0 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-3-29 21:29

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部