Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks

We are grateful for your positive and encouraging assessment of our work. We also sincerely appreciate the "accept" recommendation and recognition of our paper's evaluation, novelty, and potential for impact. We have incorporated your feedback to make our paper even stronger:

1. On Presentation, Scalability, and Overhead

Clarity of figure 1: We appreciate this constructive feedback. We acknowledge that the initial version of Figure 1 was dense. In response, we have redesigned it to be more intuitive and readable. Due to the text-only format of this rebuttal this year, we cannot display the new figure here or update the PDF, but we have implemented the following improvements for the final version:

• There is now a clearer layout, and the figure is structured into distinct stages (LLM Sampling > PCFG Parsing & Learning > Uncertainty Calculation > Prediction), guiding the reader through our pipeline.
• The confusing pie chart has been removed, and the bar chart showing rule frequencies has been simplified and now uses a consistent and explicitly labeled color-coding scheme. We have also enlarged all text elements for readability.

Runtime/Memory Profile**:** This is an excellent point. We conducted this experiment to address your concern.

As you can see, the overhead of our PCFG extraction and analysis is minimal, as it primarily involves efficient parsing (using ANTLR) and frequency counting (Maximum Likelihood Estimation) over a fixed set of 100 samples. Our experiment pipeline is dominated by LLM inference time, not UQ calculations.

2. On Methodology and Practical Application

Applicability to other formal languages

This is a fantastic suggestion. We were able to perform this pilot study to demonstrate the framework's generality.

Our parser and PCFG construction logic uses ANTLR under the hood; therefore, we can use any of the grammar files in the ANTLR-v4 repository on Github. There is no g4 file for Coq, Isabelle, or Lean, but there is one for Prolog, which is remarkably similar to first-order logic in construction. We were able to quickly adapt our PCFG analysis pipeline to work with Prolog programs without major engineering changes to our codebase, generating PCFGs and consequently the uncertainty measures. The fundamentals of our technique remain the same across programming languages with well-defined grammars. This also opens up the exciting possibility of using our tool to quantify uncertainty in general-purpose programming code generated by LLMs as future work. We converted the SMT code in Figure 1 of the paper into Prolog as follows:

% program1.pl
% ∀x. (StudiesMath(x) ∨ (StudiesPhysics(x) ∧ WorksHard(x))) → Succeeds(x).

% Facts
person(alice).
person(bob).
person(charlie).

studies_math(alice).
studies_physics(bob).
works_hard(bob).
works_hard(charlie).

% Rule
succeeds(X) :-
    studies_math(X).

succeeds(X) :-
    studies_physics(X),
    works_hard(X).

% On load: print all solutions and exit
:- initialization(main).
main :-
    forall(succeeds(X), writeln(X)),
    halt.

% program2.pl
% ∀x. ((StudiesMath(x) ∨ StudiesPhysics(x)) ∧ WorksHard(x)) → Succeeds(x).

% Facts
person(alice).
person(bob).
person(charlie).

studies_math(alice).
studies_physics(bob).
works_hard(bob).
works_hard(charlie).

% Rule
succeeds(X) :-
    ( studies_math(X)
    ; studies_physics(X)
    ),
    works_hard(X).

% On load: print all solutions and exit
:- initialization(main).
main :-
    forall(succeeds(X), writeln(X)),
    halt.

% program3.pl
% (∀x. StudiesMath(x)→Succeeds(x))  ∨  (∀x. (StudiesPhysics(x)∧WorksHard(x))→Succeeds(x))

% Facts
person(alice).
person(bob).
person(charlie).

studies_math(alice).
studies_physics(bob).
works_hard(bob).
works_hard(charlie).

% Toggle which implication you want:
option(math).      % ← comment this and uncomment the next to switch
% option(physics).

% Branch 1: StudiesMath(x) -> Succeeds(x)
succeeds(X) :-
    option(math),
    studies_math(X).

