3 ms·
> As soon as you need reliable outcomes, such as certainty whether an erroneous state can arise in a program, whether a proof for a mathematical conjecture exis
by skissane 4y ago
> As soon as you need reliable outcomes, such as certainty whether an erroneous state can arise in a program, whether a proof for a mathematical conjecture exists, or whether a counterexample exists, exhaustive search is often necessary.
Proof checking requires 100% reliability. But if you are searching the space of all possible proofs for a valid one, that process does not require 100% reliability. On the contrary, automated theorem provers rely on heuristics to guide their exploration of that space, none of which work 100% of the time. "Exhaustive search" is an infeasible strategy, because the search space is just too large. Finding proofs is the really hard part (NP-hard), and the part which most stands to benefit from "AI" techniques – checking their validity is a lot easier (polynomial time).
"New AI" deep-learning techniques can be used to augment automated theorem provers, by giving them guidance on which areas of the search space to target – see for example https://arxiv.org/abs/1701.06972 https://arxiv.org/abs/1701.06972 – that produced a seemingly modest improvement (3 percentage points) – but keep in mind how hard the problem is, a 3 percentage point improvement on a very hard problem can actually be a big deal – plus I don't know if any more recent research has improved on that.
- _carbyau_ 4y agoThe idea of chainlinking "AI to guide/choose AI for the next step" is where I expect more impressive results in future. It will be important to understand the limitations of AI to be sure of proper placement.
- versteegen 4y agoFinding a proof of a mathematical conjecture is much harder than NP-hard, it's undecidable (the Entscheidungsproblem) because the search space is infinite (and worse, doesn't necessarily include a proof even if the statement is true - Gödel's first incompleteness thm). So even if we restrict to conjectures that are actually machine-provable, it's still much harder than NP decision problems which are combinatorial so have an exponentially growing search space.
- ogogmad 4y agoRemark: Deciding if a proof of a proposition exists* up to a certain length n is NP-COMPLETE. Deciding if a proof exists at all - which is the Entscheidungsproblem - is semi-decidable. So the parent wasn't entirely wrong. * - In Peano arithmetic, let's say
- andrepd 4y ago> Finding proofs is the really hard part (NP-hard), and the part which most stands to benefit from "AI" techniques – checking their validity is a lot easier (polynomial time). Note that this is true only for boolean logic and equivalents. Anything stronger has either much higher complexity or is simply undecidable (but proof checking is fast, which is the main point).