Something I didn’t realize until now: P = NP would imply that finding the argmax of arbitrary polynomial time (P-time) functions could be done in P-time.
Proof sketch
Suppose you have some polynomial time function f: N → Q. Since f is P-time, if we feed it an n-bit input x it will output a y with at most max_output_bits(n) bits as output, where max_output_bits(n) is at most polynomial in n. Denote y_max and y_min as the largest and smallest rational numbers encodable in max_output_bits(n) bits.
Now define check(x, y) := f(x) >= y, and argsat(y) := x such that check(x, y) else None. argsat(y) is in FNP, and thus runs in P-time if P = NP. Now we can find argmax(f(x)) by running a binary search over all values y in [y_min, y_max] on the function argsat(y). The binary search will call argsat(y) at most max_output_bits(n) times, and P x P = P.
I’d previously thought of argmax as necessarily exponential time, since something being an optimum is a global property of all evaluations of the function, rather than a local property of one evaluation.
This is a cool fact I hadn’t been aware of. An alternative sketch (it might be nonsense, not being careful):
If P = NP then P = co-NP. The problem of “given x, say yes if x is the argmax of f” is co-NP, because you can polynomially verify “no” answers: a witness is y such that f(y) > f(x). So this is in P, i.e. we can polynomially answer “is this the argmax”. Since we can polynomially verify this, the map from polytime TMs for some f, to argmax, is in FNP. (<- This step is the one I’m slightly unconfident about but seems right.) So this map is in P since FNP = P (presumably).
I think this is spiritually quite similar to your proof, except that the binary search thing isn’t necessary?
Oh, indeed I was getting confused between those. So as a concrete example of your proof we could consider the following degenerate example case
def f(N: int) -> int:
if N == 0x855bdad365f9331421ab4b13737917cf97b5e8d26246a14c9af1adb060f9724a:
return 1
else:
return 0
def check(x: int, y: float) -> bool:
return f(x) >= y
def argsat(y: float, max_search: int = 2**64) -> int or None:
# We postulate that we have this function because P=NP
if y > 1:
return None
elif y <= 0:
return 0
else:
return 0x855bdad365f9331421ab4b13737917cf97b5e8d26246a14c9af1adb060f9724a
but we could also replace our degenerate f with e.g. sha256.
LW feature request/idea: something like Quick Takes, but for questions (Quick Questions?). I often want to ask a quick question or for suggestions/recommendations on something, and it feels more likely I’d get a response if it showed up in a Quick Takes like feed rather than as an ordinary post like Questions currently do.
It doesn’t feel very right to me to post such questions as Quick Takes, since they aren’t “takes”. (I also tried this once, and it got downvoted and no responses.)
Something I didn’t realize until now: P = NP would imply that finding the argmax of arbitrary polynomial time (P-time) functions could be done in P-time.
Proof sketch
Suppose you have some polynomial time function f: N → Q. Since f is P-time, if we feed it an n-bit input x it will output a y with at most max_output_bits(n) bits as output, where max_output_bits(n) is at most polynomial in n. Denote y_max and y_min as the largest and smallest rational numbers encodable in max_output_bits(n) bits.
Now define check(x, y) := f(x) >= y, and argsat(y) := x such that check(x, y) else None. argsat(y) is in FNP, and thus runs in P-time if P = NP. Now we can find argmax(f(x)) by running a binary search over all values y in [y_min, y_max] on the function argsat(y). The binary search will call argsat(y) at most max_output_bits(n) times, and P x P = P.
I’d previously thought of argmax as necessarily exponential time, since something being an optimum is a global property of all evaluations of the function, rather than a local property of one evaluation.
This is a cool fact I hadn’t been aware of. An alternative sketch (it might be nonsense, not being careful):
If P = NP then P = co-NP. The problem of “given x, say yes if x is the argmax of f” is co-NP, because you can polynomially verify “no” answers: a witness is y such that f(y) > f(x). So this is in P, i.e. we can polynomially answer “is this the argmax”. Since we can polynomially verify this, the map from polytime TMs for some f, to argmax, is in FNP. (<- This step is the one I’m slightly unconfident about but seems right.) So this map is in P since FNP = P (presumably).
I think this is spiritually quite similar to your proof, except that the binary search thing isn’t necessary?
Finding the input
xsuch thatf(x) == argmax(f(x))is left as an exercise for the reader though.I think you’re mixing up max with argmax?
Oh, indeed I was getting confused between those. So as a concrete example of your proof we could consider the following degenerate example case
but we could also replace our degenerate
fwith e.g.sha256.Is that the gist of your proof sketch?
LW feature request/idea: something like Quick Takes, but for questions (Quick Questions?). I often want to ask a quick question or for suggestions/recommendations on something, and it feels more likely I’d get a response if it showed up in a Quick Takes like feed rather than as an ordinary post like Questions currently do.
It doesn’t feel very right to me to post such questions as Quick Takes, since they aren’t “takes”. (I also tried this once, and it got downvoted and no responses.)
I’m looking for recommendations for frameworks/tools/setups that could facilitate machine checked math manipulations.
More details:
My current use case is to show that an optimized reshuffling of a big matrix computation is equivalent to the original unoptimized expression
Need to be able to index submatrices of an arbitrary sized matrices
I tried doing the manipulations with some CASes (SymPy and Mathematica), which didn’t work at all
IIUC the main reason they didn’t work is that they couldn’t handle the indexing thing
I have very little experience with proof assistants, and am not willing/able to put the effort into becoming fluent with them
The equivalence proof doesn’t need to be a readable by me if e.g. an AI can cook up a complicated equivalence proof
So long as I can trust that it didn’t cheat e.g. by sneaking in extra assumptions