Pith. sign in

REVIEW 4 major objections 4 minor 1 cited by

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

T0 review · 4 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper shows that syntactic atypicalities in LLM-generated SMT-LIB programs are measurable signals of semantic errors, and that fusing these grammar-derived uncertainty signals with lightweight machine learning lets a verification…

desk verdict The PCFG uncertainty metrics are a plausible direction, but the headline fusion claim is in-sample and needs a proper held-out evaluation before it can be trusted. read the letter →

arxiv 2505.20047 v1 pith:OSW2PBQN submitted 2025-05-26 cs.CL cs.AIcs.LOcs.SE

Debargha Ganguly , Vikash Singh , Sreehari Sankar , Biyao Zhang , Xuecen Zhang , Srinivasan Iyengar , Xiaotian Han , Amit Sharma
show 2 more authors
Shivkumar Kalyanaraman Vipin Chaudhary
This is my paper
classification cs.CLcs.AIcs.LOcs.SE
keywords largelanguagemodelsuncertaintyquantificationprobabilisticcontext-freegrammarSMT-LIBautoformalizationselectiveverificationformalreasoningsyntactictypicality
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Large language models can write formal specifications, but a probabilistic generator feeding a deterministic verifier creates a trust gap: a wrong formalization can pass through a sound solver. This paper argues that the gap is bridgeable because LLM uncertainty leaves measurable traces in the formal artifacts themselves. By modelling ensembles of LLM-generated SMT-LIB programs with a probabilistic context-free grammar, the authors extract 25 uncertainty metrics, find that grammar entropy flags reasoning errors on a logic task with AUROC above 0.93, and show that fusing these signals lets a pipeline abstain on the riskiest outputs and cut error rates by 14-100% with minimal abstention. If this holds, formal verification workflows can route LLM outputs to solvers and human reviewers based on predicted reliability rather than verifying everything or nothing.

What carries the argument

The machinery is a probabilistic context-free grammar induced from an ensemble of N=100 LLM-generated SMT-LIB programs per question, parsed with the standard SMT-LIB v2 grammar. Rule probabilities are estimated by maximum likelihood with Lidstone smoothing, and the resulting per-question PCFG yields a suite of metrics: grammar entropy and perplexity, Rényi entropies, KL divergence from uniform, spectral radius of the mean matrix, a composite NSUI score, and distributional statistics such as rule kurtosis, plus text and SMT self-consistency. These metrics quantify where the LLM's rule choices spread, recurse, or switch between terse and verbose styles; the paper's key move is treating those measured irregularities as a 'syntactic fingerprint' of reasoning failure and then fusing the metrics with a lightweight logistic regression (Ensemble ML) for selective abstention.

What would settle it

Freeze the Ensemble ML weights and the optimal abstention threshold on a training set of 100 questions, then measure AUROC and relative error reduction on a separate held-out question set from the same datasets; if performance collapses toward chance, the selective-verification claim loses its empirical support.

Watch

Extended reading notes

Core claim

The central claim is that syntactic atypicality in LLM-generated formal artifacts is a potent, quantifiable signal of underlying semantic error. When a model truly understands a logical relationship it tends to produce high-probability rule sequences; when it misunderstands, the generated SMT-LIB programs become statistically anomalous in ways the grammar exposes. The paper reports that these PCFG-derived signals are task-dependent — grammar entropy and related structural metrics nearly perfectly separate correct from incorrect o3-mini outputs on ProofWriter (AUROC 0.93, AURC 0.0008), while knowledge-intensive tasks like StrategyQA are better served by cross-modal agreement between the SMT formalization and the model's textual reasoning. A lightweight, model-agnostic fusion of these signals into an ensemble predictor (logistic regression over the metric vector) outperforms individual metrics and enables selective verification that reduces errors by 14-100% with minimal abstention.

Load-bearing premise

The load-bearing premise is that the logistic-regression weights and abstention thresholds fitted on the same 100-question sets used for evaluation continue to work on new questions the model has not seen.

Editorial extensions