% Branch 2: (StudiesPhysics(x) ∧ WorksHard(x)) -> Succeeds(x)
succeeds(X) :-
    option(physics),
    studies_physics(X),
    works_hard(X).

% On load: print all solutions and exit
:- initialization(main).
main :-
    forall(succeeds(X), writeln(X)),
    halt.

% program4.pl
% ∀x. WorksHard(x) → (StudiesMath(x) ∨ StudiesPhysics(x)) → Succeeds(x)

% Facts
person(alice).
person(bob).
person(charlie).

studies_math(alice).
studies_physics(bob).
works_hard(bob).
works_hard(charlie).

% Nested implication expands to two rules
succeeds(X) :-
    works_hard(X),
    studies_math(X).

succeeds(X) :-
    works_hard(X),
    studies_physics(X).

% On load: print all solutions and exit
:- initialization(main).
main :-
    forall(succeeds(X), writeln(X)),
    halt.

% program5.pl
% ∀x. Succeeds(x) ↔ (StudiesMath(x) ∨ (StudiesPhysics(x) ∧ WorksHard(x)))

% Facts
person(alice).
person(bob).
person(charlie).

studies_math(alice).
studies_physics(bob).
works_hard(bob).
works_hard(charlie).

% Forward direction
succeeds(X) :-
    studies_math(X).
succeeds(X) :-
    studies_physics(X),
    works_hard(X).

% Backward direction to enforce ↔
studies_math(X) :-
    succeeds(X),
    \+ (studies_physics(X), works_hard(X)).

studies_physics(X) :-
    succeeds(X),
    works_hard(X).

% On load: print all solutions and exit
:- initialization(main).
main :-
    forall(succeeds(X), writeln(X)),
    halt.

Here are some summary statistics of the generated PCFG with the following programs: Total Rules = 560, Unique rules = 33, Non-terminals = 7, Maximum probability of a rule = 1.0, Minimum probability = 0.0086, Average probability = 0.2121. There are 4.7 rules per non-terminal, with a maximum branching factor of 16. The grammar entropy is 0, KL divergence from uniform is 1.34, and spectral radius is 0.83.

The core strength of our framework is its generality. Because it is built on the standard formalism of context-free grammars, it is not tied to SMT-LIB. In the revised manuscript, we will add a dedicated discussion on extensibility and how this can adapt to other formal languages or general programming languages, provided a base grammar is available.

Please note that conducting a new large-scale empirical study on the efficacy of Prolog-based uncertainty metrics on our datasets would be beyond the time scope of the current rebuttal period, but we see this as a clear and exciting next step.

How to avoid overfitting with 25 signals

This is a good question. Let us clarify:

• In our approach, 21 out of the 25 metrics (i.e., non-ensemble methods) have no chance of overfitting since there is no "learning" happening apart from basic PCFG construction. UQ analysis is performed on a per-instance basis: for each reasoning problem, we generate 100 samples of programs and induce a new, problem-specific PCFG. There is no global "training set" of PCFGs.

• The 21 metrics are used to create a $21,1$ -dimensional feature vector for each single instance, and our ensemble methods are essentially simple regularized logistic regression models that operate on top of this. The performance of the ensemble methods is evocative of the upper bound of information present within these signals if they were combined optimally.

  Bridle, John. "Training stochastic model recognition algorithms as networks can lead to maximum mutual information estimation of parameters." Advances in neural information processing systems 2 (1989).

Actionable Thresholds for engineering

This is an excellent point, and engineers looking to deploy this in production have raised this concern with us previously. This is indeed a challenging problem that has been extensively studied in selective decision making regarding how to choose the appropriate risk threshold.

Our use of the Area Under the Risk-Coverage Curve (AURC), Error at threshold, and associated metrics are specifically designed to address this. The Risk-Coverage curve itself provides a visualization of the trade-off between risk (error rate) and coverage (percentage of problems answered). An engineer can use this curve directly as a decision-making tool:

• For safety-critical domains, an engineer could choose a point on the curve with a very low error rate, accepting a higher abstention rate (and thus more human oversight).
• For less critical applications (e.g., a programming assistant), they could select a point with higher coverage to maximize automation, tolerating a moderately higher error rate.

To present the complete picture in our evaluations, we evaluate our method in a threshold-agnostic manner using AURC. The AURC score summarizes the quality of this trade-off across all possible thresholds, with our scores consistently outperforming all known methods.

Concluding Request

Once again, we thank you for your highly positive and constructive review. In light of these clarifications and new experiments, would you please consider improving your rating to a strong accept? This would allow us to highlight this work in a spotlight or oral presentation. Please let us know if there are any concerns we have not addressed in sufficient depth. We would be happy to provide further clarification.

Thank you for your thorough evaluation of our manuscript and constructive feedback. We appreciate your recognition of the strengths, including the timeliness of the problem, the novelty of using PCFGs for UQ in autoformalization, and the systematic nature of our evaluation. We incorporated your feedback to improve our paper.

1. On Presentation and Clarity

We have addressed the readability concerns by:

On "Rigorous Standards": Thank you. We agree this phrase requires more context; therefore, we will remove that part of the sentence while maintaining the citation to Chen et al. (2022) that describes selecting only the highest-probability output. The sentiment of our original statement was not that we are improving formal verification itself, but rather providing a missing piece: insight into the quality of autoformalizations generated due to the probabilistic nature of LLMs.

On Technical Density, consolidating signals from data, and Theorem 1: We acknowledge the dense writeup and have addressed this as follows:

1. Theorem 1: Theorem 1 provides the theoretical underpinning for our sampling-based approach. It connects the number of samples (N) to the grammar's entropy, providing a probabilistic bound that our 100 samples are sufficient to cover the meaningful regions of the LLM's vast output space. It justifies why our method is sound. We have added the following explicit sentence in Section 2 to connect the theorem back to our methodology: "This theorem provides the theoretical guarantee that a sufficiently large sample set N can effectively represent the LLM's output distribution, justifying our use of samples to infer a representative PCFG."

2. Technical density and consolidating signals: We have adopted a simplified taxonomy with additional details to make the measures section more accessible: (1) Information-theoretic Measures, (2) Structure-based measures/Spectral properties, (3) Static measures of grammar structure, (4) Self-consistency-based measures, (5) Ensemble-based measures. Lines 282-286 have been restructured for clarity.

3. We have also more explicitly defined and enumerated our key takeaways from our result tables in the writeup. Adding this additional clarity was easy since the camera-ready version allows us one additional content page.

Enumeration of Metrics & MLE: We apologize for the confusion regarding MLE. MLE is not a UQ metric; it is the method used to estimate the probabilities of the PCFG rules from the sample set. The UQ metrics are then calculated from this estimated PCFG. We will clarify this distinction. Bayesian and neural approaches to PCFG estimation are useful when incorporating contextual information, such as in low-data paradigms, expert information encoded via Bayesian priors, or natural language semantics obtained via text embeddings. While we explored these techniques and mentioned them briefly, we decided not to run extensive experiments as it would detract from the core focus of UQ in this paper. We have removed the sentence, as you noted it adds unnecessary complexity to the narrative. It will still be available to users, when we open-source the code.

2. On Missing Experimental Details

• Z3 Solver Runtime: We added these performance details

The overhead of using Z3, PCFG extraction, and analysis is minimal, as it primarily involves efficient parsing (using ANTLR) and frequency counting (Maximum Likelihood Estimation) over a fixed set of 100 samples. Our experiment pipeline is dominated by LLM inference time, not solver time or UQ calculations. We also implemented a 30-second timeout for Z3 while running our experiments, so for those anomalous cases where the LLM writes faulty SMT programs that run too long (none of our questions across all 4 datasets should require that much time), they are terminated, and the LLM is asked to generate a new program.

