PaperlayerView exact revision on arXiv

Source-linked AI summary

Diagnosing Sampled LLM Reasoning in Formal Geometry: Coverage, Realization, and Validity Evidence

Xiao Yue, Guangzhi Qu

arXiv:2609.32924v1cs.AI

TL;DR

Single-answer accuracy does not show whether sampling finds the correct answer or whether its derivation is supported. CRV separates coverage, readout realization, and critic-labeled validity evidence on frozen candidate pools; on HardShift441, pass@16 reaches 68.9% while WSC reaches 38.0%.

  • Problem

    Single-output answer matching does not reveal whether repeated sampling finds a correct answer or whether its reasoning is supported by the premises.

    Source: Introduction · p. 1

  • Method

    CRV freezes candidate pools and separately measures answer coverage, readout realization, and label-blinded critic judgments of derivational support.

    Source: Introduction · pp. 1–2

  • Results

    On HardShift441, pass@16 is 68.9% while verifier-weighted self-consistency reaches 38.0%.

    Source: Introduction · p. 1

  • Takeaways & Limitations

    Coverage, realization, and critic validity evidence are distinct quantities and should be reported separately.

    Source: Coverage, realization, and validity… · p. 2

    The audited supported rate is conditional on selected correct-answer representatives and does not estimate derivational validity across all generated traces.

    Source: Blinded derivational-support audit · p. 4

Abstract

from arXiv · show

Repeated sampling can reveal a correct numerical answer without yielding either a reliable system output or a supported derivation. We present Coverage, Realization, and Validity Evidence (CRV), an evaluation protocol for sampled large language model (LLM) reasoning over formal geometry states. Coverage is answer availability, realization is readout accuracy on the frozen candidate pool, and validity evidence is a label-blinded critic judgment of derivational support rather than a proof certificate. CRV freezes each candidate pool before comparing readouts and analyzes covered failures by correct-answer multiplicity and within-problem discrimination. On HardShift441, a 441-problem set for which a reference solver leaves 406 problems unsolved, a LoRA-adapted Qwen2.5-7B generator obtains 24.2% average single-sample accuracy and 68.9% pass@16, whereas verifier-weighted self-consistency (WSC) reaches 38.0%. Readout accuracy is particularly low when the correct answer occurs only once or twice in the pool. In a separate constructed audit of 195 covered problems, the critic labels 12 correct-answer representatives as supported, 181 as refuted, and two as uncertain. These results show that coverage, realization, and validity evidence from the critic are distinct quantities and should be reported separately.

Introduction

The Introduction presents CRV as a way to distinguish answer coverage, readout realization, and critic-based validity evidence on frozen candidate pools. It emphasizes that high answer coverage does not ensure accurate selection or critic-labeled support for derivations.

Introduction

  • The model receives an initial formal geometry state containing premises and constructions, then generates a textual derivation and numerical answer before symbolic correction or checking.The state excludes intermediate deductions from the reference proof; the study distinguishes answer-level coverage, readout selection, and blinded assessment of trace support.Source: Introduction · p. 1

Coverage, realization, and validity evidence

  • CRV is a controlled evaluation protocol, not a new selector: it freezes candidate pools, compares readouts on identical answer clusters, and reports critic-labeled derivational support separately.It localizes unrealized coverage by correct-answer multiplicity and hardest-negative discrimination, separating candidate-ranking from answer-cluster aggregation failures.Source: Introduction · pp. 1–2, Related work · p. 2

Blinded derivational-support audit

  • In the constructed audit, only 12 of 195 correct-answer representatives were labeled supported; the critic assesses traces without access to answer-correctness labels.The supported rate applies only to selected correct-answer representatives, not all generated traces; a second model agreed on 33 of 34 reviewed verdicts and human review on all 20, without estimating full-pool critic accuracy.Source: Introduction · p. 1, Blinded derivational-support audit · pp. 3–4

Experimental setup

  • HardShift441 contains 441 solver-unsolved hard-state-shift problems, with HyperGNet leaving 406 unsolved; it is disjoint from legacy-hard by identifier, but is not claimed globally unseen.The reference solver solves 35 HardShift441 problems and all 184 legacy-hard problems; the shift serves as an indicator rather than evidence of missing or unvalidated labels.Source: Introduction · p. 1, Experimental setup · p. 4