If this is right

  • Verification pipelines can rank LLM-generated SMT-LIB programs by predicted correctness and send only a small risky fraction to a solver or human reviewer, cutting cost while preserving soundness.
  • Because the best signal differs by task, deployed systems should either select task-specific metrics or learn to combine them rather than relying on one universal uncertainty score.
  • The asymmetric text/SMT self-consistency result implies that LLMs may reason through formal and textual pathways that are not aligned, so improving alignment (for example by joint training) should improve both accuracy and uncertainty estimation.
  • The grammar-based approach is model-agnostic: a new LLM only requires resampling and reparsing to re-estimate rule probabilities, with no changes to the grammar or metric definitions.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial extension: the reported AUROC and error-reduction numbers are computed on the same 100-question sets where the Ensemble ML weights and abstention thresholds were chosen (Appendix D), so the transfer of these numbers to unseen questions is a testable open question rather than an established result.
  • Editorial extension: the same PCFG construction should transfer to other structured formal outputs, such as Lean or Coq proof scripts or verification-condition lists, where grammar entropy could similarly flag semantic missteps; that transfer is a natural next experiment.
  • Editorial extension: the temperature ablations show that sampling temperature changes the baseline PCFG statistics, so production systems should fix and document their sampling temperature before applying any threshold learned under another temperature.
  • Editorial extension: an immediate stress test is to flip the evaluation from within-dataset question splits to cross-dataset or cross-LLM deployment, where the syntactic fingerprint may or may not retain its discriminative power.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 4 minor

Summary. The paper proposes modeling distributions of LLM-generated SMT-LIB programs with Probabilistic Context-Free Grammars (PCFGs), deriving a suite of grammar-based uncertainty metrics, and fusing them (including a logistic-regression 'Ensemble ML') to enable selective verification of formal artifacts. The empirical study covers five LLMs on four reasoning datasets, reporting task-dependent AUROC values (e.g., 0.93 for grammar entropy on o3-mini/ProofWriter) and claiming error reductions of 14–100% with minimal abstention. The paper also states a theoretical coverage guarantee (Theorem 1) and a temperature-based ablation analysis. The methodological core—using syntactic typicality of formal outputs as a signal for semantic error—is interesting, but the headline selective-verification result is not established by the reported experiments.

Significance. If the claims were validated out-of-sample, the work would be a valuable contribution: it offers a model-agnostic, lightweight way to rank LLM-generated formal artifacts by predicted correctness before invoking a solver or human review, and it provides a structured taxonomy of uncertainty signals tied to grammar properties. The raw unsupervised findings (e.g., grammar entropy achieving high AUROC on ProofWriter) are genuinely intriguing and could guide future work on neurosymbolic verification. The paper also ships detailed tables and an appendix with experimental settings, which aids reproducibility. However, the central selective-verification claim rests on an evaluation protocol that confounds fitting and evaluation, and the unit-of-analysis is ambiguous; as presented, the quantitative headline numbers are not reliable evidence of transferable performance.

major comments (4)
  1. [Appendix D / §3.1 / Tables 10–17] The central claim of 14–100% error reduction is based on fitting both the Ensemble ML logistic regression and the optimal abstention threshold on the same 100-question data used to report AUROC and RelErrRed. Appendix D states that 'optimal abstention thresholds were determined by targeting maximum relative error reduction' and that the logistic regression is 'trained for up to 10,000 iterations on scaled features derived from the suite of PCFG uncertainty metrics,' with no held-out split, cross-validation, or calibration procedure described. With roughly 25 input features and 100 questions, this is in-sample optimization, so the reported AUROC and error-reduction figures are optimistic upper bounds at best. The transferable claim in the Abstract and Discussion is therefore not supported. The authors should add a proper train/validation/test split (e.g., cross-validation at the question level) and report out-of-sample numbers, or explicitly re-frame the current numbers as training-set diagnostics.
  2. [§2.1 / §3.1 / Appendix D] The unit of analysis is ambiguous and likely invalid for the reported per-sample selective-prediction results. The PCFG metrics are computed per question: one PCFG is induced from the 100 SMT samples of a question, yielding a single feature vector per question. Yet the evaluation is described and tabulated per SMT program sample (e.g., 'abstaining on just 5% of samples'). All 100 samples from the same question then share identical features, so the effective number of independent observations is 100, not 10,000, and the reported abstention curves conflate question-level and sample-level decisions. The authors should clarify the unit of analysis; if sample-level prediction is intended, they need sample-level features (e.g., per-sample parse-tree probability under the per-question PCFG), or they should evaluate question-level abstention with an appropriate statistical treatment.
  3. [§3.1 vs Appendix B] There is a direct contradiction about the temperature behavior of the spectral radius. Section 3.1 states that 'PCFG spectral radius from LLM-generated SMT-LIB programs consistently decreases with sampling temperature,' while Appendix B states that 'the PCFG spectral radius generally trended upwards with increasing temperature.' Both cannot be true, and the discrepancy is not discussed. The authors should correct one of the statements, verify which trend holds in the data, and align the ablation conclusions in the main text with the appendix.
  4. [Theorem 1 / Appendix A.1] The proof of Theorem 1 is mathematically invalid. Step 1 asserts that the set of atoms with probability at least 2^{-H(µ)} has mass at least 1/2; this is false in general. For example, a distribution with one atom of mass 0.6 and 2^m atoms each of mass 0.4/2^m has entropy ≈ 0.97 + 0.4m, and for sufficiently large m no atom has probability ≥ 2^{-H(µ)}, so the claimed high-probability set is empty. The subsequent union bound over 'at most 2^{H(µ)} atoms' is also unjustified. The theorem's statement and the derived ln(N)/N rate are therefore not established. The authors should either provide a correct proof or remove or qualify the theorem.
