Uncertainty Quantification for Auto Formalization [NeurIPS 2025] (github.com)

Researchers presented "Grammars of Formal Uncertainty" (NeurIPS 2025) and released an open-source toolkit that quantifies syntactic uncertainty in program-like artifacts by extracting probabilistic context-free grammars (PCFGs) from source files. The system automatically downloads/generates ANTLR v4 parsers for a grammar (examples: SMT-LIB, Prolog), learns PCFG rule probabilities from a corpus, and reports entropy-based uncertainty metrics—Shannon grammar entropy, perplexity (exp cross-entropy), a Normalized Syntactic Uncertainty Index (NSUI), KL divergence from uniform, and Rényi entropy. The package exposes CLI commands, a REST API (/analyze, /grammars, /setup, /health), and is extensible to new languages by implementing a GrammarHandler. This work is significant for the AI/ML community because it gives a lightweight, grammar-aware signal to decide when to trust automated formalizers or LLMs that generate formal code/logic: high syntactic entropy or perplexity identifies ambiguous or rare syntactic constructs that often correlate with downstream failure modes in automated reasoning. Practically, the toolkit supports dataset-scale experiments (examples provided for SMT datasets such as ProofWriter), runs via pip or Docker, and produces per-file and corpus-level uncertainty statistics that can be integrated into verification, active learning, or model-selection pipelines to prioritize human review or targeted data augmentation.