Update. Here is a more direct construction. (See edit history for previous version.)
There is such a universal computable group as you request. Let $F$
be the free group on infinitely many generators $\langle
a_p\rangle_p$, indexed by the Turing machine programs $p$. Let $G$
be the quotient of this group by all the $k^{th}$ powers $a_p^k$, whenever the program $p$
halts (on trivial input) in exactly $k$ steps.
Let us represent the group $G$ by reduced words in the generators
$a_p$ and their inverses, but in the case that we took the quotient
by $a_p^k$, then in these words we use exponents on $a_p$ in the interval
$(-k/2,k/2]$. (The reason for using this exponent format is that if we were to use only the positive powers of the finite-order generators, then we wouldn't be able to compute inverses in $G$, since we cannot compute whether $a_p$ has finite order or not.) First of all, we can computably recognize whether a
word in the generators fits this description, simply by checking
whether it is reduced and whether any of the exponents is too
large. The point of this last issue is that we can tell if the
exponent $a_p^r$ is too large by checking if program $p$ halts in
$2r$ steps or not. Similarly, we can easily compute the inverse of
a word from the word, and we can computably multiply words. Again,
whenever we have a word with some new exponents on the generators,
we need to check whether they reduce because of our quotient, and
this is possible by running the relevant computation for sufficient
number to steps to determine it.
Thus, we have a computable representation of the group $G$.
Finally, I claim that it is universal in the sense you requested.
Given any Turing machine program $p$, let $x_p=a_p$ and let
$y_p=a_q$ for some other program $q$ known not to halt. Thus, by
design, the group generated by $x_p,y_p$ will be the free group on
these generators if and only if $p$ does not halt.
An essentially equivalent presentation of the group can be made without reference to Turing machines or computations, but only to Diophantine equations, simply by using the Diophantine representation of the universal Turing machine. That is, since every c.e. set is the solution set of a Diophantine equation, there is a fixed Diophantine equation $d(y,\vec x)=0$, such that Turing machine program $p$ halts on trivial input if and only if $d(p,\vec x)=0$ has a solution in the integers, viewing the program as its Gödel code. So we may define the group $G$ as above, with infinitely many generators $a_n$, but taking the quotient by $a_n^k$, if $k$ is the size of the smallest integer solution of $d(n,\vec x)=0$. I'm not sure this makes the group "natural," (and my opinion is that this word has no robust, coherent mathematical meaning), but it does omit any mention of Turing machines, using instead a fixed Diophantine equation.
Lastly, let me observe that my group is not finitely generated, and
it may be interesting to have a finitely generated example, or even
a finitely presented example. I suspect that one can apply one of the embedding theorems to place this example into a finitely generated or even finitely presented group.
The first thing to notice is that if ZF is consistent, then it is
consistent with ZFC that what you call ProveLoop is actually decidable. The
reason is that if ZF is consistent, then by the incompleteness
theorem, it is consistent with ZFC that $\neg$Con(ZF), in which case everything is provable in
ZF, in which case every program is in ProveLoop.
So in the proof that ProveLoop is undecidable, one needs to make
an additional assumption about the reliability of the proofs in ZF to
avoid this issue with the incompleteness theorem.
Meanwhile, under such a consistency assumption, ProveLoop is indeed
equivalent to the halting problem.
Theorem. Assume Con(ZF). Then ProveLoop is Turing
equivalent to the Halting problem.
Proof. Under the Con(ZF) assumption, it follows that whenever ZF proves that a program doesn't halt, then it really doesn't halt, since if it did halt, then this fact would also be provable, contrary to consistency.
Clearly ProveLoop is c.e. and hence reducible to the
halting problem, as you pointed out. Conversely, let's reduce the
halting problem to ProveLoop. Given any program $p$, we want to
decide whether $p$ halts on a blank tape, using an oracle for
ProveLoop.
Define a computable function $f$, so that $f(q)$ is the program
such that, on trivial input, if $p$ halts on the blank tape, then
$f(q)$ jumps into an immediate infinite loop, and otherwise, while waiting for $p$ to halt, the program $f(q)$ halts just in case it finds a proof that $q$ does not halt.
By the recursion theorem, there is a program $r$ such that $r$ and
$f(r)$ compute the same function, and we can find this $r$
effectively. Furthermore, by using the $r$ from the proof of the recursion theorem, we may also assume that ZF proves that $r$ and $f(r)$ compute the same function. Notice that it can't ever be that $r$ halts on account of finding a proof that $r$ does not halt, by our assumption which ensures the accuracy of proofs of non-halting, and so definitely $r$ does not halt in any case. Meanwhile, if $p$ halts, then $r$ does not halt, but for a trivial reason that will be provable in ZF, namely, the fact that $p$ halted; and otherwise, when $p$ does not halt, then $r$ will run forever, but this fact will not be provable (for if it were provable, then $r$ would halt, contrary to consequence of our assumption that such proofs are reliable). So what we have is exactly a reduction of the halting problem to ProveLoop, as desired. QED
Best Answer
The mortality problem for $3\times 3$ matrices: given a finite set $F$ of $3\times 3$ integer matrices, decide whether the zero matrix is a product of members of $F$ (with repetitions allowed). This was proved unsolvable by Michael Paterson, Studies in Applied Mathematics 49 (1970), 105--107, doi: 10.1002/sapm1970491105.
The corresponding problem for $2\times 2$ matrices is apparently still open.
Edit (11 September 2016): The problem for $2\times 2$ matrices is apparently still open, despite the solution of a seemingly similar problem mentioned in Igor Potapov's answer below.