One of OpenAI’s artificial intelligence models generated a proof that claims to disprove the Exponential Time Hypothesis, a foundational assumption in theoretical computer science, and human verification is underway.
The hypothesis was widely believed to be true — until AI took a look at it.
OpenAI said Monday that its AI found a “natural language disproof” on Oct. 16, and the company formalized the result in Lean on Oct. 17.
People were interested in these podcasts
“Surprisingly, our system has recently proved that the [hypothesis] is false, a result that was subsequently verified in Lean,” OpenAI said in a statement. “The refutation of the ETH reopens questions about how much faster these tasks could become, and may help guide the search for better algorithms.”
The hypothesis is a long-standing guess in computer science that some logic puzzles cannot be solved quickly by any computer program.
In these puzzles, a computer must decide whether a set of true-or-false switches can be set so that every listed condition is met at once. The guess says that each added switch roughly doubles the work, so large versions of the puzzle would take impractically long even with the best possible method.
Researchers have used the hypothesis in hundreds of papers to conclude that many other problems, in fields such as graph theory, databases and computational biology, are also hard to solve quickly. If it is false, some of those problems may have faster solutions than experts assumed, though OpenAI said finding them will take significant further research.
A group led by Russell Impagliazzo and Ramamohan Paturi, two of the original proposers of the hypothesis, and Ryan Williams, another expert in algorithm design and complexity theory, will examine the AI’s work.
“If the claim is correct, it will change an important part of theoretical computer science,” the three said in a dear colleague letter. “[The hypothesis] has helped organize decades of research, connecting problems and sharpening our understanding of computational difficulty. The ideas, reductions, and techniques developed through that work retain their value, even as some of their interpretations may change. There should be room both for excitement about new possibilities and for thoughtful reassessment of directions many of us have pursued for years.”
Mr. Paturi said his first reaction to the claimed refutation of the hypothesis was surprise.
“If it holds up, it would be a major advance in our understanding of the limits of computation,” he said in a statement to The Washington Times.
The research developed around the hypothesis over the past three decades remains valuable, he added, including the connections between problems and the techniques used to study them.
Mr. Paturi said that not participating in “the examination of a claim this important is unthinkable.”
“Examining, questioning, explaining, and building on one another’s work is central to how science advances,” he said.
OpenAI has published the AI-written proof and the Lean formalization and agreed to make all raw data public. The company agreed to commit to funding a conference to “understand the implications of this work on the field as a whole.”
Contact the author
Please read our comment policy before commenting.