Multiplicity-conditioned failure localization

  • Correct-answer multiplicity separates generation failures from low- and high-multiplicity pools, while hardest-negative win rates measure whether a correct trace outranks the strongest incorrect trace.The random-ranking reference is adjusted to each problem’s proportion of correct candidates rather than fixed at 0.5; cluster-aggregating readouts also depend on how scores combine within answer clusters.Source: Multiplicity-conditioned failure… · p. 3

Selectors leave much of the coverage unrealized

  • WSC accuracy trails Best-of-K by 9.89 percentage points on c1 and 13.06 points on c2, but exceeds it by 7.97 points on c3+.WSC achieves 4.87% on c1, 13.53% on c2, and 75.63% on c3+; all readouts have zero c0 accuracy because no correct answer is present.Source: Selectors leave much of the coverage… · p. 5, Figure 2 · p. 5

Repeated sampling reveals answer-level coverage

Selectors leave much of the coverage unrealized

  • Across 75 problems that changed multiplicity bands across seeds, WSC accuracy was 24.67 points higher in c3+ than c1 or c2, alongside a 0.091 higher hardest-negative margin.The association is not causal because changing the random seed affects both the number and quality of generated traces; the descriptive multiplicity pattern also appeared across all 27 cross-backbone development cells.Source: Repeated sampling reveals answer-level… · p. 5, Selectors leave much of the coverage… · p. 6
  • 14.57%, 26.59%, and 66.82% hardest-negative win rates for c1, c2, and c3+ exceed random-ranking baselines, yet low-multiplicity correct traces usually lose.Candidate-level AUC is approximately 0.819 on HardShift441 versus 0.903 in-domain, a descriptive comparison confounded by differing datasets and candidate-generating systems; pass@K grows faster than realized accuracy as sampling rises from 8 to 16.Source: Selectors leave much of the coverage… · p. 6

A blinded critic labels most audited correct-answer representatives as refuted

  • 12 of 195 correct-answer representatives were labeled supported, 181 refuted, and two uncertain by the blinded critic.The audit is conditional on constructed representatives, not an estimate of valid-trace prevalence; reviewed strata checks do not establish critic calibration or full-pool accuracy.Source: A blinded critic labels most audited… · p. 6

Exploratory intervention screening

  • Stronger generation, verifier training, larger verifiers, and ensembles show local gains, but no tested intervention closes the gap consistently across settings.The trained pointwise verifier improves legacy-hard accuracy over Majority by 10.51 percentage points; results come from independent candidate pools and splits and are exploratory.Source: Exploratory intervention screening · pp. 6–7, Table 4 · p. 7

Discussion

  • On HardShift441, low-multiplicity pools rarely yield the correct answer in evaluated readouts, motivating stronger discrimination and aggregation that preserves rare-answer clusters.This pattern does not establish a causal multiplicity effect; the analysis concerns numerical-answer generation over formal states, selected audit traces, and a reference solver that leaves 406 of 441 problems unsolved.Source: Discussion · p. 7

Conclusion

  • 68.9% pass@16 versus 38.0% WSC on HardShift441 shows that answer availability exceeds realized readout accuracy, especially for covered c1 and c2 problems.The conclusion cautions that pass@K is neither deployable readout accuracy nor evidence of derivational validity.Source: Conclusion · p. 7

1 Scope of this report

The report sets out the CRV analysis and its supporting experiments, while keeping exploratory studies and adjacent tasks separate. It also identifies the appendix’s evidence-tier and claim-evidence tables.

1 Scope of this report

  • Sections 2–12 document CRV and its supporting experiments, including data, methods, results, and ablations.Source: §1 · p. 9
  • Exploratory development studies and adjacent tasks, including theorem selection and executable FormalGeo policies, are presented separately because they use different inputs and outcomes.Source: §1 · p. 9
  • HardShift441 names the solver-unsolved hard-state shift; WSC names verifier-weighted answer-cluster readout, and pass@K measures the fraction with a correct answer among the first K candidates.Source: §1 · p. 9

