Is the Witness Size of Membership for Every NP Language Already Known?
If you don't mind artificial languages, we can construct such problems using pretty much any number k whose value is unknown to mathematicians. For example, we don't know the value of R(5,5) (the fifth Ramsey number), or the size of the largest excluded minor of the family of knotless graphs (this number is finite due to the Robertson-Seymour theorem), or the value of BB(10), where BB() stands for the Busy Beaver function. Let k equal any of these numbers. We know that k is finite, but we don't know the value of k.

Now construct some problem in NP where the witness is of size $O(n^k)$. Off the top of my head I can't think of a nice way of doing this, but here's one way. Let the input be a succinct description of a graph. Since the description size is n, the graph is on exponentially many vertices. (For example, maybe the input is a circuit that accepts two inputs x and y and tells you if (x,y) is an edge in the graph.) The question is to determine if the graph contains a path of length $n^k$. This problem is in NP because the prover can send the list of vertices on the path in order, which the verifier can check. The size of the witness is $n^k$.