minor comments (4)
  1. [§1 / §2 / Table 2] The claim that 'known UQ techniques like the entropy of token probabilities fail' is based entirely on DeepSeek-v3-0324, the only model for which token logprobs are available; this limitation should be stated prominently where the claim is made, and the model name appears inconsistently as 'DeepSeek-v3-0324' and 'DeepSeek-v3-04-21' in different places.
  2. [Table 12 / §3.1] Several entries report Err@T = 0.0000 and RelErrRed = 1.0000 at abstention thresholds of 0.05 or 0.10; with only 100 questions (or 10,000 samples but 100 independent units), such perfect error elimination after abstention should be accompanied by exact error counts and, ideally, confidence intervals.
  3. [Figure 1] The caption states that 'No synthetic or simulated data is used,' but the figure appears to present aggregate measurements and derived PCFG rule frequencies; please clarify what is measured versus what is computed from the LLM outputs.
  4. [References] Several reference entries have malformed URLs, such as 'URLhttps://arxiv.org/abs/2310.06825.' and 'URLhttps://arxiv.org/abs/2203.11171.'; please fix the formatting and ensure all URLs are complete.

Circularity Check

2 steps flagged · score 6.0 of 10

Selective-verification results are in-sample fitted values: Ensemble ML weights and abstention thresholds are fit on the same 100-question corpora used to report AUROC and error reductions.

  1. fitted input called prediction [Appendix D (Supplementary Experimental Details); results reported in Section 3.1 and Tables 10\u201317.]
    "In the analysis of selective prediction utility (error vs. abstention), optimal abstention thresholds were determined by targeting maximum relative error reduction while considering abstention levels up to a practical maximum of 50%. For our Ensemble ML predictor, a Logistic Regression model was employed, configured with balanced class weights and trained for up to 10,000 iterations on scaled features derived from the suite of PCFG uncertainty metrics."

    The paper's headline claim that lightweight fusion 'enables selective verification' and 'cut[s] error rates by 14-100%' is supported by AUROC, Err@T, and RelErrRed values computed on the same 100-question datasets used to fit the logistic-regression weights and to select the abstention thresholds. No held-out split, cross-validation, or separate calibration set is described. The logistic regression is trained to predict errors on these questions, so the reported discrimination and error-reduction numbers are training-set performance estimates. The 'prediction' of selective-verification benefit is therefore not an independent out-of-sample result; it is the fitted model's in-sample score.

  2. self definitional [Caption of Table 2 and Appendix D; summarized in Abstract and Section 3.1.]
    "The uncertainty-aware abstention metrics reflect how the model can selectively answer questions by applying an optimal uncertainty threshold (Opt.Thresh) that minimizes error rate (Err@T) and maximizes error reduction (RelErrRed) compared to answering all questions."

    The caption defines RelErrRed as the value obtained by applying the optimal uncertainty threshold, and Appendix D states that thresholds are chosen by 'targeting maximum relative error reduction' on the same 100-question corpus. Thus the reported 14-100% error reductions are, by construction, the optimized in-sample value of the objective used to pick the threshold. The abstract presents these optimized training-set values as a general capability ('enables selective verification, drastically reducing errors'), but the evaluation is not independent of the selection rule.