1.1 Evidence tiers; 1.2 Claim and evidence map

2 Formal task, data, and split provenance

The project distinguishes theorem selection from direct solving, applying CRV only to direct solving with natural-language problems and formal-state information. HardShift441 defines the hard-state shift, while split and historical-artifact boundaries qualify claims of separation.

2.1 Two tasks in the project

  • Theorem selection chooses a recorded next action from a proof frontier and applicable theorem instances, whereas direct solving generates a derivation and numerical answer from a natural-language problem and, in the main setting, an initial-state rendering.Source: §2.1 · p. 10
  • The direct-solve target is a scalar quantity, and difficulty labels proxy annotated trajectory length: one step, two or three steps, or at least four.Source: §2.1 · p. 11

2.2 Formal state supplied to the model

  • The renderer supplies step-zero fact nodes but withholds proof hyperedges and later theorem applications, exposing formal premises without supplying a solution trajectory.Source: §2.2 · p. 11
  • The default state renders eligible step-zero facts as English bullets; a variant retains a one-hop target-neighborhood, while other variants select or deduplicate fact types.Source: §2.2 · p. 11

2.3 Dataset composition

  • HardShift441 has no PID overlap with legacy hard and averages 4.51 more state nodes and 0.51 more annotated proof steps, with a target-kind total-variation distance of 0.1997.Source: §2.3 · p. 11
  • HardShift441 was frozen before primary candidate generation; the later 300/60/81 PID split supports within-experiment separation, not a globally untouched benchmark.Source: §2.3 · p. 11

2.4 Gold provenance and leakage discipline

  • The reference HyperGNet run solves 35 of 441 FormalGeo7K problems and leaves 406 unsolved; experiment manifests enforce PID separation relative to designated training data, not a global never-seen status.Source: §2.4 · pp. 11–12
  • The theorem-selection studies use two checked-in state-action corpora of 23,757 and 23,389 records and metadata for 196 theorems, whereas direct-solve splits are problem-level.Source: §2.4 · p. 12

3 Exact CRV protocol

CRV evaluates answer availability, readout selection on a shared frozen candidate pool, and critic judgments of derivational support. It further examines covered problems by correct-answer multiplicity and uses a label-blinded process audit.

3.1 Candidate generation, parsing, and answer clusters

  • Candidate traces are parsed into scalar answers or unparsed values, and numeric gold matching uses absolute and relative tolerances of 10^-6.Source: §3.1 · p. 12
  • All readouts are evaluated on the same frozen candidate pool, so their differences reflect selection rather than generation.Source: §3.1 · p. 12

3.2 Coverage and realized readouts

  • Majority selects the largest answer cluster, while Best-of-K selects the candidate with the highest pointwise verifier score.Source: §3.2 · p. 12

3.3 Multiplicity and hardest-negative comparisons

  • The exchangeable reference for a correct candidate ranking first varies with multiplicity: 6.25% for c1, 12.50% for c2, and 45.71% on average for observed c3+ pools.Source: §3.3 · p. 13

3.4 True-prefix budget curves

  • Budget curves evaluate observed prefixes at K = 1, 2, 4, 8, and 16, preserving candidate order; at K = 1, majority, WSC, and coverage coincide.Source: §3.4 · p. 13

3.5 Blinded process audit

  • The process audit compares selected correct- and wrong-answer representatives one trace at a time, hiding gold labels, competing traces, verifier scores, and side names from the auditor.Source: §3.5 · p. 13
  • The audit’s supported rate describes selected representatives in that audit sample, not all generated traces or correct-answer clusters.Source: §3.5 · p. 13
  • Figure 1 depicts the diagnostic flow, with candidate generation frozen before coverage, readout, multiplicity, and derivational-support analyses are compared.Source: Figure 1 · p. 14

4 Models, prompts, and training details

The methods pair a direct-solve prompt and sampled candidate pools with pointwise outcome verification and a separate process critic. The appendix also specifies generator selection, calibration, and training configurations.

