-
Notifications
You must be signed in to change notification settings - Fork 162
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
LogUp-GKR proposition to simplify input layer polynomials #1417
Comments
The argument needs linearity in order for it to go through, but the expression proposed in the simplification is not linear in |
Ah yes, good catch, Thaler's simplification indeed doesn't apply in this case. |
(I am re-opening based on an offline discussion.) Indeed, Thaler's idea does not seem to apply here but nevertheless we can simplify the current treatment of the input layer by making the following observation. The equation linking the input layer to its successor can be expressed as follows: and where and From a performance standpoint, the tree depth stays the same but we avoid running the sum-check of degree 3 for |
Implemented in facebook/winterfell#295 |
I believe we can simplify proving the input layer by getting rid of
FinalLayerProof.before_merge_proof
, following an argument analogous to how Thaler simplified the layer polynomial definition from the original GKR paper in this note.This simplification would simplify the code for the input layer, as well as reduce proving time (since we run$\nu - 1$ fewer sum-check rounds).
Notation
We will use the following notation, which is very similar to what was used in other issues. It is probably easier to skip to the next section, and only refer back to specific parts of this list when needed.
In LogUp-GKR, each layer is interpolated by 2 polynomials. We will denote the input layer polynomials as
Similarly,$p_{d-1}$ and $q_{d-1}$ will be used to refer
Also, given any function$\psi(x, y)$ , we define $\psi_{\hat{x}}(y) = \psi(\hat{x}, y)$ . In words, this is the notation we'll use to bind a variable $x$ to a fixed value $\hat{x}$ .
Lastly, we will automatically "destructure" variables. Specifically, if$x = (x_0, x_1)$ , then $\psi(x) = \psi(x_0, x_1)$ .
Current treatment of input layer
Let$w \in {0,1}^{\nu - 1}$ .The input layer is currently defined as
We run a sum-check over$w$ and $x$ in 2 phases (using
GkrComposition
andGkrCompositionMerge
, respectively). The first phase's result is stored inFinalLayerProof.before_merge_proof
, while the second phase's result is stored inFinalLayerProof.after_merge_proof
.The first sum-check is over$w$ (i.e. $x$ is treated as a constant). Once we completed the $\nu - 1$ rounds, we will have sampled $\nu-1$ random elements that we'll call $\rho_w$ . This corresponds to
merge_randomness
inGkrCompositionMerge::new
.Then, the second sum-check is over the remaining$x$ variables, and uses $\rho_w$ instead of $\hat{w}$ . It is defined as:
where we abuse the$\tilde{p}_d$ and $\tilde{q}_d$ notation to mean:
Simplification of input layer
I believe we can forgo the first sum-check over$w$ , and define our input layer sum-check as
where we reuse the same abuse of notation for$\tilde{p}_d$ and $\tilde{q}_d$ from the previous section. In practice this reduces to only running the $\hat{w}$ as
FinalLayerProof.after_merge_proof
part of the input layer, and usemerge_randomness
argument toGkrCompositionMerge::new
.Formally, this reuses the same idea from Thaler, specifically equations 3 and 4, and subsequent proof. Basically, to show that the right-hand side is an equivalent definition of$(p_{d-1} + \lambda q_{d-1})(\hat{w}, \hat{x})$ , we only need to show that our definition is a proper MLE of the input layer data; that is,
This, along with the fact that the MLE of a function is unique, completes the proof. I believe the same proof (after equation 4) from Thaler's note applies here, so I will leave it out.
The text was updated successfully, but these errors were encountered: