Yes, currently the problem is open whether or not the Partition Principle and the Axiom of Choice are equivalent. There are two major factors for this (in my opinion):
Many people become less interested in choiceless results. So while they might be very happy to hear about them, they prefer to put their research efforts towards other directions.
The Partition Principle gives us just enough structure on the cardinals so the obvious approaches fail pretty fast; but it also indicates that the failure of the axiom of choice might be far away from the ordinals. In other equivalences we can usually show that if a principle fails somewhere, then it will often fail on something which is "close to the ordinals" in some sense.
This is a vague statement, and I don't intend to clarify on it further. To understand it, feel free to try and apply some of the usual approaches to this problem.
Forcing. Forcing is a great tool for proving consistency results. The "Miller property" which is better described as absoluteness, is not the reason why $L(\Bbb R)$ fails to satisfy the axiom of choice. This is actually not that difficult, once you add "enough" reals which "look the same" you can easily confuse the axiom of choice in a model like $L(x)$ where $x$ is any set including sufficiently many reals.
This was observed by Feferman/Solovay a long time ago. If you add $\omega_1$ Cohen reals to $L$, then $L(\Bbb R)$ fails to satisfy the axiom of choice (but it does satisfy the principle of dependent choice).
But models of the form $L(x)$ will almost usually fail to satisfy the partition principle if the axiom of choice fails. For example there is a definable surjection from $\Bbb R$ onto $\omega_1$; but if there are not $\omega_1$ sequences of reals in $L(x)$ then there is no injection back. Another example is that if there is an infinite Dedekind-finite set, then there is one which can be mapped onto $\omega$, but by definition there will be no injection in the other direction.
And this is true in many of these constructions of inner models of generic extensions. We will usually be able to single out that the set we are interested in has this sort of property which witnesses the failure of the Partition Principle.
So what about forcing? Forcing works fine without the axiom of choice. But we are so used to thinking about it in terms of the axiom of choice, that it becomes very difficult to use forcing as arbitrarily as we do when choice fails. We lose the ability to talk about chain conditions (because some forcings don't have maximal antichains at all), the mixing lemma can fail, and closure does not imply distributivity.
Then when we force over models where the axiom of choice fails we lose the ability to use these tools, and again we can often find examples which are either very hard to understand (so we don't know much about them yet), or witness the catastrophes which may befall on us (we may add unintentional real numbers in the process, and so on and so forth).
So we can try and appeal to absoluteness, but this will usually work for forcings which are associated with ordinals, forcings which are well-ordered inherently (like collapsing something to $\omega$) or has sufficiently "pretty" structure. Not to mention that if the Principle fails, it can fail in many places, which would require you to work much harder than you would have. There is a reason why so little people throughout history understood Sageev's proof for "For all infinite $a$, $a+a=a$ does not imply the axiom of choice". It's a monumentally difficult proof which is spanned over 180 pages (and that's an edited version of his Ph.D.)
So what can we do? Not much currently. As I wrote in the comment, I find this problem to be a lighthouse in the bogs of mathematics. I think to myself what sort of thing would have helped me to prove such a result. But there is a huge distance from my ideas to implementations, and even when the tools I currently craft will be ready for use, it might still take a long time before I will have any idea on how to apply them properly to this problem.
Question 1: $M^B$ is obtained by taking the whole definition of $V^B$, for complete Boolean algebras $B$ in $V$, and interpreting everything in $M$. It is what $M$ thinks is the $B$-valued universe.
I'd rather not think in terms of $V^B$, as in your suggestion of $V^B\cap M$, because it's not clear what $V^B$ would mean here. The problem is that $B$ is a complete Boolean algebra in the sense of $M$, i.e., its subsets in $M$ have suprema and infima, but it is usually not complete in $V$.
Question 2: The idea that $\check M$ serves as a name for the ground model is justified after the fact, when one proves that, for any name $\dot a$, the interpretation of $\dot a$ with respect to a generic $G$ is in the ground model $M$ iff $\Vert\dot a\in \check M\Vert\in G$.
Similarly, one checks later that the interpretation of $\dot G$ with respect to any generic $G$ is $G$ itself.
You might find it useful to check that the truth value of "$\dot G$ is an $\check M$-generic filter in $\check P$" is $1$.
Best Answer
No; consider for example $\varphi(x$) = "Every other bit of $x$ is $0$." No Cohen-generic real has this property, but if $c$ is Cohen-generic then the "spaced out" version of $c$ $$0,c(0),0,c(1),0,c(2),...$$ is not in $V$ but does satisfy the property $\varphi$.
What is true is that every new real is "equivalent to" a Cohen real in a precise sense: assuming $\mathsf{V=L}$ for simplicity, if $c$ is Cohen over $L$ and $d\in L[c]\setminus L$ then $d\equiv_ce$ for some Cohen real $e\in L[c]$. Here "$\equiv_c$" is the relation of equivalent constructibility degree: we say $x\le_cy$ iff $x\in L[y]$. (If we don't assume $\mathsf{V=L}$ we need to replace $\equiv_c$ with the "mod $V$" analogue.)
This can be seen by looking at the possible factors of the Cohen algebra (I think Jech has a good writeup of the details). Note, however, that there is no $\varphi$ occurring here; this is just a property of newly-added reals.