4.1 Generator prompt

  • The direct-solve prompt combines the problem text with an optional state block and requests step-by-step reasoning with a boxed numerical answer.Source: §4.1 · p. 14
  • Main pools use 16 samples at temperature 0.8 and top-p 0.95, with a 3,072-token output limit; prefix experiments reuse those candidates.Source: §4.1 · p. 14

4.2 Outcome-verifier prompt and target

  • The outcome verifier judges whether a candidate’s final answer is correct, with its Yes label tied to parsed-number agreement with dataset gold rather than derivation validity.Source: §4.2 · p. 14

4.3 Main generator and verifier training

  • Model scale names include 7B, 8B, 14B, and 32B, while training descriptions use SFT and LoRA.Source: §4.3 · p. 15
  • Table 4 identifies the main training configurations as its scope.Source: Table 4 · p. 15
  • The diversity-trained generator selects hard-problem traces across source-arm and token-length-quartile buckets before filling remaining slots by score.Source: §4.3 · p. 15
  • The three main 7B verifier seeds use frozen calibration pairs (1.5, 2), (1.5, 2), and (1.75, 1), retained unless recalibration is studied.Source: §4.3 · p. 15

4.4 Process-critic instruction

  • The process critic grades step support, localizes the first unsupported step, and may return uncertain when the state is insufficient.Source: §4.4 · p. 15

5 Statistical protocol

The protocol treats problem identifiers as the primary uncertainty unit and distinguishes matched interface and state-content effects. Boxed derivations produce the largest matched gain, while state effects vary by model and target.

5 Statistical protocol

  • Problem identifiers are the primary uncertainty unit; the main CRV interval resamples PIDs while holding observed generator and verifier seeds fixed.Paired differences are formed within each of 10,000 PID-bootstrap replicates; a hierarchical sensitivity analysis also weights generator and verifier seeds.Source: §5 · p. 16

6.1 Chain of thought, image input, and textual state

  • 28.57 points: boxed derivations outperform answer-only JSON on matched one-step problems, with paired McNemar p ≈3 × 10−47.Image input adds 5.32 points in the answer-only condition, but its 3.17-point CoT gain is not significant; natural-state text reaches 59.66%, statistically indistinguishable from the VLM result of 58.82%.Source: §6.1 · p. 16, Table 5 · p. 16

6.2 State-content ablations

  • Full-state effects vary by model and split: equations alone nearly match the general 7B, but trail Qwen3-32B by 5.32 points.Natural or goal-relevant state is the strongest general default, while target type does not support a reliable router.Source: §6.2 · pp. 16–17, Table 6 · p. 17
  • 63.49%: the per-kind oracle router on easy problems exceeds learned routing, which reaches at most 61.54% and stays below the best single Math-7B state arm at 61.62%.Target-type features capture some heterogeneity but do not identify the best input reliably enough to improve deployment.Source: §6.2 · p. 17

7 Expanded coverage and realization results

Increasing the candidate budget expands answer coverage more than it improves readout accuracy, especially when correct answers occur at low multiplicity. Verifier weighting helps once correct evidence is redundant, but several readout and deployment interventions remain limited.

7.1 OOD budget curve

  • K = 16: the coverage–WSC gap is 27.66–34.29 pp, and conversion efficiency falls from 0.543 at K = 2 to 0.125.From K = 8 to K = 16, 114 PID-seed observations gain coverage, but WSC records 42 fixes and 39 breaks under the stated diagnostic binarization.Source: §7.1 · pp. 17–18, Table 7 · p. 17

7.2 Legacy curve and stronger-generator replication

  • +7.07 points: on legacy hard, Qwen3-8B at K = 8 improves readout over the older K = 16 system, while its K = 8-to-16 coverage gain yields only 1.93 points of WSC.On legacy easy/medium at K = 16, coverage is 88.60%, majority 67.36%, and WSC 69.78%.Source: §7.2 · p. 18, Table 8 · p. 18

7.3 Within-problem multiplicity contrast

  • +24.67 pp: among eligible HardShift441 PIDs, high-multiplicity WSC is 39.11% versus 14.44% at low multiplicity.The paired contrast is observational because changing generator seed changes both multiplicity and trace content; the hardest-negative margin rises by 0.091.Source: §7.3 · p. 18, Figure 3 · p. 20