Choice of N=100 and PCFG Size:

We chose to generate N=100 samples because that was heuristically the maximum number of samples we could afford within our compute budget. We needed to sample extensively because we did not constrain the LLM-based SMT generation. We made this choice because we wanted to observe how LLMs behave with minimal prompt engineering while generating valid SMT code.

This approach should work at N=50 or fewer samples as well. As you reduce the number of samples, you may want to constrain: (1) the theories that can be used in your SMT programs (LIA, RA, etc.), (2) use multi-stage autoformalization pipelines, where the first stage is variable definition generation. This way, generated SMT constraints will only use previously defined variables in the pipeline, reducing the need for extensive sampling. Without these constraints, a smaller N (e.g., 5-10) would likely result in less stable estimates of rule probabilities, potentially weakening the UQ signal.

Regarding the size of the PCFG: Here are some summary metadata statistics of a generated PCFG on ProofWriter, which had the longest SMT programs generated from 100 SMT programs in response to a single question: Total Rules = 63,202, Unique rules = 42, Non-terminals = 24, Maximum probability observed among unique rules = 1.0, Minimum probability observed for a unique rule = ~0.00035, Average probability across unique rules = 0.5714.

Shorthand 'SC': Yes, 'SC' stands for Self-Consistency, and we have now ensured it is defined upon its first use. Thank you for pointing this out.

3. On the Nature of Sampling-Based UQ

Reviewer's Question: "Can it happen that LLM produce the correct translation if you ask for one translation, but because you ask for 100 translations, it might produce a lot of wrong ones? In this case, it seems that the approach puts way more weights on translations that are wrong."

This is an excellent question! We want to clarify that we do not ask the LLM to generate 100 translations in one prompt. We repeatedly sample one translation 100 times to obtain our 100 SMT programs. No context from the previous LLM call are carried forward to the next LLM call for the sake of fair and distinct autoformalization generations.

We would like to describe the intuition as follows: imagine running inference on a CNN with the same image 100 times. If you get 10 different answers, you would conclude that there is significant uncertainty in the model output, correct? Similarly, our goal is to assess the LLM's confidence. If a model produces one correct translation but 99 syntactically diverse (and potentially incorrect) alternatives, our PCFG will capture this high diversity, resulting in high grammar entropy. This high entropy signals low model confidence or high uncertainty.

A confident, reliable model would generate 100 programs that are generally syntactically equivalent or very similar and canonical, leading to low entropy. Therefore, our approach does not "overweight" wrong translations; it correctly interprets a scattered, diverse output distribution as a sign of unreliability. This is the risk we aim to flag for the user.

4. Enumeration of all measures

You can find an enumeration of all 25 uncertainty measures we benchmarked in the 25 rows of Tables 3, 4, etc. For your reference, in case you have detailed questions about how we implemented and/or calculated these measures, we describe them shorthand below. We will also add these details to the appendix:

1. Grammar Entropy (nonterminals)

2. Perplexity (from #1)

3. KL Divergence(vs uniform)

4. NSUI: grammar_entropy/max_entropy) * (spectral_radius/(1+spectral_radius))

5. Renyi Ent (2)

6. Renyi Ent (0.5)

7. Max Ent: weighted Σlog2(num_rules) per nonterminal

8. Ent Ratio: grammar_entropy/max_entropy (normalized entropy in NSUI)

9. Spectral Factor: spectral_radius/(1+spectral_radius) (normalized spectral in NSUI)

10. Spectral Radius: largest eigenvalue of dependency graph Jacobian

11. # Nonterminals: unique LHS symbols

12. # Rules: total count

13. Avg Rules / # NT:

14. Avg RHS Len

15. Max Branch Factor: max alt rules per nonterminal

16. Rule Dist Mean

17. Rule Dist StdDev

18. Rule Dist Skew