full rationale

The PCFG framework itself is not circular: the grammar is the standard SMT-LIB grammar, rule probabilities are estimated by MLE from generated programs, and the standalone metrics such as grammar entropy are computed directly from those estimates. The reported grammar-entropy AUROC of 0.9301 for o3-mini on ProofWriter is a legitimate measurement on the collected 100-question corpus, though selecting the best of 25 metrics post hoc is a multiple-testing caveat rather than circularity. The paper's citations to the authors' prior work are analogical and not load-bearing. However, the central selective-verification claim depends on two fitted components: the Ensemble ML logistic-regression weights and the optimal abstention thresholds. Appendix D specifies that both are determined on the same 100-question corpora used to report AUROC and relative error reduction, with no held-out split or cross-validation. Consequently, the headline error reductions are in-sample values of the fitted model and threshold-selection objective, not predictions on new questions. This is partial circularity of the 'fitted input called prediction' form; the standalone PCFG uncertainty signals retain independent content, so the overall score is 6 rather than higher.

Assumptions & free parameters 4 free parameters · 5 assumptions · 0 invented entities

The central claim rests on a PCFG approximation of LLM output distributions, which requires assumptions of measurability, positive mass on valid programs, and i.i.d. sampling. The fusion result additionally depends on weights and thresholds fitted to the evaluation data. No new physical entities are introduced.

free parameters (4)
  • Lidstone smoothing constant beta_s = 1
    Laplace smoothing constant used in MLE of PCFG rule probabilities; chosen by hand and affects all derived metrics.
  • Number of samples per question N = 100
    Corpus size for PCFG estimation; chosen by hand; governs the fidelity of the approximation to the LLM distribution.
  • Logistic regression weights in Ensemble ML = learned in-sample
    Fitted to the same 100-question evaluation sets; no held-out split or cross-validation is described.
  • Optimal abstention threshold Opt.T = varies (e.g., 0.05 to 0.50)
    Selected on the evaluation data to minimize error rate; the reported error reductions depend on this post hoc choice.
assumptions (5)
  • domain assumption The SMT-LIB language L_SMT is measurable in the cylinder sigma-algebra and is approximated by its standard CFG G_SMT
    Invoked in Section 2 Problem Setup; needed to define the conditional measure mu_{T,theta,SMT}.
  • domain assumption mu_{T,theta}(L_SMT) > 0, i.e., the LLM assigns positive probability to valid SMT-LIB programs
    Stated in Section 2 as 'reasonable and empirically validated'; required for the conditional measure to be well-defined.
  • domain assumption The N generated SMT-LIB programs are i.i.d. samples from mu_{T,theta,SMT}
    Used to justify MLE convergence via the law of large numbers (Section 2, Approximation); actual sampling uses retries and fixed temperature.
  • standard math A PCFG defines a consistent probability measure iff the spectral radius of its moment matrix is at most 1
    Invoked in Section 2 without citation; standard result in PCFG theory but should be referenced.
  • standard math The typical-set argument in Theorem 1: there are at most 2^H(mu) atoms of probability at least 2^{-H(mu)}
    Used in Appendix A.1; the subsequent union bound step is incorrect, so the theorem as stated is not supported.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks." pith.science (2026). https://pith.science/paper/OSW2PBQN

@misc{pith2026250520047,
  author       = {Pith},
  title        = {Pith review of: Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OSW2PBQN}},
  note         = {Machine review of arXiv:2505.20047}
}
read the original abstract

Large language models (LLMs) show remarkable promise for democratizing automated reasoning by generating formal specifications. However, a fundamental tension exists: LLMs are probabilistic, while formal verification demands deterministic guarantees. This paper addresses this epistemological gap by comprehensively investigating failure modes and uncertainty quantification (UQ) in LLM-generated formal artifacts. Our systematic evaluation of five frontier LLMs reveals Satisfiability Modulo Theories (SMT) based autoformalization's domain-specific impact on accuracy (from +34.8% on logical tasks to -44.5% on factual ones), with known UQ techniques like the entropy of token probabilities failing to identify these errors. We introduce a probabilistic context-free grammar (PCFG) framework to model LLM outputs, yielding a refined uncertainty taxonomy. We find uncertainty signals are task-dependent (e.g., grammar entropy for logic, AUROC>0.93). Finally, a lightweight fusion of these signals enables selective verification, drastically reducing errors (14-100%) with minimal abstention, transforming LLM-driven formalization into a reliable engineering discipline.