7.4 Multiplicity-by-readout decomposition

  • For c1 and c2, WSC trails Best-of-K by 9.89 and 13.06 pp; for c3+, WSC leads by 7.97 pp.Frequency aggregation penalizes rare correct clusters, while it becomes useful after the generator supplies redundant correct evidence.Source: Table 9 · p. 18, §7.4 · p. 19, Figure 2 · p. 19

8.1 Training-free readouts

  • None of six training-free alternatives passed the preregistered +3 pp significant-improvement threshold over majority.Mean-token-logprob ranking decreases accuracy by 8.29 points on easy/medium base candidates and 11.66 points on anchor candidates at K = 16; equation substitution is uninformative for 569/570 problems.Source: §8.1 · pp. 19–20, Figure 3 · p. 20

8.2 Trained 7B outcome verifiers

  • 53.44%: the mixed 7B verifier’s mean hard-anchor WSC across three seeds, versus a 42.93% majority baseline, with all paired lifts significant.The two trained 32B seeds average 57.61%, 4.17 points above the trained 7B mean, but the deployment criterion was not completed and individual comparisons were not significant.Source: §8.2 · p. 20, Table 10 · p. 20, §8.3 · p. 21

8.4 Low-budget and adaptive readouts

  • At comparable cost, margin-based dynamic stopping underperforms fixed K; one hard configuration reaches 46.86% at average K = 5.04 versus 54.27% at fixed K = 8.Two-sample readout is a degraded mode, not an accuracy-preserving substitute for K = 16; oracle anytime selection also cannot satisfy the locked criterion.Source: §8.4 · p. 21

8.5 Compute frontier

  • On hard problems, 32B greedy reaches 50.54%, above every tested 7B majority readout; the 7B approach remains useful when memory is constrained.The cost proxy is parameter-count times generation count and omits memory and hardware effects; the 7B multi-sample setup exceeds one 32B decode under that proxy.Source: §8.5 · p. 21, Figure 4 · p. 22

9 OOD verifier interventions

Generator and verifier interventions can increase candidate coverage without commensurate realized accuracy, and OOD verifier repairs do not improve both OOD and legacy settings. Results also show trade-offs from distillation, stronger generators, and mixing candidate sources.

9.1 Cross-scale generator transfer

  • On HardShift441, 14B pass@16 is 71.73% versus 68.93% for 7B, but WSC is 38.57% versus 38.00%, with paired CI [−1.36, 2.54].The 2.80-point coverage gain corresponds to only a 0.58-point readout gain; conversion efficiency falls from 0.231 in the legacy comparison to 0.075 OOD.Source: §9.1 · p. 22

9.2 OOD-matched pointwise and ranking training

  • 44.44%: two-epoch groupwise ranking WSC on OOD development, but legacy hard regresses 9.24 points and easy/medium 5.18 points.A 75/25 legacy-data mix preserves the OOD result but leaves legacy hard 3.81 points below baseline.Source: §9.2 · pp. 22–23

9.3 Multi-backbone replication

  • Across three seeds, the same-model verifier advantage is only +1.10 pp, CI [−0.82, 3.02], and the initially best cross-family pairing averages +0.41 pp.All nine backbone/seed combinations regress on legacy hard; every verifier family is weak on c1 and stronger on c3+.Source: §9.3 · p. 23, Figure 5 · p. 23, Table 12

10.1 Blanket SFT, short traces, and targeted distillation

  • Targeted distillation is the first net-positive SFT recipe: three-seed accuracy averages 53.02±0.40%, although paired tests are nonsignificant and the bootstrap interval crosses zero.Formal-trace SFT shortens median output from 1,239 to 361 characters but harms targets requiring calculation; shorter teacher traces do not resolve the accuracy bottleneck.Source: §10.1 · p. 24, Table 13 · p. 24

10.2 RFT (rejection-sampling fine-tuning)

  • With the mixed outcome verifier, diversity-trained generation raises legacy hard WSC from 53.44 to 56.52% and easy/medium from 69.78 to 71.04%.The gains are the most consistent among tested 7B generator changes, although the reported RFT results vary across seeds and evaluation can vary with batch composition.Source: §10.2 · p. 24

