Anyway, I will try to check if working witn large enough $\alpha$ suffices to follow the proof of Halpern and Lévy.

Thanks again, Asaf! I had never seen class names, and so I have a doubt. Does the class name $f$ really define a class in $N$? If the generic ultrafilter would be available in $N$ the answer would be clearly yes. For instance, we can assign an ordinal rank to each name, and restrict $f$ to a set name $f_\alpha$ defined for names in $D$ of rank $\leq \alpha$. Then the sequence $\{f_\alpha\}_{\alpha\in ON^M}$ is definable in $M$ and each $(f_\alpha)_G\in N$, but, is the map $\alpha\mapsto (f_\alpha)_G$ definable in $N$? I cannot see this.

Thank you very much! I will think carefully about all you have said. I did not pretend to avoid the Halpern-Lauchli lemma, but just the specific way Halpern and Lévy describe the sets of $N$.

Maybe I don't understand what you are suggesting. A negative answer would require a model of ZF + UT in which there is a translation invariant measure. A model with an ultrafilter but no Vitali set would not allow us to conclude. And if we could prove that there is no such model, this would mean that UT implies the existence of a Vitali set. I have no idea about how this could be proved. I think that a positive answer would consist of generalizing some proof of the existence of a non Lebesgue measurable set from UT in the same way than Vitali's argument can be generalizec.

I have added the $\sigma$-finite hypothesis to the question.

Yes, I am thinking of $\sigma$-finite measures. A translation invariant $\sigma$-finite measure defined on $\mathcal P\mathbb R$ for which $[0,1]$ has measure $1$ would extend Lebesgue measure. Assuming the consistency of a measurable cardinal, it is consistent with AC the existence of an extension of Lebesgue measure to $\mathcal P\mathbb R$. AC implies that such extension cannot be translation invariant (by the Vitali argument). I am asking whether the ultrafilter theorem suffices.