May Boolean circuits be exponentially more concise than Boolean formulae? Consider a family $(f_n)_{1 \leq n}$ of Boolean functions, where $f_n$ is a function on $n$ variables. Consider for every $n$ the smallest Boolean formula $F_n$ describing $f_n$, and the smallest Boolean circuit $C_n$ describing $f_n$. Say we have $|F_n| = \Omega(g(|C_n|))$ for a certain function $g$.

What is the fastest-growing $g$ for which this is known to be possible, and the slowest-growing $g$ for which it is known to be impossible? (From the comments, it seems like there is still a gap here, but I'm trying to understand which one.)

This is the "simple" version of my question. What I am interested in is a multi-output, probabilistic (=weighted), variant of the problem, defined as follows. It is clear how to extend circuits to be multi-output, and I define a $k$-output formula to be just a $k$-tuple of formulas on the same inputs. I say that the input variables have a certain probability of being true (written in binary and accounted for in the circuit or formula size), each independently from the others, and I look at the probability distribution on the tuple of outputs (forgetting which input is yielding which output, just looking at the distribution on values), given this product distribution on the inputs, in the circuit and formula context. Here again the circuits are certainly more concise than formulae, but how much? Are there some distributions that can be exponentially more concise to represent with circuits, intuitively because of sub-expression reuse?

To give an example for this more elaborate version, consider the following distribution on $n$ outputs:


$000 \cdots 00$ with probability $1/2$,
$100 \cdots 00$ with probability $1/4$,
$110 \cdots 00$ with probability $1/8$,
...
$111 \cdots 10$ with probability $1/2^n$,
$111 \cdots 11$ with probability $1/2^n$.


There is a multi-output probabilistic circuit of size $O(n)$ which generates this (and reuses the draw of the $i$-th bit to draw the $(i+1)$-th). By contrast, the straightforward Boolean function encoding of this is quadratic, and I can't see how you could make it shorter but yet cannot prove it...
The circuit complexity of any boolean function of $n$ variables is at most $(1+o(1))2^n/n$, so a separation of between circuit and formula complexity of $\Omega(2^n)$ is not possible. This upper bound was established by Lupanov, and his method is known as the Lupanov representation of boolean functions. It also gives an upper bound of $(1+o(1))2^n/\log n$ for the formula complexity of any $n$-variable boolean function. See for example these lecture notes for a detailed presentation. Of course this does not rule out a separation of $2^{\Omega(n)}$. 

To the best of my knowledge the biggest separation known currently is $n^{3-o(1)}$ (over the de&nbsp;Morgan basis). It was proved by Håstad for a function with linear circuit complexity. This was an improvement on the method of Andreev, who showed a formula size lower bound of $\Omega(n^{2.5})$ for the same function using the method of random restrictions. You can check these notes for Andreev's proof. Håstad's bound is essentially tight for Andreev's method.

The class of functions computable by polynomial size formulas coincides with (nonuniform) NC1 and the class of functions computable by polysize circuits is P/poly. Separating these two classes is a well-known open problem in complexity theory, and is almost certainly well out of reach.