10.3 Larger and stronger generators

  • Across three generation seeds, Qwen3 at K = 8 improves hard and easy/medium readout by 7.07 and 2.94 points over the older 7B K = 16 system.Halving Qwen3 samples reduces end-to-end latency 19.7%, below the locked efficiency threshold; stronger generation improves accuracy without reducing cost in this comparison.Source: §10.3 · pp. 24–25

10.4 Generator diversity and evidence concentration

  • At fixed K = 16, mixing 12 Qwen3 and four Qwen2.5 samples raises coverage by 0.76 points but lowers the best realized readout by 1.38 points.Under a fixed four-sample budget, the best heterogeneous mixture gains only 0.72 points of pass@4 and 0.44 points of WSC, below preregistered gates.Source: §10.4 · p. 25

11 Selection, aggregation, and repair interventions

Selection, aggregation, and repair experiments produce limited or setting-specific gains, while the process audit finds few supported derivations among correct-answer representatives. Adjacent theorem-selection studies likewise find representation heterogeneity that learned routers do not reliably exploit.

11.1 Outcome-only GRPO (Group Relative Policy Optimization)

  • Outcome-only GRPO leaves greedy accuracy within engine noise and does not change majority or coverage.The result is specific to LoRA GRPO with binary answer correctness, which gives the same reward to valid derivations, lucky guesses, copied values, or error cancellation.Source: §11.1 · p. 25

11.2 Answer-cluster preference learning

  • At K = 4, answer-cluster WSC rises only from 82.48 to 84.14%, short of the two-point gate; DPO adds 0.31 points beyond continued SFT while length grows.The repaired content selector still loses on disagreements, with 149 fixes versus 214 breaks; verifier ensembles and learned aggregation do not beat the best single verifier by the two-point gate.Source: §11.2 · pp. 25–26, §11.3 · p. 26, §11.4 · p. 26

11.5 Error-conditioned local repair

  • At development K = 4, local repair decreases accuracy from 82.61 to 71.20%, with five fixes and 26 breaks.The model learns to re-solve rather than conservatively edit, failing the identity-preservation constraint.Source: §11.5 · p. 26

12.1 Pair construction and verdict distribution

  • Only 12/195 correct-answer representatives (6.15%) are labeled supported; 181 are refuted and two uncertain, while tie-adjusted pairwise win rate is 53.6%.The most frequent first errors include invented geometric relations and theorem uses with unestablished preconditions; audits support selected-strata reliability but do not estimate valid-trace prevalence.Source: §12.1 · pp. 26–27, Table 14 · p. 26, §12.2 · p. 27

12.2 First-error taxonomy

  • The text-only process critic cannot resolve roughly 12% of refutations involving state-underdetermined orientation, arc order, or diagram conventions.The passage identifies richer state encoding or formal certificate checking as needed to resolve those cases.Source: §12.2 · p. 27

12.4 Answer-only generative critics

  • The stronger answer-only critic reaches 78.4% pairwise win rate but only 78.4% high-confidence-refutation precision, and c1 win rate remains 35.3%.The process-aware audit contains too few valid traces for answer selection, while answer-only critics re-solve unreliably.Source: §12.4 · p. 27

13.1 Zero-shot state ablation

  • For Qwen2.5-7B, full state changes family accuracy by +22.1 points for line and −34.0 for perpendicular, while this family structure largely disappears for Math-7B.The family effects remain directionally stable across candidate-count and proof-step strata.Source: §13.1 · p. 28, Table 15 · p. 28

13.2 State routing, candidate deltas, and symbolic lookahead

  • Gold-family oracle routing reaches 42.2–43.1%, but learned routers do not realize its 3–4-point headroom; candidate deltas repair some families harmed by full state.Symbolic lookahead reaches 39.58%, only 0.57 points above no-state zero shot; a limited hybrid reaches 40.7% without establishing a general ranker.Source: §13.2 · pp. 28–29, Figure 6 · p. 28

14 Adjacent project study II: theorem attribution

The adjacent studies examine theorem attribution and executable FormalGeo policies, which use targets and settings distinct from sampled textual reasoning. Their results expose attribution limits and show how candidate-generation costs and certification constrain executable-policy outcomes.