19. Rule Dist Kurtosis

20. Self Consistency Text: fraction agreeing with majority text ans

21. Self Consistency SMT: fraction agreeing with majority SMT ans

22. Ensemble Average: arithmetic mean of normalized uncertainty

23. Ensemble Weighted: correlation-weighted avg (squared correlations)

24. Ensemble ML:LogisticRegression on scaled features $negated grammar\_entropy, perplexity, spectral\_radius, nsui, spectral\_factor, kl\_divergence, max\_entropy, smt\_consistency$

25. Ensemble Simple: (1-norm_grammar_entropy)*0.33 + (1-norm_spectral_radius)*0.33 + smt_consistency***0.34

Rebuttal word limits restrict our description length, but we are happy to discuss further!

Concluding Request

We believe we have comprehensively addressed all identified weaknesses. Given these detailed responses and improvements, would you please consider increasing your rating to accept or strong accept? We're happy to address any additional questions.

Thank you for your feedback and for recognizing the key strengths of our work, including our novel use of probabilistic formal grammars for uncertainty quantification and the valuable integration of formal methods with LLMs. We appreciate your acknowledgment of our innovative spectral and information-theoretic measures, which validates the core novelty of our approach.

We hope to address your concerns and demonstrate the value of our contribution through this rebuttal. We welcome further engagement as we work to convey the novelty of our approach to all readers.

1. On Novelty and Relation to Prior Work (Weaknesses 1 & 3)

Concern: "There is a rich body of work that uses formal grammars at inference time without probabilities. The paper does not adequately discuss these approaches or builds the results of this work in context of these earlier methods."

Our Response: Our paper's core novelty lies not in merely using a grammar, but in using a Probabilistic Context-Free Grammar (PCFG) to model the LLM's entire output distribution for a given question for the purpose of UQ. This is a fundamental departure from prior work that uses grammars deterministically for constrained decoding. Although we believe these areas are not directly related, as per your suggestion we are adding a paragraph on known usage of grammars at inference time to our related works section.

Here is why we are different from prior work: Constrained decoding modifies the LM head by zeroing out probabilities of tokens that are invalid based on the known language (e.g., JSON) grammar. This is not feasible with commercially available, non-open-weight frontier LMs that we focus on in this paper. Furthermore, this approach is not related to our task of UQ, since LLMs can reliably generate syntactically valid SMT in our experiments. To clarify our position:

• Our Contribution is Probabilistic UQ, Not Constrained Decoding: As stated in our central thesis (Page 1), "Existing methods often ignore this $probabilistic uncertainty$ by selecting only the highest-probability output $token$ ... a simplification that we argue undermines the rigorous standards required for formal reasoning." Our work directly addresses this simplification. We do not merely ensure outputs are syntactically valid; we analyze the statistical patterns within an ensemble of valid outputs to quantify the model's uncertainty.

• Explicit Discussion in Related Works: Our Related Works section (Section 4) currently situates our work appropriately within the task of UQ. We discuss the use of PCFGs in various domains and explicitly state, "Our work extends PCFG inference... to verification artifacts" (Page 9). The novelty lies in applying this probabilistic framework to diagnose LLM reasoning failures, which, to our knowledge and according to all three other reviewers, represents a completely new direction.

2. On the Aptness of the Title and Scope (Weakness 2)

Reviewer's Concern: "The title 'Grammars of Formal Uncertainty' is not apt as the paper does not build grammars of formal uncertainty. Similarly, the broad mention of automated reasoning tasks leaves the strong ties that the paper has to SMT methods..."

Our Response: We believe the title is both apt and evocative of our contribution.

• On the Title: The grammar serves as the instrument through which we structure, model, and measure the uncertainty inherent in the LLM's formal outputs. The PCFG, with its rule probabilities learned from the LLM's own generations, becomes a "grammar of formal uncertainty", a formal object that describes the LLM's autoformalization confidence and confusion. This is not merely semantic.

