Self-Brier and Formal Semantic Entropy

An LLM may give conflicting answers to the same question while reporting high confidence in each. We introduce two uncertainty scores that summarize its expressed certainty across repeated outputs without reference answers. Self-Brier replaces the observed outcome in the Brier score with an indicator of agreement with the most frequent sampled answer. It averages the squared differences between confidence and this indicator, combining doubt among supporters with confidence among dissenters. Formal Semantic Entropy groups formalized claims by logical equivalence and computes entropy from the group frequencies. An auxiliary model translates responses into formulas over a shared vocabulary. A theorem prover, here the SMT solver Z3, checks equivalence under shared assumptions. The groups depend on which claims the translation retains and how faithfully it represents the response. We study three models on four public reasoning benchmarks. Formal entropy covers FOLIO, ZebraLogic, and GSM-Hard. In a secondary error-detection evaluation, Self-Brier has higher mean AUROC than voting on all four benchmarks, but its gains over confidence remain uncertain. Formal entropy has higher mean AUROC than our binary LLM-equivalence baseline on all three formalized benchmarks; confidence has higher mean AUROC than formal entropy on each.