14 Adjacent project study II: theorem attribution

  • The experiments distinguish theorem attribution from derivational support and executable policies from sampled textual reasoning.The attribution labels concern theorem naming, while executable-policy results use FormalGeo actions checked by a symbolic engine.Source: §14 · p. 29, §15 · p. 30

14.1 Formal theorem identifiers

  • With an oracle shortlist, theorem-base F1 rises to 0.606/0.560, but exact base-set match on correct answers is 58.0% for easy and 10.1% for medium.Formal-trace SFT raises open-inventory F1 to 0.455/0.566, while answer accuracy falls to roughly 35 to 39%.Source: §14.1 · p. 29

14.2 Natural-language rule attribution

  • In a 1,500-problem expansion, model-judge explanation-correct rates are 67.4%, 56.2%, and 19.4% on easy, medium, and hard, respectively.Only the 200-example pilot received a 10-case human spot check; the expansion lacked completed human calibration.Source: §14.2 · p. 29

15.1 Theorem policy and candidate-generation cost

  • On 50 validation problems, HyperGNet solves 42%, while a local theorem-selector LoRA reaches 40%; beam four lowers results under the fixed time budget.An oracle graph solves all 50 at K = 16, but 28 of 29 rescued cases share a greedy-equivalent sequence, implicating candidate execution cost rather than theorem ranking.Source: §15.1 · p. 30

15.2 Budget-aware candidate generation

  • A two-action candidate limit raises the 60-second solve rate from 43.0 to 85.5% on a fresh 200-problem validation set; the paired gain is +42.5 pp.Hard timeouts fall from 113 to 24, and median runtime falls from 60 seconds to 0.74 seconds.Source: §15.2 · p. 30
  • In a 2×2 study, K = 2 yields 89.5% without goal-aware termination and 90.5% with it, indicating most of the gain comes from small-K generation.The small-K main effect is +34.75 pp; the termination main effect is +8.75 pp, with a −15.5 pp interaction.Source: §15.2 · p. 30

15.3 Thinking and formal cascades with certification

  • The formal-then-thinking cascade reaches 98.9/99.0% on legacy hard/easy-medium, but four false successes and inadequate efficiency prevent it passing critical gates.Certificate-first reruns eliminate the four known false successes but certified coverage remains 7.61% on hard and 12.18% on easy/medium, below the 20% threshold.Source: §15.3 · pp. 30–31

16 Experiment inventory

Table 16 inventories experiments across different pools, splits, and objectives, so their outcomes should be interpreted within each experiment. Across the inventory, several approaches show headroom or gains, while others fail to improve selection, efficiency, or generalization.

Direct solving and generator training

  • Textual step-zero state adds 3 to 8 points, while image and Math specialization yield smaller gains; pointwise no-state reaches 41.33%.Learned state routing does not beat the best single arm, despite oracle headroom.Source: §16 · p. 31
  • Formal traces are harmful, raw teacher traces tie, and targeted-plus-anchor distillation is directionally positive but small and nonsignificant.The diversity-trained generator gives the stable deployment improvement after initial large gains proved seed-sensitive.Source: §16 · p. 31

Selection, verification, and efficiency

  • Coverage near 90% on legacy easy/medium reveals a realization problem, while outcome-GRPO recipes fail to improve beyond engine noise.Training-free logprob best-of-K and binary filtering are harmful; verifier help is strongest in-domain, with mixed hard data giving a stable +10.51 pp hard lift.Source: §16 · p. 31
  • A trained 32B verifier gives a smaller two-seed gain over trained 7B, while hard-negative training makes the verifier over-conservative.Matched candidates and hard-negative refinements both fail to improve the mixed verifier.Source: §16 · p. 32
  • Remote routing matches always-remote accuracy at a 56.55% call rate, above the 40% budget gate; local repair breaks more correct answers than it fixes.Adaptive budgeting does not preserve hard accuracy, for which fixed K = 16 remains the accurate operating point.Source: §16 · p. 32
  • Trace-aware set selection narrows its deficit to 0.71 points but does not surpass WSC; heterogeneous generator mixtures gain less than one point at four samples.Internal preference metrics improve under cluster-preference training, but external K = 4 accuracy gain is too small and outputs grow longer.Source: §16 · p. 32