• On the Scope: We are transparent that our experiments are instantiated using the SMT-LIB standard. We state this explicitly in our methodology (Section 2): "...we adopt the stable, widely supported SMT-LIB standard as a common intermediate representation..." This is a methodological choice to ground our framework in SMT, a powerful, standardized, and representative sub-domain of automated reasoning used in real-world automated reasoning production systems and prior publications that employ SMT solvers.

  To illustrate our point, please see: A billion SMT queries a day, Amazon Science, FLOC 2022.

  The framework itself is general. The PCFG-based UQ approach can be applied to any formal language for which a grammar can be defined, as we demonstrate in our rebuttal pilot study to reviewer yS8U, where we show our method is easily extensible to Prolog (similar to first-order logic). SMT is our primary case study, not a fundamental limitation of the method**.**

3. On the Contribution of Theorem 1 (Weakness 3 & Question 1)

Reviewer's Concern: "Theorem 1... is a straightforward result that can be proved directly from the definition of entropy... Appropriate citations should be provided for each of the steps, such as T. M. Cover and J. A. Thomas, Elements of Information Theory."

Our Response: We agree that Theorem 1 builds upon foundational principles of information theory, and we thank the reviewer for the suggestion. We have gladly added a citation to Cover and Thomas to acknowledge the classical roots of typical set arguments.

However, by dismissing this as "straightforward" you are overlooking its important role in our paper. The theorem's contribution is not a claim of inventing a new mathematical principle, but its novel application and contextualization. It provides the first formal, theoretical bridge, to our knowledge, between:

1. The number of samples (N) drawn from an LLM.
2. The Shannon entropy (H(µ)) of the LLM's output distribution.
3. The probabilistic bound of covering the space of possible formal programs.

This theorem provides the theoretical justification for our sampling-based UQ methodology. It demonstrates why analyzing an ensemble of outputs is a principled way to understand the model's uncertainty over the entire generation space. Its value is in its application, not its elementary nature. We will make this more clear in the paper.

4. On the Experimental Methodology (Weakness 4 & Question 2)

Reviewer's Concern: "It is not clear if the probabilities in the PCFG are obtained from a different data set than the UQ measures obtained during analysis. If the train and test set come from the same data set, the UQ methods will not generalize..."

Our Response: We believe this concern stems from a misunderstanding of our experimental design, which we will make more explicit in our methodology. Our methodology operates at the instance level, not through a traditional train/test split, and this is a core feature of our contribution.

As detailed in Appendix D, "For each of the selected questions, a unique PCFG was induced from its corresponding 100 SMT samples."

To be unequivocally clear:

1. For a single input question, we prompt the LLM to generate an ensemble of N=100 formal (SMT) programs.
2. From this specific ensemble of 100 programs, we induce a per-question PCFG.(each PCFG is independent of other PCFGs).
3. The UQ measures (entropy, spectral radius, etc.) are calculated from this instance-specific PCFG. For 21 of these measures (Table 3, rows 1-21), no learning occurs. Only our 4 ensemble-based techniques (Table 3, rows 22-25) learn how to weight each of these 21 measures to produce a better uncertainty signal and understand the total signal present among the metrics.
4. These UQ metrics are then used to predict the correctness of the answer for that same single input question.

There is no "training set" from which PCFG probabilities are learned and a "test set" on which they are applied. Your concern about generalization is misplaced because the goal is not to build a global PCFG model,, but to assess the LLM's uncertainty on a case-by-case basis. This instance-specific analysis is allows our method to provide confidence scores for each new autoformalization problem an LLM encounters.

5. On the Discussion of Efficacy and Risk (Limitations)

Reviewer's Concern: "The effiicacy of UQ metrics and risk of incorrect applications may be better discussed."

Our Response:

• Efficacy: We are puzzled by the limitation comment on efficacy, as a significant portion of our Results section (Section 3) and Appendix is dedicated to a rigorous, multi-faceted evaluation of efficacy and risk. We evaluate 25 different metrics using AUROC, ECE, AURC, Brier scores and more across multiple models and datasets (Tables 3, 4, and 10-17). This constitutes a direct and comprehensive assessment of efficacy.

• Risk of Incorrect Applications: We’d love to clarify this. The entire premise of our selective prediction analysis is to manage this risk. We use the Area Under the Risk-Coverage Curve (AURC) and explicitly report the error rate at optimal abstention thresholds (Err@T) and the resulting Relative Error Reduction (RelErrRed). For instance, for 03-mini on ProofWriter, we demonstrate that our method enables "filtering nearly all errors by abstaining on a minute fraction of outputs" (Page 7), achieving a 100% error reduction (Table 12). This is not a peripheral point; it is a central result of our paper and a direct, quantitative discussion of managing the risk of incorrect application.

Concluding Request

We believe we have addressed all identified weaknesses and questions in detail. In light of these comprehensive responses, would you please consider increasing your rating to an accept?

We would be happy to address any additional questions you may have. Thank you for your thorough review.

We thank you for your thoughtful and constructive comments. We are happy to hear that you recognise the importance of the problem we address, and the novelty of applying PCFGs for uncertainty estimation. We find the questions you have raised to be very insightful and have ultimately led us to strengthen our paper.

We address each point below:

1. On Syntactic vs. Semantic Uncertainty (Weakness 1 & Question 1)

Our Response: Thanks for pointing this out. We conducted the experiments you requested, and here are the results.

Additional results for Table 2: Semantic uncertainty quantification metrics for detecting autoformalization errors with respect to ground truth using DeepSeek-v3-0324 across datasets. Entailment checking was performed using independent prompts to DeepSeek-v3-0324, comparing the generated SMT code with the question as prior context. The uncertainty-aware abstention metrics reflect how the model can selectively answer questions by applying an optimal uncertainty threshold (Opt.Thresh) to withhold answers on uncertain questions, minimizing error rate (Err@T) and maximizing error reduction (RelErrRed) compared to answering all questions.

While we observe moderate performance on a few configurations, and near-random performance on the rest, we can conclude that semantic uncertainty does not distinctly capture the epistemic uncertainties in autoformalization. We would also note that the artificially high AUROC on FOLIO comes from the fact that the LLM autoformalizations are disproportionately composed of errors. To better contextualize the understanding of high AUROC, but poor performance here, we must observe the high AURC value, corresponding with a high risk, in spite of holding out on most uncertain decisions.

We would also like to note here that we ran the same experiments with `nli-deberta-v3-large` as the model, similar to Kuhn et al, and all performance metrics, across all datasets, were close to random guessing. This is because `nli-deberta-v3-large` models have not seen formal structured artifacts, such as SMT code in their training data, and therefore, cannot appropriately judge entailment over them.

Intuition on why our technique works : As we mentioned in our paper, our central thesis is that syntactic typicality is itself a powerful, computationally tractable, and previously underexplored signal for identifying semantic errors (pg 8). When an LLM is confident and "understands" a problem, it tends to generate programs from a narrower, canonical part of the grammar. When it is uncertain, it explores more varied and statistically anomalous syntactic structures. This "syntactic fingerprint" of failure is what our PCFG framework is designed to detect, and our results prove that this works well.

We also believe that although LLMs have learnt to generate passable syntactically correct structures in SMT, they still make mistakes in autoformalization, akin to early LLMs generating valid but logically unsound python code. These same mistakes hold for LLMs judging formal artifacts for entailment too (hence semantic entropy captures low signal about the uncertainty towards incorrectness). We believe that as these models get better over time, these mistakes will be reduced, and UQ methods such as semantic entropy will start working better.

Efficiency:

