There are many double-negation translations $f$, each with the property that $\vdash\varphi$ classically iff $\vdash f(\varphi)$ intuitionistically. Is there a translation the other way? Specifically, I mean, is there a function $f$ on formulae such that $\vdash\varphi$ intuitionistically iff $\vdash f(\varphi)$ classically?
For the purposes of this question, let us consider only propositional (intuitionistic and classical) logic, even though the double-negation translations mentioned above generalize to first-order logic.
Even in just the propositional case, given the difference in complexity between the two logics' semantics, one would expect any such $f$ would increase the size/complexity of its argument, perhaps even a lot. But making the translation as efficient as possible is a secondary (bonus?) question that comes after the question of whether such a translation exists at all.
Based on an analysis of computational complexity, we should not expect any such $f$ to be computable in polynomial time.
It is well-known that the problem of determining whether $\vdash \phi$ classically is a co-NP complete problem, since its complement is trivially equivalent to the famous satisfiability problem, the first problem ever proved to be NP-complete.
It is less known, but still established in the literature, that the task of determining whether $\vdash \phi$ constructively is PSPACE-complete.
If we had a polynomial-time reduction $f$ from the intuitionist problem to the classical problem, this would prove that $PSPACE = co-NP = NP$. However, it is not presently known whether $PSPACE = NP$, nor is it even known whether $NP = co-NP$.
Of course, if we wanted to be silly, we could define $f(\phi) = \top$ if $\phi$ is an intuitionist tautology and $\bot$ otherwise. This would satisfy your criterion. But this function does not reveal much insight, and, as mentioned, computing $f(\phi)$ is a $PSPACE$-complete problem which we should not expect to be solvable in polynomial time.