3 ms·

Can someone explain why proving and math problem solving is not a far easier problem for computers? Why does it require any “artificial intelligence” at all? F

by lumb63 2y ago

Can someone explain why proving and math problem solving is not a far easier problem for computers? Why does it require any “artificial intelligence” at all? For example, suppose a computer is asked to prove the sum of two even numbers is an even number. It could pull up its list of “things it knows about even numbers”, namely that an even number modulo 2 is 0. Assuming the first number is “a” and the second is “b”, then it knows a=2x and b=2y for some x and y. It then knows via the distributive property that the sum is 2(x+y), which satisfies the definition of an even number. What am I missing that makes this problem so much harder than applying a finite and known set of axioms and manipulations?

zone411 2y ago
The problems in question require much, much more complex proofs. Try example IMO problems yourself and see if they don't require much intelligence: https://artofproblemsolving.com/wiki/index.php/IMO_Problems_and_Solutions https://artofproblemsolving.com/wiki/index.php/IMO_Problems_.... And then keep in mind that research math is orders of magnitude more complex still.
runeblaze 2y ago
Another answer is that 3SAT and co can be seen as distilled variants of proving statements. Well, 3SAT is famously hard.
psb217 2y ago
In a sense, the model _is_ simply applying a finite and known set of axioms and manipulations. What makes this hard in practice is that the number of possible ways in which to perform multiple steps of this sort of axiomatic reasoning grows exponentially with the length of the shortest possible solution for a given problem. This is similar to the way in which the tree of possible futures in games like go/chess grows exponentially as one tries to plan further into the future. This makes it natural address these problems using similar techniques, which is what this research team did. The "magic" in their solution is the use of neural nets to make good guesses about which branches of these massive search trees to explore, and make good guesses about how good any particular branch is even before they reach the end of the branch. These tricks let them (massively) reduce the effective branching factor and depth of the search trees required to produce solutions to math problems or win board games.
ComplexSystems 2y ago
What you're missing is that this kind of thing has arbitrarily been declared "artificial intelligence" territory. Once the ability of computers to do has been established, it will no longer be artificial intelligence territory; at that point it'll just be another algorithm.
booleandilemma 2y ago
Proofs require a certain ingenuity that computers just don't have, imo. A computer would never be able to come up with something like Cantor's diagonalization proof on its own.
- Davidzheng 2y ago
  Are you sure alphaproof can't

by lumb63 2y ago

zone411 2y ago

The problems in question require much, much more complex proofs. Try example IMO problems yourself and see if they don't require much intelligence: https://artofproblemsolving.com/wiki/index.php/IMO_Problems_and_Solutions https://artofproblemsolving.com/wiki/index.php/IMO_Problems_.... And then keep in mind that research math is orders of magnitude more complex still.

runeblaze 2y ago

Another answer is that 3SAT and co can be seen as distilled variants of proving statements. Well, 3SAT is famously hard.

psb217 2y ago

In a sense, the model _is_ simply applying a finite and known set of axioms and manipulations. What makes this hard in practice is that the number of possible ways in which to perform multiple steps of this sort of axiomatic reasoning grows exponentially with the length of the shortest possible solution for a given problem. This is similar to the way in which the tree of possible futures in games like go/chess grows exponentially as one tries to plan further into the future. This makes it natural address these problems using similar techniques, which is what this research team did. The "magic" in their solution is the use of neural nets to make good guesses about which branches of these massive search trees to explore, and make good guesses about how good any particular branch is even before they reach the end of the branch. These tricks let them (massively) reduce the effective branching factor and depth of the search trees required to produce solutions to math problems or win board games.

ComplexSystems 2y ago

What you're missing is that this kind of thing has arbitrarily been declared "artificial intelligence" territory. Once the ability of computers to do has been established, it will no longer be artificial intelligence territory; at that point it'll just be another algorithm.

booleandilemma 2y ago

Proofs require a certain ingenuity that computers just don't have, imo. A computer would never be able to come up with something like Cantor's diagonalization proof on its own.

Davidzheng 2y ago
Are you sure alphaproof can't