Previous answer completely rewritten
It seems to me that your hypothesis is true, up to a constant correction:
$$\sum_{\textstyle{\pi: \{1,2,\ldots,n\} \to \{\mathbb{I}, \sigma_x, \sigma_y, \sigma_z\} \atop \forall i \in \{x,y,z\}:\ \mathrm{card}(\pi^{-1}(\sigma_i))=n_i}} \!\!\bigotimes_{i=1}^n\ \ \pi(i) \cong \frac1{n_x! n_y! n_z!} \mathopen{:} \left( a^\dagger b + b^\dagger a \right)^{n_x} \left( - i a^\dagger b + i b^\dagger a \right)^{n_y} \left( a^\dagger a - b^\dagger b\right)^{n_z} \mathclose{:},$$
and that this can be proven using multivariate induction.
For generic $n_x, n_y, n_z$, let $$[\![n_x, n_y, n_z]\!]$$ symbolically denote the operator on the left-hand side, in the qubit picture.
The induction step may be based upon the observation
$$[\![1,0,0]\!][\![n_x, n_y, n_z]\!] = (n_x+1)[\![n_x+1, n_y, n_z]\!] - i(n_y+1)[\![n_x, n_y+1, n_z-1]\!] + i(n_z+1)[\![n_x, n_y-1, n_z+1]\!] + (n-n_x-n_y-n_z+1)[\![n_x-1, n_y, n_z]\!].$$
(It's a matter of simple combinatorics to find the multipliers.) There are perfectly analogous relations for multiplying by $[\![0,1,0]\!]$ or $[\![0,0,1]\!]$ from the left, too. Defining the double square brackets to be zero when either of the components is negative, this set of relations holds universally and the sufficient set of anchor points is the Wigner representation of $[\![1,0,0]\!]$, $[\![0,1,0]\!]$, $[\![0,0,1]\!]$, where we prove the equivalence to the Fock picture formulas directly.
Now one would just prove either of the relations (arguing by symmetry) to hold for the right-hand side, using re-ordering of the products after a multiplication by $$[\![1,0,0]\!] \cong a^\dagger b + ab^\dagger$$ and $$n \cong a^\dagger a + b^\dagger b$$ from the left. It requires a certain amount of work but should be doable. (I tried but ran into some kind of a numerical error.)
With a future edit on my mind, I will try to finish the proof of the induction step to see if I am right about the additional factor.
Assuming the relation is true, I doubt that there is any more "closed form" than the expansion
$$\sum_{j=0}^{n_x} \sum_{k=0}^{n_y} \sum_{l=0}^{n_z} \frac{(-1)^{k+n_z-l} i^{n_y}}{j!k!l!(n_x-j)!(n_y-k)!(n_z-l)!}
(a^\dagger)^{j+k+l} a^{n_x+n_y-j-k+l} (b^\dagger)^{n_x+n_y+n_z-j-k-l} b^{j+k+n_z-l}$$
as this does not seem to have any factorisation except for the one employing the normal reordering brackets.
Best Answer
There are algorithms to generate all elements of the Clifford group for a specified number of qubits. One implementation is available here: http://www.cgranade.com/python-quaec/ (see the
qecc.clifford_group(nq, consider_phases=False)iterator). The code implementing this can be seen here. It basically generates all possible mappings and then filters out those that do not fulfill the commutation and anticommutation relations. The section "Number of Elements" of this goes in a bit more depth.There are also algorithms that can give you a random Clifford operator without having to generate the entire group (which makes it exponentially more efficient if all you need is just a random sample of the Clifford group). See https://arxiv.org/pdf/1406.2170.pdf.