I wonder if there are any known implications of Babai's recent quasi-polynomial time algorithm for Graph Isomorphism to separating words by DFA's. In both cases the ultimate goal is to differentiate some object, though the conditions are quite different. I would like to know what people more familiar with Babai's proof think about whether some of the ideas there are applicable to word separation or not.
I hadn't thought about the Separating Words problem before, but based on looking at the Robson paper referenced in the linked answer, I don't immediately see how techniques from GI would apply.
At a high level, note that techniques for GI such as Luks's and Babai's all compute the automorphism group of a graph, and are very group-theoretic in nature. In the Separating Words Problem, I don't see how groups like this would naturally arise (though perhaps I've just missed it).
At a more detailed level, before asking whether Babai's algorithm has any application here, it is worth asking whether Luks's technique could apply, as this is the framework of Babai's algorithm. (Babai's main improvement was to handle the bottleneck case of Luks's algorithm - Johnson groups - much more efficiently.) Again, my answer to this is more or less the same as in the previous paragraph.
For example, is there a natural symmetry group (aside from a permutation of the alphabet) that preserves the length of the separating word? Even if there were, I don't see how the techniques would apply, but it might at least provide a foothold.
Now, of course, there are lots of combinatorial and group-theoretic lemmas proved along the way in Babai's paper, and it's impossible to say that those won't be relevant, but at least at first glance I don't see how.