OOD generalization and process validity

  • Process-critic checks find supported correct-answer traces too rare for selection, while coverage headroom and low multiplicity generalize across backbones.Three Qwen3 generation seeds are positive on both legacy splits, and K = 16 remains best; adjacent attribution audits lack human calibration at scale.Source: §16 · pp. 32–33

17 Code supplement and reproducibility scope

The supplement includes a curated source snapshot spanning final-manuscript experiments and supplementary studies. It supports code inspection and fresh reruns, but exact retrospective replay requires raw generations that are not included.

17.1 Included code

  • The 186 Python files and 54 shell launchers cover direct solving, CRV analyses, generator and verifier training, process audits, and adjacent formal-policy studies.Large data and model artifacts are excluded; the package is a project-level source snapshot.Source: §17.1 · p. 33, §17.2 · p. 34
  • The package removes two unrelated dependencies without changing experiment prompts, candidate construction, scoring, or statistical analysis.Some scripts retain environment-specific model paths or service configuration that must be adjusted.Source: §17.1 · p. 34

17.2 Included source scope and excluded large artifacts

  • The submission excludes raw completions, full candidate pools, verifier scores, training logs, API responses, and checkpoints, limiting exact retrospective replay.Fresh reproduction requires the input corpus, model access, and compute; results can vary with inference engine, model revision, or hosted API.Source: §17.2 · p. 34, §17.3 · p. 34

17.4 Recommended reproduction sequence

  • The recommended CRV rerun constructs the split, generates ordered candidate prefixes, scores candidates, computes readouts and intervals, then regenerates tables.The interval step uses 10,000 bootstrap replicates and random seed 20260724.Source: §17.4 · p. 35

18 Limitations and reporting boundaries

The paper states boundaries on target auditing, split isolation, audit interpretation, and model and cost coverage. These qualifications constrain what the reported measurements establish.

18 Limitations and reporting boundaries

  • The numerical targets come from FormalGeo7K without an independent audit of all targets, and no split is globally untouched across the available PID universe.The reference HyperGNet run leaves 406 of 441 OOD problems unsolved.Source: §18 · p. 35
  • The process audit covers 195 correct-answer representatives selected by cluster multiplicity and verifier score, not every covered problem.One primary model critic supplies verdicts; human review did not validate the exact location of each first error.Source: §18 · p. 35
  • Controlled matrices cover a small set of Qwen and Llama backbones with one formal-state rendering.Intervention and multi-backbone results use development or legacy splits examined during development.Source: §18 · p. 35
  • Within-PID contrasts locate system failure but do not estimate the causal effect of duplicating one correct trace.Generator seeds change both multiplicity and trace quality.Source: §18 · p. 35
  • Parameter count times generation count is only a coarse cost proxy, and measured latency depends on configuration.Executable search, theorem attribution, and theorem selection use different targets from sampled direct-solve CRV and should be interpreted separately.Source: §18 · p. 35

19 Summary of findings

Across evaluated settings, no tested alternative consistently closes the gap, while in-domain outcome-verifier training and stronger generation show the most repeatable gains. The findings distinguish answer coverage, readout accuracy, and derivational support, with readout performance tied to correct-answer multiplicity.

19 Summary of findings

  • As K grows, coverage rises while realized accuracy plateaus; higher correct-answer multiplicity coincides with higher readout accuracy and a larger hardest-negative margin.At low multiplicity, the verifier often ranks a wrong trace first, while frequency aggregation further downweights the rare correct cluster.Source: §19 · p. 35
  • In-domain outcome-verifier training and stronger generation give the most repeatable gains, but remain limited by OOD discrimination and low multiplicity.None of the tested alternatives closes the gap consistently.Source: §19 · p. 36
  • Answer-level coverage measures whether a pool contains a correct numerical answer, but only a small fraction of selected correct-answer representatives had defensible derivations in the blinded audit.Candidate generation, answer selection, and derivation checking capture distinct parts of the task.Source: §19 · p. 36

Related papers

Loading 2609.32924v1…