Are there physical theories that require the axiom of choice to be "true" to work?
No, nothing in physics depends on the validity of the axiom of choice because physics deals with the explanation of observable phenomena. Infinite collections of sets – and they're the issue of the axiom of choice – are obviously not observable (we only observe a finite number of objects), so experimental physics may say nothing about the validity of the axiom of choice. If it could say something, it would be very paradoxical because axiom of choice is about pure maths and moreover, maths may prove that both systems with AC or non-AC are equally consistent.
Theoretical physics is no different because it deals with various well-defined, "constructible" objects such as spaces of real or complex functions or functionals.
For a physicist, just like for an open-minded evidence-based mathematician, the axiom of choice is a matter of personal preferences and "beliefs". A physicist could say that any non-constructible object, like a particular selected "set of elements" postulated to exist by the axiom of choice, is "unphysical". In mathematics, the axiom of choice may simplify some proofs but if I were deciding, I would choose a stronger framework in which the axiom of choice is invalid. A particular advantage of this choice is that one can't prove the existence of unmeasurable sets in the Lebesgue theory of measure. Consequently, one may add a very convenient and elegant extra axiom that all subsets of real numbers are measurable – an advantage that physicists are more likely to appreciate because they use measures often, even if they don't speak about them.
Rigorous arguments in functional analysis are made much simpler by employing the axiom of choice. As we are free to model our physics in any set theory we like, and any set theory containing ZF contains a model of ZFC, we are entitled to use this simplification without fear of inconsistency. Discarding the axiom of choice would only make concepts and proofs more tedious, without giving any higher degree of assurance of the results.
For example, the standard proof of the spectral theorem for self-adjoint operators depends on the axiom of choice, I believe, and much in mathematical physics depends on the spectral theorem.
On the other hand, already on the level of theoretical physics, one often replaces scrupulously integrals by finite sums, takes limits irrespective of their mathematical existence, and employs lots of other mathematically dubious trickery to get quickly at the results.
So on this level of reasoning, nothing depends on subtleties that make a difference only when one begins to care about precise definitions and arguments in the presence of infinity.
The following paper may be of interest:
Norbert Brunner, Karl Svozil, Matthias Baaz, "The Axiom of Choice in Quantum Theory". Mathematical Logic Quarterly, vol. 42 (1) pp. 319-340 (1996).
The abstract is as follows:
We construct peculiar Hilbert spaces from counterexamples to the axiom of choice. We identify the intrinsically effective Hamiltonians with those observables of quantum theory which may coexist with such spaces. Here a self adjoint operator is intrinsically effective if and only if the Schrödinger equation of its generated semigroup is soluble by means of eigenfunction series expansions.
Also relevant is the fact that classical analysis doesn't require much more than dependent choice, which is consistent with "All sets of reals are Lebesgue measurable". However the combination of the two statements requires a stronger assumption as a theory (inaccessible cardinals).
What does baffle me, however, with physicists that have strong objections to the Banach-Tarski paradox, that it makes much less sense that a set can be partitioned into strictly more [non-empty] parts than elements. And that is a consequence of having all sets Lebesgue measurable.
So while you may sleep quietly knowing that you cannot partition an orange into five parts and combining the parts into two oranges (thus solving world hunger), you have an equally disturbing problem. You can cut out a line [read: the real numbers] into more parts than points.