Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 5: Borderline accept: Technically solid paper where reasons to accept outweigh reasons to reject, e.g., limited evaluation. Please use sparingly.
review_content: summary: The authors study an interesting problem --- applying an algebraic proof system to certify the correctness of Monte Carlo estimators. They proposed a verifiable randomized approximation scheme based on an arithmetic circuit. Specifically, they consider both the succinct arithmetic circuit and the approximated circuit to approximate random variables. Moreover, they apply their analysis to two applications --- approximate model counting of disjunctive normal form and gradient estimation.  
strengths_and_weaknesses: The authors propose a generic method to certify the correctness of Monte Carlo estimators with explicit examples. The authors fairly state the potential limitations, e.g., the lack of experiments. Though unfamiliar with this area, I think this is a welcome contribution to the trustworthy machine learning community.
questions: Could the authors briefly discuss the challenges of deploying their algorithms in practice? 
limitations: None.
review_title: null

final_score: rating: 3: Reject: For instance, a paper with technical flaws, weak evaluation, inadequate reproducibility and incompletely addressed ethical considerations.
review_content: summary:   This paper proposes to verify Monte Carlo algorithms through the use of low-degree arithmetic circuits.
  The idea being that if a Monte Carlo algorithm can be made to agree with a computation as represented
  by this circuit we can be reasonably confident in the correctness of the computation after a relatively
  small number of problem instances.

strengths_and_weaknesses:   Originality:

  While I'm not if arithmetic circuits have been used to confirm the correctness of Monte Carlo inference,
  the idea of using multiple inference algorithms to check the correctness of each algorithm against
  the other is not new. Many of the examples used in the paper appear to be effectively doing just that. It
  appears the polynomial looks like a tractable expectation.
  
  Technical Quality:

  While the paper has many examples of how these circuits could be constructed there isn't much that
  looks like a generic method. There are no experiments or really any results showing empirically how
  much extra time is needed to produce a correctness certificate, even for all the examples mentioned.
  The work would greatly benefit from a more thorough exploration of some of the example circuits but
  also a more systematic way to produce these circuits.
  
  Clarity:

  I found the paper challenging to follow. There are many examples introduced and many extensions suggested
  for the approach, but not much detail about the general algorithm itself.
  
  Significance:

  I think there is much potential value in producing correctness proofs for Monte Carlo inference algorithms.
  While it's not fully clear how often an arithmetic circuit can be found for all expectations, if that set
  of problems can be better clarified, this could be a big deal.

questions: What inference problems is this method best suited for?

How might one go about finding an arithmetic circuit for a particular problem?

How much additional computation should one expect on a typical example problem?
limitations: The authors do discuss some of the limitations of this work. Possible negative societal impacts are not discussed, but I suspect the risks are fairly minimal. The research problem being addressed is very general.
review_title: null

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: summary: Monte Carlo integration methods are ubiquitous in modern computational tasks and can be highly parallelized across multiple servers. This paper introduces a framework based in algebraic circuits for verifying that the returned estimates provided by the servers were not adversarially manipulated. If the estimates were properly computed, the verification technique will not indicate the information has been manipulated. If they were not properly computed, the technique will indicate that manipulation has occurred with high probability. The authors demonstrate their technique on several classical problems, such as permanent estimation.
strengths_and_weaknesses: Strengths: While this paper is mostly outside of my area of knowledge, it seems original and to have practical applications in distributed computing. A strength of the paper is the focus on examples. The examples considered are common, practical problems and illustrate the usefulness of this technique. Another strength is that the introduction clearly illustrates the motivation for the problem and provides insight into the technique being used. 

Weaknesses: One weakness is that the main theorem (theorem 1) feels buried in the paper. Most of the paper focuses on example problems, but it may be valuable to give a brief proof sketch of the main theorem.

questions: Nothing additional.
limitations: The authors discuss the limitations of their work in the discussion section at the end of the paper. In particular, they note that it is non-obvious how to construct these verification systems for problems in which estimates do not have pairwise independence, such as MCMC or sequential inference problems. Moreover, they mention that engineering low degree circuits by hand is difficult, and that learning circuit structure is hard even for restricted problem classes.
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: This paper introduces an MC integration technique in that the computations have an algebraic proof of correctness where the proof is polynomial evaluated at random points. It provides a verified randomized approximation scheme for weighed counting to approximate the target quantity by use of MC. 
strengths_and_weaknesses: Strengths:
- It is well-written and easy to follow. 
- Proof of this technique seems to be very standard in the literature, especially complexity theory but it is interesting to see the application in this context. 

Weakness: 
- Using MC requires samples to be as uncorrelated as possible to converge. This is often hard to accomplish in practice, hence MCMC. 
- There are similarities between this work and some previous work specifically [27]. 
- Some discussion on the effect of size and degree of circuits seems to be necessary.
- Seems like finding the appropriate circuit that approximates the random variable of interest is not an easy task 

questions: - how does it compare to others for instance [27], [8]?
- how is pairwise independence not a very restrictive assumption in practice? 
- The performance of an MC estimator depends on the variance of the estimator. How does this method which equips MC estimators with proof correctness depend on the variance of the estimator and how would it be affected?
 -  Even though the gradient estimation for VI is interesting, however, the used estimate of the gradient is shown to have high variance. How does it work for other more advanced gradient estimators and how would the size of sub-circuits change to keep the error low? 
limitations: - Samples must be i.i.d. which is hard to draw in practice. 
- Lack of comparison to other techniques
- seems choosing circuits can be difficult and begs some more discussion on that. 
- Even though some nice examples are provided it feels like it is not something widely applicable specifically for state-of-the-art methods.
review_title: null

Meta-review: metareview: Reviewers collectively had relatively low confidence when reviewing this paper. This is not surprising, as the paper reads somewhat more like a theory CS paper, rather than a typical ML paper (even a theory one). The main concerns seemed to be that the work is not super concrete, and fairly speculative. These seem like natural concerns for a TCS-style paper, which the authors have tried to address with many explicit examples, and it seems tough to further address this without completely changing the focus of the paper. I cautiously recommend acceptance with the hope that there will be further exploration of these ideas, perhaps with more practical instantiation.
confidence: Less certain
Decision: Accept