If P/poly = NP/poly, then NP $\subset$ P/poly, with known interesting implications, like the collapse of the polynomial hierarchy. But if somebody would manage to prove P/poly != NP/poly, could we derive any interesting implications from this result?

One motivation for investigating NP/poly is a drawback of Hutter's algorithm, namely that it depends on a fixed formal system $\mathsf{F}$:

For a given sufficiently strong formal axiomatic system $\mathsf{F}$ (like $\mathsf{PA}$ or $\mathsf{ZFC}$) and any given function $p^*(x)$ that can be specified within the formal system $\mathsf{F}$, Hutter's algorithm $M_{\mathsf{F},p^*}$ computes the function $p^*(x)$ nearly as quickly as any (provably quick) algorithm $p$ provably computing $p^*(x)$.

The dependence on a fixed formal system $\mathsf{F}$ is a drawback, because any fixed formal system is limited in the true statements it can prove, and also because the length of the shortest proof strongly depends on the formal system (first order logic vs. higher order logic).

Working in deterministic/poly allows to circumvent this drawback. (However, the proof that it is the fastest and shortest algorithm becomes questionable then, because the formal systems are no longer controllable). And working in nondeterministic/poly allows to address another drawback: Hutter's algorithm uses proof search, which is a natural nondeterministic process.