In this paper, we obtain several new results on lower bounds and derandomization for ACC^0 circuits (constant-depth circuits consisting of AND/OR/MOD_m gates for a fixed constant m, a frontier class in circuit complexity):

1. We prove that any polynomial-time Merlin-Arthur proof system with an ACC^0 verifier (denoted by MA_{ACC^0}) can be simulated by a nondeterministic proof system with quasi-polynomial running time and polynomial proof length on infinitely many input lengths. This improves the previous simulation by [Chen, Lyu, and Williams, FOCS 2020], which requires both quasi-polynomial running time and proof length.

2. We show that MA_{ACC^0} cannot be computed by fixed-polynomial-size ACC^0 circuits, and our hard languages are hard on a sufficiently dense set of input lengths.

3. We show that NEXP (nondeterministic exponential-time) does not have ACC^0 circuits of sub-half-exponential size, improving the previous sub-third-exponential size lower bound for NEXP against ACC^0 by [Williams, J. ACM 2014].

Combining our first and second results gives a conceptually simpler and derandomization-centric proof of the recent breakthrough result NQP = \NTIME[2^{polylog(n)}] is not in ACC^0 by [Murray and Williams, SICOMP 2020]: Instead of going through an easy witness lemma as they did, we first prove an ACC^0 lower bound for a subclass of MA, and then derandomize that subclass into NQP, while retaining its hardness against ACC^0.

Moreover, since our derandomization of MA_{ACC^0} achieves a polynomial proof length, we indeed prove that nondeterministic quasi-polynomial-time with n^{omega(1)} nondeterminism bits (denoted as NTIMEGUESS[2^{polylog(n)},n^{omega(1)}]) has no poly(n)-size ACC^0 circuits, giving a new proof of a result by Vyas. Combining with a win-win argument based on randomized encodings from [Chen and Ren, STOC 2020], we also prove that NTIMEGUESS[2^{polylog(n)},n^{omega(1)}] cannot be (1/2+1/poly(n))-approximated by poly(n)-size ACC^0 circuits, improving the recent strongly average-case lower bounds for NQP against ACC^0 by [Chen and Ren, STOC 2020].

One interesting technical ingredient behind our second result is the construction of a PSPACE-complete language that is paddable, downward self-reducible, same-length checkable, and weakly error correctable. Moreover, all its reducibility properties have corresponding AC^0[2] non-adaptive oracle circuits. Our construction builds and improves upon similar constructions from [Trevisan and Vadhan, Complexity 2007] and [Chen, FOCS 2019], which all require at least TC^0 oracle circuits for implementing these properties.