Proof autoformalization aims to translate a mathematical informal proof in natural language into a formal proof in a formal language such as Lean 4. Existing LLM-based models for proof autoformalization are typically evaluated only on well-formed informal proofs from curated datasets. We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from these idealized ones, and we present the first study on the robustness of proof autoformalization models. We formulate two categories of perturbations: a global perturbation paraphrases the informal theorem-proof pair in a different style, under which the formalization should remain consistent; a local perturbation alters a value, symbol, or proof step, possibly in a counterfactual way, and a robust formalization should faithfully reflect the perturbation rather than reverting to the original or inferring a different one on its own. We build a benchmark with both perturbations on miniF2F and MATH-500, and automatically measure how stable a proof autoformalization's correctness is under global perturbations and how faithfully its output reflects local perturbations. We evaluate seven recent models: their correctness varies under global perturbations, and they mostly fail to remain faithful under local perturbations.
Self-consistency answers a question by generating multiple responses and selecting the most frequent answer. Its evaluation requires both correctness labels and information about which responses agree; correctness labels alone generally determine neither voting accuracy nor the benefit of additional votes. For tasks in which all correct responses map to the same normalized answer, we derive sharp accuracy bounds using classical stochastic majorization, refined by abstention counts and answer-category limits. We also derive sharp bounds on accuracy changes across voting budgets that share a response pool. When answer-category counts are available, we introduce Plurality-U, a count-based dynamic program that exactly averages voting accuracy over all fixed-size subsets, eliminating finite-pool Monte Carlo error. On 1,403,520 stored outputs from recent reasoning models in Scorio Lite and Scorio Trace, recording abstention counts and answer options cuts the width of SuperGPQA accuracy intervals by more than half. For moving from 9 to 17 votes, our bounds reduce interval width by a median of 77.7% on SuperGPQA and 72.3% on 14 GPQA and Adaptive-Consistency pools, compared with a baseline that combines separate accuracy bounds. Exact computation has lower paired median runtime than 2,000-subset Monte Carlo in 14 of 15 tested pool-budget settings. These results clarify what incomplete logs can establish and provide an exact evaluation procedure when answer counts are retained.
Automatic judges offer inexpensive information about model outputs, but an evaluation team must decide how to turn that information into fewer human annotations. Scores can guide sampling, correct an estimate, or support adaptive acquisition, and these uses may capture overlapping gains. We compare their incremental value on fixed evaluation pools from three preference datasets, and 19 attributed-question-answering systems. Matched comparisons use the same scores, account for pilot labels and budget rules, and separate acquisition from estimation. Score stratification is a strong reference: after ten-bin stratification, the best fixed local linear correction offers only 1.00--5.27% further MSE reduction in the primary configurations. Unequal allocation offers larger gains in some pools, but can increase error when confident scores conceal variable human outcomes. Comparison on AttributedQA, shrinking learned quotas toward score-only quotas lowers pooled MSE for 17 of 19 systems relative to the score-only procedure, but ordinary pooled 95% intervals cover only 88.09--93.54%. The same shrinkage improves on the score-only reference in only one of eight preference configurations. Ranking experiments further show that lower individual MSE need not improve system selection. These findings support a simple starting procedure, proportional sampling within score strata followed by a stratified human mean, and identify what additional evidence is needed to justify correction or adaptation for the intended evaluation output.