This doesn't answer your question, but gives some information that
might be useful.
Main Claim: ZFC + "There is a proper class of inaccessible limits of measurable cardinals" + "There is some measurable cardinal $\kappa$ and an
ordinal definable normal measure on $\kappa$" disproves the statement
in question.
Corollary: If ZFC + VP is consistent, then so is ZFC + VP + the
negation of the statement in question.
Proof of corollary: Let $\kappa$ be a measurable cardinal. Let $\mu$
be a normal measure on $\kappa$.
In some interval of form $(\kappa^+,\eta)$, where $\eta$ is ${<}$ the
next measurable $>\kappa$, we can force an encoding of
$(\mathcal{P}(\kappa),\mu)$ into the GCH pattern, without adding
$\kappa$-sequences. This preserves the fact that $\mu$ is a normal
measure on $\kappa$, makes $\mu$ OD, and preserves all large cardinal
structure for critical points $>\kappa$, hence VP.
Proof of Main Claim: We deal here with linear iterations of $V$ of length
${<\omega}$ which use only normal measures. That is, a sequence
$\left<M_n,\mu_n\right>_{n\leq N}$ such that $N<\omega$, $M_0=V$,and
for $n<N$ we have $\mu_n\in M_n$ and $M_n\models$"$\mu_n$ is a normal
measure on some measurable cardinal",
and $M_{n+1}=\mathrm{Ult}_0(M_n,\mu_n)$, where the $\mathrm{Ult}_0$
denotes the ultrapower constructed using only functions in $M_n$. The
critical points of the iteration are the ordinals $\kappa_n$ such
that $\mu_n$ is a measure on $\kappa_n$. (So
$\kappa_n=\mathrm{crit}(i_{n,n+1})$ where $i_{n,n+1}:M_n\to M_{n+1}$
is the ultrapower map,
and $i_{mn}:M_m\to M_n$ is defined by composing these, for $m< n$.)
We would like to find a second order formula $\varphi$
which is averageable, but not (somewhat) obviously averageable.
We will look for $\varphi$ in the language of set theory.
Note that such a formula is averageable as witnessed by ultrafilter
$U$ iff $M=\mathrm{Ult}(V,U)$ is $\varphi$-correct; that is, iff we
have $M\models\varphi(X)\iff V\models\varphi(X)$ for all structures
$X\in M$ for the language of set theory. Of course $\varphi$ can be
taken to demand that $X$ is transitive, and so if desired, one can
restrict attention to such things, and also further to sets of the
form $V_\alpha^M$, or even ordinals
(we will do the latter below). To arrange $\varphi$ we will look at a
kind of closure point of forming ultrapowers -- produced by
considering finite iterations via normal measures, and roughly,
$\varphi(\lambda)$ will say that $\lambda$ is inaccessible in some
such finite iterate. However, in order for the correctness proof to
work, we will need to slightly modify this plan, by restricting the
possible nature of the iterations further, and this is where the OD
measure comes in.
Let $\lambda_0$ be the least inaccessible cardinal such that there is
a normal measure $U\in V_{\lambda_0}$ such that $U$ is (first order)
definable from ordinal parameters over $V_{\lambda_0}$. Then by
minimizing on ordinal parameters, actually there is one which is
outright definable from no parameters over $V_{\lambda_0}$. Let $U_0$
be such, and we fix a definition of $U_0$ over $V_{\lambda_0}$. Note
that $\lambda_0$ and $U_0$
are uniformly second-order describable over any ordinal
$\gamma\geq\lambda_0$ (one just uses the 2nd order quantifiers to
request a subset of $\gamma$
encoding the right sort of information, so as to recover $V_{\lambda_0},U_0$).
Let $\xi_0$ be the corresponding measurable cardinal, i.e. $U_0$ is a
normal measure on $\xi_0$.
Let $\varphi(\lambda)$ be the second order statement in the language
of set theory asserting the following clauses:
$\lambda$ is (isomorphic to) an ordinal,
$\lambda\geq\lambda_0$,
there is a finite linear iteration $\left<M_n,\mu_n\right>_{n\leq N}$ of $V$
(so $N<\omega$) which uses only normal measures, with strictly
increasing critical points $\left<\kappa_n\right>_{n< N}$ (i.e.
$\kappa_n<\kappa_{n+1}$),
if $N>0$ then $\xi_0\leq\kappa_0$,
there is $N_0\leq N$ such that:
(i) $\left<M_n,\mu_n\right>_{n\leq N_0}$
is just given by iterating $U_0$ and its resulting images,
i.e. if $0<N_0$ then $\mu_0=U_0$, and if $0<m<N_0$ then
$\mu_m=i_{0m}(U_0)=(U_0)^{M_m}$ (note possibly $N_0=0$);
(ii) if $N_0<N$ then $i_{0N_0}(\xi_0)<\kappa_{N_0}$
and $\kappa_n$ is not a limit of measurable cardinals
in $M_n$, for $N_0\leq n<N$.
$M_N\models$"$\lambda$ is an inaccessible limit of measurables", and $i_{0N}(\xi_0)<\lambda$
and $\kappa_n<\lambda$ for all $n<N$.
(The requirement that $\kappa_n<\lambda$ for all $n<N$
actually makes no difference to the truth of $\varphi(\lambda)$, since
otherwise we can always cut an iteration off at the first point a critical point goes $\geq\lambda$.)
The fact that $\varphi$ is second order is because we can code all the
information needed to verify that $\varphi(\lambda)$ holds in a subset
of $\lambda$, and given an appropriate such code, it's simply
definable to say that it works. For suppose
$\left<M_n,\mu_n\right>_{n\leq N}$
is an iteration as above, and $\lambda$ is an inaccessible limit of measurables of $M_N$ as above. If $\lambda\in\mathrm{rg}(i_{0N})$, say
$i_{0N}(\bar{\lambda})=\lambda$, then note $\xi_0<\bar{\lambda}$ and
$\kappa_n< i_{0n}(\bar{\lambda})$ for each $n<N$ (we
can't have $\kappa_n=i_{0n}(\bar{\lambda})$
because $\kappa_n$ is only a successor measurable of $M_n$).
Note then that in fact $\bar{\lambda}=i_{0n}(\bar{\lambda})=\lambda$
(using the inaccessibility of $\bar{\lambda}$ in $V$).
But also the iteration can be considered as an iteration starting with first model $M_0=V_{\bar{\lambda}}$ (instead of first model $M_0=V$). By inaccessibility, $|V_\lambda|=\lambda$, so there is $A\subseteq\lambda$ coding $V_\lambda$ and the iteration, which is enough. Now suppose instead that
$\lambda\notin\mathrm{rg}(i_{0N})$, and let $\theta$ be the least ordinal
such that $i_{0N}(\theta)>\lambda$. Then note $\theta$ is a limit of
inaccessible limits of measurable cardinals of $V$, so $\theta=|V_\theta|$. The iteration
is equivalent to one on $V_{\theta+1}$;
we have $\kappa_n<i_{0n}(\theta)$ since otherwise $\theta$ would be a successor measurable in $V$, which it isn't. (Therefore $\theta$ is in fact singular of measurable cofinality, and $i_{0N}``\theta$ is bounded in $i_{0N}(\theta)$.)
So it suffices to see that
$|V_{\theta+1}|\leq\lambda$, as then we can code $V_{\theta+1}$ through a subset of $\lambda$. But
$i_{0N}``V_\theta\subseteq V_{\theta'}^{M_N}$ where $\theta'=\sup
i_{0N}``\theta<\lambda$, and we get an injection $V_{\theta+1}\to
V_{\theta'+1}^{M_N}$ by sending $X\mapsto i_{0N}(X)\cap
V_{\theta'}^{M_N}$.
(Note that if $X\neq Y$ then $i_{0N}(X),i_{0N}(Y)$ disagree somewhere
within $i_{0N}``V_{\theta}$). But $M_N$ has a bijection between
$V_{\theta'+1}^{M_N}$ and some ordinal ${<\lambda}$, since
$M_N\models$"$\lambda$ is inaccessible", which suffices.)
Now I claim that $\varphi$ is absolute between $V$ and
$M=\mathrm{Ult}(V,U_0)$ (that is, for all $\lambda\in M$, we have
$\varphi(\lambda)\iff M\models\varphi(\lambda)$), and note that it
follows that $\varphi$ is averageable, as witnessed by $U_0$. (Letting
$\lambda=\Pi_{\eta<\kappa}\kappa_\eta$, where the $\kappa_\eta$ are
ordinals,
we get $\varphi(\lambda)$ iff $M\models\varphi(\lambda)$
iff $\{\eta<\kappa\bigm|\varphi(\kappa_\eta)\}\in U_0$.)
Proof: It is immediate that $M\models\varphi(\lambda)\implies
V\models\varphi(\lambda)$, since given the witnessing finite iteration
in $M$,
just insert $(V,U_0)$ at the front, and note this yields a witness
which works for $\lambda$ in $V$. So suppose
$V\models\varphi(\lambda)$
and let $\left<M_n,\mu_n\right>_{n\leq N}$ be a witnessing iteration.
If $N>0$ and $\mu_0=U_0$ then the tail $\left<M_n,\mu_n\right>_{1\leq
n\leq N}$ works in $M$. So suppose either $N=0$ or $\mu_0\neq U_0$,
and hence $\xi_0<\kappa_0$ in the latter case. If $N=0$ it is easy:
by $\varphi(\lambda)$, we have $\xi_0<\lambda$ and $\lambda$
inaccessible, so $i^V_{U_0}(\lambda)=\lambda$, so
$M\models\varphi(\lambda)$.
Suppose $N>0$. Then $i_{U_0}(\lambda)=\lambda$ still,
so $M\models\varphi(\lambda)$. For $U_0\in M_N$,
and $\lambda>\xi_0$ is inaccessible in $M_N$,
so $i^{M_N}_{U_0}(\lambda)=\lambda$ where
$i^{M_N}_{U_0}:M_N\to\mathrm{Ult}_0(M_N,U_0)$ is the ultrapower map
associated to the internal ultrapower of $M_N$, i.e. formed using only
functions in $M_N$.
But since the iteration leading to $M_N$ has critical points $>\xi_0$,
$M_N$ is $\xi_0$-closed, so this embedding is the same as
$i^V_{U_0}\upharpoonright M_N$, so
$i^V_{U_0}(\lambda)=i^{M_N}_{U_0}(\lambda)=\lambda$.
This proves the claim above. It remains to see that $\varphi$ is not
(somewhat) obviously averageable. Suppose otherwise, and let $\widehat{\varphi}$ be the witness, and let $\widehat{\varphi}\in V_{\gamma_0}$ where $\gamma_0$ is a successor inaccessible with $\xi_0<\gamma_0$. Let $\lambda$ be the least inaccessible limit of measurables such that $\lambda>\gamma_0$. So $\varphi(\lambda)$ holds, so $\widehat{\varphi}((\lambda;R_1,\ldots,R_k))$ holds for some predicates $R_1,\ldots,R_k$. Now let $X\preccurlyeq V_{\lambda+1}$ with $V_{\gamma_0+1}\subseteq X$ and $X$ closed under $\gamma_0$-seqences and $|X|<\lambda$. Let $C$ be the transitive collapse of $X$. Note the fact that $\widehat{\varphi}((\lambda;R_1,\ldots,R_k))$ holds is first order over $V_{\lambda+1}$, and reflects into $C$ regarding the collapsed version $(\bar{\lambda},\bar{R}_1,\ldots,\bar{R}_n)$, which is correct about this assertion, because $C$ is closed under $\gamma_0$-sequences. So $\varphi(\bar{\lambda})$ holds. But $\gamma_0<\bar{\lambda}<\lambda$,
and $\gamma_0$ is a successor inaccessible with $\xi_0<\gamma_0$.
It follows that $\gamma_0$ is fixed by all the finite iteration maps under consideration, and hence so is $\lambda$. So no such iterate can witness $\varphi(\bar{\lambda})$, a contradiction.
