The answer is yes, NP/poly is defined as the class of problems solvable in polynomial time by a non-deterministic Turing machine that has access to a polynomial-bounded advice function--the advice function only adds power; however, I'm having a hard time understanding NP/poly's containment of NP from the angle of the definition below of NP/poly:
A nondeterministic circuit has two inputs x,y. The circuit C accepts x iff there exists y such that C(x,y) = 1. The size of the circuit is measured as a function of |x|. NP/poly is the set of languages decided by polynomial size non-deterministic circuits.
A nondeterministic Turing machine has two inputs w,c. A verifier V accepts w iff there exists a certificate c such that V(w,c) = 1. The length of computation is measured as a function of |w|. NP is the set of languages decided by a nondeterministic Turing machine that runs in polynomial time.
From the verifier angle, for a couple reasons it is hard to see how a single circuit of poly size could implement a verifier for an NP problem for all the words of a given length.
For example. let's say an NP language has an exponential number of yes instances of a given length all with various certificates. Let's say we consider those certificates that are descriptions of the accepting branches of a non-deterministic Turing machine that correctly decide each w of the given length--how could a single poly size circuit simulate all these (possibly exponential number of) c's (solution paths) on their respective w's to see if the verifier works?
A circuit can only have a single size input and for each size of input there is only one circuit in the circuit family; yet, for a given word w of length b there are an infinte number of c's that are poly|w| that are potential certificates--how can the single circuit for inputs of length b accept on all the different certificates for the w's of length b when their lengths are variable?
Looking for some help on how I'm thinking about this wrong, thank you!