Figures

Figures reproduced from arXiv: 2505.20047 by the authors.

Figure 1
Figure 1. Analysis of empirically observed LLM-generated SMT-LIB formalizations for the statement [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Spectral Radius VS Temperature [PITH_FULL_IMAGE:figures/full_fig_p019_2.png] view at source ↗
Figure 5
Figure 5. Entropy Ratio vs Temp [PITH_FULL_IMAGE:figures/full_fig_p019_5.png] view at source ↗
Figures from the paper (5 more)
Figure 6
Figure 6. Figure 6: NSUI vs Temp [PITH_FULL_IMAGE:figures/full_fig_p019_6.png]
Figure 8
Figure 8. Figure 8: Perplexity vs Temp [PITH_FULL_IMAGE:figures/full_fig_p020_8.png]
Figure 10
Figure 10. Figure 10: Max Branching Factor vs Temp [PITH_FULL_IMAGE:figures/full_fig_p020_10.png]
Figure 12
Figure 12. Figure 12: Kurtosis vs Temp [PITH_FULL_IMAGE:figures/full_fig_p020_12.png]
Figure 15
Figure 15. Figure 15: SMT vs. Text Error Ratio Analysis for Gemini Flash 2.0: Depicts less-calibrated SMT generation, evidenced by a weaker correlation between SMT and Text error patterns. The figures juxtapose SMT versus Text error ratios (with marginals) for o3-mini ( [PITH_FULL_IMAGE:f…

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. AI4Research: A Survey of Artificial Intelligence for Scientific Research

    cs.CL 2025-07 conditional novelty 4.0 of 10

    A survey that organizes AI-for-research work into five tasks, comprehension, survey, discovery, writing, and peer review, and compiles associated tools and benchmarks.

Reference graph

Works this paper leans on

43 extracted references · 12 canonical work pages · cited by 1 Pith paper

  1. [6]

    Self-consistency improves chain of thought reasoning in language models.arXiv preprint arXiv:2203.11171,

    Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models.arXiv preprint arXiv:2203.11171,

    arXiv

  2. [7]

    URLhttps://aclanthology.org/2021.tacl-1.21/

    doi: 10.1162/tacl_a_00370. URLhttps://aclanthology.org/2021.tacl-1.21/. Abulhair Saparov and He He. Language models are greedy reasoners: A systematic formal analysis of chain-of-thought. InThe Eleventh International Conference on Learning Representations,

    doi:10.1162/tacl_a_00370 2021

  3. [8]

    FOLIO: Natural language reasoning with first-order logic

    Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, Lucy Sun, Alexander Wardle-Solano, Hannah Szabó, Ekaterina Zubova, Matthew Burtell, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, Ansong Ni, Linyong Nan, Jungo Kasai, Tao Yu, Rui Zhang, Alexander Fabbri, Wojciech Ma...

    work page 2024

  4. [9]

    tailedness

    revealed extreme model-specific behaviors under SMT. DeepSeek R1’s SMT output, for instance, correctly identified all 242 false statements (0 FP, 242 TN) but failed to correctly identify any of the 258 true statements (0 TP, 258 FN), indicating a systematic bias in its SMT generation towards unsatisfiability or an inability to complete proofs for satisfia...

    work page 2000

  5. [11]

    To- wards a Mathematics Formalisation Assistant using Large Language Models.arXiv preprint arXiv:2211.07524,

    Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. To- wards a Mathematics Formalisation Assistant using Large Language Models.arXiv preprint arXiv:2211.07524,

    arXiv

  6. [12]

    FIMO: A Challenge Formal Dataset for Auto- mated Theorem Proving.arXiv preprint arXiv:2309.04295,

    Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. FIMO: A Challenge Formal Dataset for Auto- mated Theorem Proving.arXiv preprint arXiv:2309.04295,

    arXiv

  7. [13]

    Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving.arXiv preprint arXiv:2405.01379,

    Xin Quan, Marco Valentino, Louise A Dennis, and André Freitas. Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving.arXiv preprint arXiv:2405.01379,

    arXiv

  8. [14]

    DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data.arXiv preprint arXiv:2405.14333, 2024b

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data.arXiv preprint arXiv:2405.14333, 2024b. Daniel Whalen. Holophrasm: A Neural Automated Theorem Prover for Higher-Order Logic.arXiv preprint arXiv:1608.02644,

    arXiv

Show all 43 references
  1. [16]

    Proving Theorems Recursively.arXiv preprint arXiv:2405.14414,

    12 Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li, et al. Proving Theorems Recursively.arXiv preprint arXiv:2405.14414,

    arXiv

  2. [17]

    Large Language Models’ Understanding of Math: Source Criticism and Extrapolation.arXiv preprint arXiv:2311.07618,

    Roozbeh Yousefzadeh and Xuenan Cao. Large Language Models’ Understanding of Math: Source Criticism and Extrapolation.arXiv preprint arXiv:2311.07618,

    arXiv

  3. [18]

    Experimental Results from Applying GPT-4 to An Unpublished Formal Language.arXiv preprint arXiv:2305.12196,

    Gregor vom Scheidt. Experimental Results from Applying GPT-4 to An Unpublished Formal Language.arXiv preprint arXiv:2305.12196,

    arXiv

  4. [19]

    Large Language Models for Mathematicians.arXiv preprint arXiv:2312.04556, 2023a

    Simon Frieder, Julius Berner, Philipp Petersen, and Thomas Lukasiewicz. Large Language Models for Mathematicians.arXiv preprint arXiv:2312.04556, 2023a. Simon Frieder, Luca Pinchetti, Alexis Chevalier, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Christi...

    arXiv

  5. [20]

    An In- Context Learning Agent for Formal Theorem-Proving.arXiv preprint arXiv:2310.04353,

    Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An In- Context Learning Agent for Formal Theorem-Proving.arXiv preprint arXiv:2310.04353,

    arXiv

  6. [21]

    Automated Theorem Proving in Intuition- istic Propositional Logic by Deep Reinforcement Learning.arXiv preprint arXiv:1811.00796,

    Mitsuru Kusumoto, Keisuke Yahata, and Masahiro Sakai. Automated Theorem Proving in Intuition- istic Propositional Logic by Deep Reinforcement Learning.arXiv preprint arXiv:1811.00796,

    arXiv

  7. [22]

    DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function

    Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, et al. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function. InProceedings of the Annual Meeting of the Association ...

    arXiv

  8. [23]

    Semantic uncertainty: Linguistic invariances for uncertainty estimation in natural language generation.arXiv preprint arXiv:2302.09664,

    Lorenz Kuhn, Yarin Gal, and Sebastian Farquhar. Semantic uncertainty: Linguistic invariances for uncertainty estimation in natural language generation.arXiv preprint arXiv:2302.09664,

    arXiv

  9. [24]

    Gtbench: Uncovering the strategic reasoning limitations of llms via game-theoretic evaluations.arXiv preprint arXiv:2402.12348,

    Jinhao Duan, Renming Zhang, James Diffenderfer, Bhavya Kailkhura, Lichao Sun, Elias Stengel- Eskin, Mohit Bansal, Tianlong Chen, and Kaidi Xu. Gtbench: Uncovering the strategic reasoning limitations of llms via game-theoretic evaluations.arXiv preprint arXiv:2402.12348,

    arXiv

  10. [25]

    Uncertainty estimation in large language models to support biodiversity conservation

    Maria Mora-Cross and Saul Calderon-Ramirez. Uncertainty estimation in large language models to support biodiversity conservation. InProceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (V...

    2024

  11. [28]

    Gabriel Y

    URLhttps://arxiv.org/abs/2002.06715. Gabriel Y . Arteaga, Thomas B. Schön, and Nicolas Pielawski. Hallucination detection in llms: Fast and memory-efficient finetuned models,

    2002 arXiv

  12. [29]

    Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou

    URLhttps://arxiv.org/abs/2409.02976. Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc Le, Ed Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models, 2023b. URLhttps://arxiv.org/abs/2203.11171. Jeremy R. Col...

    arXiv

  13. [30]

    org/abs/2305.14613

    URL https://arxiv. org/abs/2305.14613. Hsiu-Yuan Huang, Zichen Wu, Yutong Yang, Junzhao Zhang, and Yunfang Wu. Unc-ttp: A method for classifying llm uncertainty to improve in-context example selection, 2024b. URL https: //arxiv.org/abs/2408.09172. Jiaxin Zhang, Zhuohang Li, Ka...

    arXiv

  14. [31]

    Jiuhai Chen and Jonas Mueller

    URL https://arxiv.org/ abs/2303.08896. Jiuhai Chen and Jonas Mueller. Quantifying uncertainty in answers from any language model and enhancing their trustworthiness. In Lun-Wei Ku, Andre Martins, and Vivek Srikumar, editors,Pro- ceedings of the 62nd Annual Meeting of the Assoc...

    arXiv

  15. [32]

    URLhttps://aclanthology.org/2024.acl-long.283

    Association for Computational Linguistics. URLhttps://aclanthology.org/2024.acl-long.283. Zhen Lin, Shubhendu Trivedi, and Jimeng Sun. Generating with confidence: Uncertainty quantifica- tion for black-box large language models,

    2024

  16. [33]

    Kumar Shridhar, Felix Laumann, and Marcus Liwicki

    URLhttps://arxiv.org/abs/2305.19187. Kumar Shridhar, Felix Laumann, and Marcus Liwicki. A comprehensive guide to bayesian convolu- tional neural network with variational inference,

    arXiv

  17. [34]

    URL https://arxiv.org/abs/1901. 02731. Charles Blundell, Julien Cornebise, Koray Kavukcuoglu, and Daan Wierstra. Weight uncertainty in neural network. InInternational conference on machine learning, pages 1613–1622. PMLR,

    1901

  18. [36]

    Jeremiah Zhe Liu, Zi Lin, Shreyas Padhy, Dustin Tran, Tania Bedrax-Weiss, and Balaji Lakshmi- narayanan

    URLhttps://arxiv.org/abs/ 1707.05922. Jeremiah Zhe Liu, Zi Lin, Shreyas Padhy, Dustin Tran, Tania Bedrax-Weiss, and Balaji Lakshmi- narayanan. Simple and principled uncertainty estimation with deterministic deep learning via distance awareness,

    arXiv

  19. [37]

    Yijun Xiao and William Yang Wang

    URLhttps://arxiv.org/abs/2006.10108. Yijun Xiao and William Yang Wang. Quantifying uncertainties in natural language processing tasks,

    2006 arXiv

  20. [40]

    Miao Xiong, Zhiyuan Hu, Xinyang Lu, Yifei Li, Jie Fu, Junxian He, and Bryan Hooi

    URL https: //arxiv.org/abs/2305.14975. Miao Xiong, Zhiyuan Hu, Xinyang Lu, Yifei Li, Jie Fu, Junxian He, and Bryan Hooi. Can llms express their uncertainty? an empirical evaluation of confidence elicitation in llms,

    arXiv

  21. [41]

    Takeshi Kojima, Shixiang (Shane) Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwa- sawa

    URL https://arxiv.org/abs/2306.13063. Takeshi Kojima, Shixiang (Shane) Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwa- sawa. Large language models are zero-shot reasoners. In S. Koyejo, S. Mo- hamed, A. Agarwal, D. Belgrave, K. Cho, and A. Oh, editors,Advances in Neu- ral Info...

    arXiv

  22. [42]

    Tobias Groot and Matias Valdenegro-Toro

    URL https://proceedings.neurips.cc/paper_files/paper/2022/file/ 8bb0d291acd4acf06ef112099c16f326-Paper-Conference.pdf. Tobias Groot and Matias Valdenegro-Toro. Overconfidence is key: Verbalized uncertainty evaluation in large language and vision-language models,

    2022

  23. [1951]

    URLhttp://www.jstor.org/stable/2236703

    ISSN 00034851. URLhttp://www.jstor.org/stable/2236703. 15 Tomoharu Iwata and Zoubin Ghahramani. Improving output uncertainty estimation and generalization in deep learning via neural network gaussian processes,

  24. [1965]

    Dropout: a simple way to prevent neural networks from overfitting.The journal of machine learning research, 15(1):1929–1958,

    Nitish Srivastava, Geoffrey Hinton, Alex Krizhevsky, Ilya Sutskever, and Ruslan Salakhutdinov. Dropout: a simple way to prevent neural networks from overfitting.The journal of machine learning research, 15(1):1929–1958,

    1929

  25. [1996]

    Teaching models to express their uncertainty in words, 2022b

    Stephanie Lin, Jacob Hilton, and Owain Evans. Teaching models to express their uncertainty in words, 2022b. URLhttps://arxiv.org/abs/2205.14334. Katherine Tian, Eric Mitchell, Allan Zhou, Archit Sharma, Rafael Rafailov, Huaxiu Yao, Chelsea Finn, and Christopher D. Manning. Jus...

    arXiv

  26. [1998]

    Synthesizing finite-state protocols from scenarios and requirements

    Rajeev Alur, Milo Martin, Mukund Raghothaman, Christos Stergiou, Stavros Tripakis, and Abhishek Udupa. Synthesizing finite-state protocols from scenarios and requirements. InHardware and Software: Verification and Testing: 10th International Haifa Verification Conference, HVC ...

    2014

  27. [2009]

    Language models are few-shot learners.Advances in neural information processing systems, 33:1877–1901,

    Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are few-shot learners.Advances in neural information processing systems, 33:1877–1901,

    1901

  28. [2017]

    Lm- polygraph: Uncertainty estimation for language models.arXiv preprint arXiv:2311.07383,

    14 Ekaterina Fadeeva, Roman Vashurin, Akim Tsvigun, Artem Vazhentsev, Sergey Petrakov, Kirill Fedyanin, Daniil Vasilev, Elizaveta Goncharova, Alexander Panchenko, Maxim Panov, et al. Lm- polygraph: Uncertainty estimation for language models.arXiv preprint arXiv:2311.07383,

    arXiv

  29. [2018]

    Leda Cosmides and John Tooby

    URLhttps://arxiv.org/abs/1811.07253. Leda Cosmides and John Tooby. Are humans good intuitive statisticians after all? rethinking some conclusions from the literature on judgment under uncertainty.cognition, 58(1):1–73,

    arXiv

  30. [2019]

    Generative Language Modeling for Automated Theorem Proving

    Stanislas Polu and Ilya Sutskever. Generative Language Modeling for Automated Theorem Proving. arXiv preprint arXiv:2009.03393,

    2009 arXiv

  31. [2020]

    Evaluating large language models trained on code.arXiv preprint arXiv:2107.03374,

    Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde De Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evaluating large language models trained on code.arXiv preprint arXiv:2107.03374,

    arXiv

  32. [2021]

    Albert Q. Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, Lélio Renard Lavaud, Marie-Anne Lachaux, Pierre Stock, Teven Le Scao, Thibaut Lavril, Thomas ...

    arXiv

  33. [2022]

    Language models (mostly) know what they know.arXiv preprint arXiv:2207.05221,

    Saurav Kadavath, Tom Conerly, Amanda Askell, Tom Henighan, Dawn Drain, Ethan Perez, Nicholas Schiefer, Zac Hatfield-Dodds, Nova DasSarma, Eli Tran-Johnson, et al. Language models (mostly) know what they know.arXiv preprint arXiv:2207.05221,

    arXiv

  34. [2023]

    Emergent abilities of large language models

    Jason Wei, Yi Tay, Rishi Bommasani, Colin Raffel, Barret Zoph, Sebastian Borgeaud, Dani Yogatama, Maarten Bosma, Denny Zhou, Donald Metzler, et al. Emergent abilities of large language models. arXiv preprint arXiv:2206.07682, 2022a. Wenhu Chen, Xueguang Ma, Xinyi Wang, and Wil...

    arXiv

  35. [2024]

    doi: 10.18653/v1/2024

    Association for Computational Linguistics. doi: 10.18653/v1/2024. emnlp-main.1229. URLhttps://aclanthology.org/2024.emnlp-main.1229/. Debargha Ganguly, Warren Richard Morningstar, Andrew Seohwan Yu, and Vipin Chaudhary. Forte : Finding outliers with representation typicality e...

    2024 doi

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.