You didn't specify exactly what "claimed benefits" for non-univalent type theory in general you're referring to, and I happen to believe that even non-univalent type theory does have substantial benefits for the formalization of mathematics. So let me start by recapping those, not to defend type theory in general, but because some of the benefits of univalent type theory expand on them.
One of these benefits is explained eloquently by Andrej Bauer in his answer to the question linked by LSpice in the comments: namely, since mathematics as it is done by mathematicians is essentially typed, and type theory has much more robust error-detection, whether or not the foundational kernel of your proof assistant is type theory, the vernacular that you actually use will almost inevitably be a form of type theory; and in that case why bother putting a layer of set theory under it?
Another benefit of a type-theoretic proof assistant is that type theory has many models, so that a proof formalized in (constructive) type theory actually proves much more than an analogous proof formalized in ZFC. This is where things like categories, sheaves, and so on generally enter the picture, but the basic point can be appreciated without any of those words. For example, instead of interpreting "type" as "set", one can additionally interpret "type" as "topological space", and the same theorems and proofs will be valid. (Technically, he textbook definition of "topological space" isn't quite nice enough for this to be precisely true, but there are well-known modifications of it that are.) Thus, when you prove something in type theory, you haven't just proven the theorem about sets that you would have proven in the analogous ZFC proof, but you've also proven a theorem about topological spaces at the same time. For instance, your theorem about groups is automatically also a theorem about topological groups. My paper The logic of space is an introduction to type theory (including univalence) from this perspective.
So what about univalent type theory? Like non-univalent type theory, it also has many models. Roughly speaking, every model of univalent type theory is an "extension" of some model of non-univalent type theory, and most interesting models of non-univalent type theory can be extended to some model of univalent type theory. But the two classes of models are not equivalent, because a given non-univalent model could be extended to more than one univalent model, and often we may want to access univalent features that depend on the choice of model. To be sure, the difference lies entirely in the world of homotopy theory / higher category theory, so this is not presently a feature that's of much relevance to mathematicians who don't yet care about such things. However, with the increasing importance of such "homotopification" in mathematics, it seems like a good thing to accomodate in the design of a purportedly generic proof assistant, even if it will be invisible to many of its users.
More importantly for the average mathematician, univalence also makes type theory an even closer match for ordinary mathematical practice, and hence a better vernacular for a proof assistant; and also fixes some of the traditional problems of type theory relative to set theory.
Firstly, mathematics is naturally univalent: group theorists do not distinguish between isomorphic groups, and so on. Thus, one naturally wants a vernacular for a proof assistant that can also seamlessly replace one structure with an isomorphic one. Plenty of work has gone into finding ways to build such invariance on top of existing set-theoretic or type-theoretic foundations, which more or less amounts to building a univalent context on top of a non-univalent one; so we may ask, in parallel with Andrej's point, once we have a univalent vernacular, why bother putting a non-univalent layer under it?
Secondly, while you didn't say what drawbacks of non-univalent type theory you have in mind, traditionally many of those drawbacks have involved the unnatural treatment of quotients. Non-univalent type theory doesn't really have a good way to deal with quotients, leading to the introduction of things like "setoids" that look very unnatural to an ordinary mathematician. But univalent type theory solves this problem, with a very natural presentation of quotients that has all the properties an ordinary mathematician would expect. Similarly, impredicative notions such as powersets are often klunky to deal with in non-univalent type theory, but work much better in univalent type theory.
I should say, though, as I said in my answer to the question linked by Wowoju in the comments, that these benefits are not currently huge. The usefulness of univalence for isomorphism-invariance, in particular, is limited in the absence of proof assistants that can actually use univalence to transfer a definition across an isomorphism automatically and compute the result, rather than forcing the user to laboriously unwind the transport to figure out the result. Cubical Agda, and other more recent proof assistants based on cubical type theories, have the promise of behaving in this way, but we still have a lot to learn about how best to design such proof assistants and what can be done with them. Moreover, we are still working out how to reconcile these computational features with the desired many models of type theory. So while I believe the potential benefits are substantial, many of them are still in the future.