Another key advantage of our method is its efficiency when there is large-scale sampling of formal artifacts from the LLM. With semantic-entropy based metrics, there need to be (M choose 2)-comparisons between generated autoformalizations to check entailment, which combinatorially explodes at large values of M. Similarly, verifying semantic equivalence between two arbitrary SMT programs is, in general, an undecidable problem. While approximations exist, they are often computationally expensive. Our approach, based on parsing and frequency counts, is lightweight and can be applied at scale on a per-instance basis.

2. On Clarity of Figures and Tables (Weakness 2)

Our Response: We appreciate this constructive feedback. We acknowledge that the initial version of Figure 1 was dense. In response, we have redesigned it to be more intuitive and readable. Due to the text-only format of this rebuttal this year, we cannot display the new figure here or update the PDF, but we have implemented the following improvements for the final version:

• There is now a clearer layout, and the figure is now structured into distinct stages (LLM Sampling > PCFG Parsing & Learning > Uncertainty Calculation > Prediction), guiding the reader through our pipeline.
• The (confusing) pie chart has been removed, and the bar chart showing rule frequencies is simplified now uses a consistent and explicitly labeled color-coding scheme We have also enlarged all text elements for readability.

We have also noted your concern about the need for abstraction of uncertainty metrics, and have incorporated the following simplified abstracted taxonomy : (1) Information-theoretic Measures (2) Structure based measures/ Spectral properties (3) Static measures of grammar structure (4) Self consistency based measures (5) Ensemble-based measures. Moreover, adding this additional clarity was easy since the camera-ready version allows us one additional content page.

3. On Sample Quality and Temperature (Question 2)

Our Response: This is a great question. We investigated this in our ablation studies, the results of which are detailed in Appendix B (Temperature-Varied SMT Generation and PCFG Analysis, pages 18-20) available in the supplementary material zip file. Our empirical analysis shows that our PCFG-derived metrics are robust across the temperature spectrum. We found that grammatical properties exhibit smooth and predictable changes in response to temperature, rather than chaotic behavior or sharp phase transitions.

For example, as shown in Figure 3 (Page 19), grammar entropy increases predictably with temperature, reflecting the increased diversity of the samples. This also helps confirm that our metrics are sensitive and correctly capture the changing nature of the LLM's output distribution with respect to temperature.

Varying parameters like temperature do not harm the quality of the PCFG. The PCFG merely probabilistically models the production rules from the grammar, irrespective of temperature, or distribution of temperatures samples are drawn from. In fact, all our UQ experiments involve SMT & Text generation by sampling (N=100 times) with a uniform distribution at temperatures between 0.1 and 2.0, a detail we will add to our appendix.

4. On the Number of Samples Used (Question 3)

Our Response: Thanks for bringing this up, because it highlights a point we must make more explicit. We do mention 5 samples, but this was for a different part of our analysis. Our experimental setup has two stages:

1. Initial Benchmarking (N=5): In Section 3 (Page 6), we first establish the baseline performance of Text vs. SMT reasoning. For this high-level comparison (Table 1 and appendix tables 5-9), we used N=5 samples per question.
2. UQ Analysis (N=100): For our core contribution, the PCFG-based uncertainty quantification, we used a much larger corpus of N=100 SMT samples per question. This larger ensemble is necessary to induce a statistically meaningful PCFG for each reasoning instance. This is explicitly stated in Appendix D (Page 29): "a corpus of NSMT​=100 SMT-LIB v2 program samples per question was generated."

We apologize for the confusion and have added a sentence in Section 3.1 to explicitly differentiate the sample sizes used for the initial benchmarking versus the main UQ analysis.

Additional note on Strength 1: Thank you for pointing out Li et al 2024,”Guiding enumerative program synthesis..” we have highlighted that paper in our related works section.

Concluding Request

We believe we have addressed all identified weaknesses and questions in detail. May you please increase our rating upwards towards an accept or strong accept? We are happy to answer any more questions you may have. Thank you for your review.