One-Sided Verification Under Limited Expert Review

1 Introduction

• Candidate generation can outpace essential expert review, while LLM-as-a-Judge frameworks cannot reliably establish scientific validity.Automated feedback may be unavailable or too expensive, making it difficult to assess candidates and guide subsequent attempts.Source: §1 · p. 2
• The paper targets maximizing TNR subject to a low FNR constraint, preserving valid solutions while filtering invalid candidates to reduce review effort.At a fixed FNR constraint, higher TNR lowers the number of candidates requiring human review per valid solution found.Source: §1 · p. 2
• OSVERIFY separates error proposal from validation: a hierarchical proposer searches solution parts at multiple granularities, and a validator judges whether proposed errors are substantial.The validator is post-trained on substantial and non-substantial proposed errors to distinguish error types and generalize across problem difficulties.Source: §1 · p. 2
• 46% fewer invalid candidates required human review on average than with baselines under a low-FNR setting, and gains carried over to unseen FirstProof-Eval.Validator training further improved the reduction.Source: §1 · pp. 2–3
• OSVERIFY identified 45 and 88 expert-verified issues in two mathematics papers, and helped resolve three open conjectures whose proofs experts confirmed.The original paper authors confirmed the reported errors and proposed corrections.Source: §1 · p. 3

2 Verification under Limited Human Effort

• Accuracy can be high when valid solutions are rare, AUROC does not directly characterize the low-FNR regime, and neither metric quantifies expert review effort.PASS candidates are retained for human review, while REJECT candidates are filtered out.Source: §2 · p. 3
• One-sided verification maximizes TNR subject to an FNR ceiling, treating valid solutions as positive and retaining PASS candidates for human review.The constraint preserves at least a 1 − τ fraction of valid solutions for review.Source: §2 · p. 3
• Under the FNR constraint, higher TNR lowers the average number of PASS candidates requiring review per retained valid solution.The review-cost definition uses p, the proportion of valid solutions.Source: §2 · p. 4
• Voting and thresholding select a TNR–FNR trade-off rather than improving TNR under the constraint, and added judgments eventually saturate.Figure 2 reports higher TNR for error-level than solution-level judgments at matched FNR, particularly in the low-FNR regime.Source: §2 · p. 4, Figure 2 · p. 4

3 OSVERIFY: Decoupling Error Proposal and Validation

• AUROC improved from 0.68 to 0.90 on FirstProof-Eval; error-level TNR was higher than solution-level TNR at matched FNR, particularly in the low-FNR regime.Both distributions used gpt-oss-120b.Source: §3 · p. 5

3.1 Error Proposer

• Hierarchical decomposition searches for substantial errors at multiple solution granularities, from the overall argument to individual parts.The proposer recursively splits the solution and seeks errors in each resulting part.Source: §3.1 · p. 5

3.2 Error Validator

• The validator checks whether each proposed error is real and invalidates the solution, distinguishing substantial errors from hallucinated or minor issues.This distinction accommodates task-dependent standards: minor errors may be serious in production but acceptable in proof sketches.Source: §3.2 · p. 6
• Reinforcement-learning post-training teaches the validator to classify proposed errors as substantial or not using error-level supervision.For invalid solutions, reference-assisted judgments label an error positive only when at least three of five samples judge it substantial; remaining errors are discarded.Source: §3.2 · p. 6

4.2 OSVERIFY Reduces Review Effort under the Same FNR Constraint

• At 5% FNR, OSVERIFY raises oss TNR over VOTING from 38.4% to 70.4% on Putnam100, 69.2% to 84.7% on H2V, and 35.9% to 58.0% on FirstProof-Eval.The comparison is reported in Table 1 under empirical FNR constraints.Source: Table 1 · p. 7, §4.2 · p. 8

4.1 Experimental Setup

• Evaluations use three mathematical benchmarks, with reference solutions and formal proof checkers withheld from intentionally weaker verifier backbones.The benchmarks are Putnam100, H2V, and FirstProof-Eval; the setup is intended to study verification without reliable automated evaluation.Source: §4.1 · p. 7

4.2 OSVERIFY Reduces Review Effort under the Same FNR Constraint

• Validator training further raises TNR on Putnam100 and FirstProof-Eval, including from 50.4% to 57.8% on FirstProof-Eval at zero FNR.On H2V, the training-free validator already reaches the proposer’s coverage limit, leaving little room for training gains.Source: §4.2 · p. 8

4.3 Scaling Analysis and Meta-Algorithm Applications

• At 5% FNR, trained OSVERIFY reaches the same 58% TNR with almost four times less compute than its untrained counterpart.The token budget includes decomposition, error proposing, and error validation.Source: Figure 4 · p. 9, §4.3 · p. 9
• Deeper decomposition raises TNR before saturating, with most gains reached by depth two; longer FirstProof-Eval solutions leave more room for decomposition.Many Putnam100 solutions stop decomposing before the depth limit.Source: Figure 3 · p. 8, §4.3 · p. 9
• On FirstProof-Eval at zero empirical FNR, increasing validation votes from 10 to 30 raises TNR from 38.7% to 56.5% with oss and from 13.6% to 52.3% with 5mini.Tighter FNR constraints benefit more from additional votes; performance under the 10% constraint generally saturates with fewer resamples.Source: Figure 3 · p. 8, §4.3 · p. 9
• OSVERIFY can pair existing error-search procedures with shared validation and thresholding, improving TNR over VOTING for MULTIAGENT DEBATE and PFBV on H2V.At zero FNR, TNR rises from 71.2% to 80.8% for MULTIAGENT DEBATE and from 0% to 92.6% for PFBV.Source: §4.3 · p. 9

4.4 Mathematical Research Case Study

• OSVERIFY found expert-confirmed errors in 11 mathematical papers and helped verify three formerly open relative Langlands statements.It also reported an overlooked mistake in a paper proving the Manin constant conjecture and reproduced the result with a problem-solving system.Source: §4.4 · p. 10

• Formal proof checking offers machine-checked guarantees, but formalizing research proofs remains costly; natural-language methods instead verify criteria, steps, or proof blocks.Judging units in isolation can cause spurious failures when context is lost.Source: §5 · p. 11
• OSVERIFY keeps the full problem and solution in context while proposing errors at each decomposition level, rejecting only after independent validation confirms an error.This contrasts with approaches that supervise judgments of whole solutions, steps, or critiques.Source: §5 · p. 11
• Earlier LLM checkers find expert-confirmed errors in published papers but have low precision, motivating an explicit constraint on false rejections.The paper’s objective follows the Neyman–Pearson paradigm of constraining one class-conditional error rate while optimizing the other.Source: §5 · p. 11

6 Conclusion

• OSVERIFY separates error proposal from validation to improve TNR under low FNR constraints while preserving valid candidates for expert review.Experiments on three mathematical benchmarks and human-confirmed research applications support its potential to support discovery with limited human effort.Source: §6 · p. 11

A Additional Related Work

• AI discovery systems use automated evaluators to scale search, while critique-assisted methods help humans find flaws and leave them as final arbiters.The paper focuses on filtering candidates for limited expert review without discarding rare valid solutions.Source: A Additional Related Work · p. 20
• LLM judges evaluate generated outputs, while self-correction, critique-based revision, multiagent debate, and judgment aggregation offer other evaluation strategies.The discussion notes that self-correction without external feedback can fail to improve reasoning.Source: A Additional Related Work · p. 20
• Prior verifier training covers whole solutions, reasoning steps, or critiques; this paper trains validators on individual proposed errors.The related-work discussion includes outcome and process verifiers, generative verifiers, natural-language feedback, and reinforcement learning for judges and critics.Source: A Additional Related Work · p. 20

• Pessimistic voting rejects when any of 16 sampled judgments rejects, whereas optimistic voting rejects only when all 16 reject.Source: §B.1 · p. 20, Table 2 · p. 21
• Within each draw, an infeasible voting rule is replaced by always-pass before TNR is averaged.Source: §B.1 · p. 20, Table 2 · p. 21
• The comparisons draw 16 judgments without replacement from each recorded 64-judgment pool and average results over 2,000 resampling trials.Source: Table 2 · p. 21

B.2 Cost analysis

• Inference cost is mean input and output tokens per solution, including reasoning, summed across each method’s stages and used as a proxy for compute.The comparison jointly varies VOTING judgments and OSVERIFY proposal budget, decomposition depth, and validation votes; component-wise estimates include reconstructed validator inputs and estimated outputs.Source: §B.2 · pp. 21–22, Table 3 · p. 22
• At approximately 128k tokens per solution and a 5% FNR constraint on Putnam100, TNR is 41.4% for VOTING, 86.2% for OSVERIFY, and 94.8% for the trained-validator configuration.Figure 5 compares the best empirical TNR attainable within each input-plus-output token budget.Source: §B.2 · p. 21, Figure 5 · p. 22

B.3 Saturation of the VOTING baseline

• With oss under a 5% FNR cap, increasing VOTING from 16 to 64 judgments changes TNR from 41.4% to 39.7% on Putnam100 and leaves it at 35.6% on FirstProof-Eval.The authors report diminishing returns, with most curves approaching a plateau within the first few dozen judgments; 64 judgments do not recover OSVERIFY’s main-table gains in these configurations.Source: §B.3 · pp. 22–23, Figure 6 · p. 23

B.4 Held-out threshold selection on Putnam

• For deployment-style Putnam evaluation, thresholds are selected on 100 held-out valid solutions with no shared problems with Putnam100, using the FactTest order-statistic procedure at δ = 0.10.The resulting calibration indices are k = 99 for τ = 0.05 and k = 95 for τ = 0.10; rejection is only for scores strictly above the kth smallest calibration score.Source: §B.4 · p. 23, Table 4 · p. 23

B.5 Training data audit ablation

• The full setup uses reference-assisted screening of proposed errors from invalid solutions, while the ablated setup omits that audit.The comparison is between the resulting oss validators.Source: §B.5 · p. 23, Figure 7 · p. 24
• With auditing, TNR is 89.6±1.7% on Putnam100, 83.2±0.7% on H2V, and 62.3±0.8% on FirstProof-Eval; without auditing, it is 84.8±2.6%, 82.6±0.7%, and 60.0±1.5%, respectively.Auditing improves mean TNR by 4.8, 0.6, and 2.3 percentage points, respectively, under a 5% empirical FNR constraint.Source: §B.5 · p. 24, Figure 7 · p. 24
• The reported results support checking individual proposed errors rather than relying solely on the invalidity of their source solutions.Source: §B.5 · p. 24

C.1 Evaluation datasets

• Putnam100 contains 50 official solutions to 46 problems and invalid solutions generated by three models, screened against official references and independently verified by human experts.Source: §C.1 · p. 24
• H2V’s 200 solutions to 79 problems have 1,860 expert-labeled steps; five solutions were relabeled invalid after re-examination, with the changes independently confirmed by an expert.The five relabelings comprised four solutions with false steps and one omitting a necessary upper-bound direction.Source: §C.1 · pp. 24–25
• FirstProof-Eval contains 94 solutions to the 20 First Proof problems: 17 human-written, 39 generated by GPT and Gemini models, and 38 publicly released, all with human-assigned validity labels.Source: §C.1 · p. 25
• In H2V solution 62, a counterexample shows that an interior endpoint of a vertical cut need not be a corner of the rectangle above it, invalidating the proof’s strip-decomposition premise.The authors conclude the proof’s later move-counting steps do not establish the result and relabel the solution invalid.Source: §C.1 · p. 25

C.2 Training data and supervision

• Training examples pair a problem, submitted solution, proposed error, and binary rejection target; valid-source errors are negative, while substantial errors on invalid solutions are positive after reference-assisted screening and at least 3 of 5 validation votes.Easy examples and prompts with fewer than 8,192 output tokens remaining in a 32,768-token context window are excluded.Source: §C.2 · p. 25, Table 6 · p. 26

D.1 Evaluation protocol and metrics

• Evaluation independently samples judgments without replacement and reselects the threshold maximizing empirical TNR under the specified FNR constraint in each trial; reported means and standard deviations span 2,000 trials.Evaluation solutions remain fixed across the resampling trials.Source: §D.1 · p. 26

D.2 Models and inference configurations

• Unless specified otherwise, OSVERIFY uses the same backbone for proposing and validating errors, and validation calls include the problem, full solution, focused excerpt, and proposed error.Dataset-specific policies are fixed within each experiment; the trained validator is oss with a LoRA adapter and validates errors proposed by the training-free oss proposer.Source: §D.2 · p. 26, Table 7 · p. 26

D.3 Setup of whole-solution judging and proposed-error checking

• Whole-solution judging scores the fraction of 15 judgments that reject a solution, while proposed-error checking scores the fraction of 15 votes calling an error SUBSTANTIAL.For whole solutions, TNR and FNR are fractions of the 59 invalid and 35 valid FirstProof-Eval solutions rejected; for errors, they are defined against an independent audit’s substantial versus minor or not-real labels.Source: §D.3 · p. 26

D.4 Hierarchical proposal and aggregation

• Hierarchical proposal decomposes the solution to a maximum depth of two in the main comparison, retaining each node and its descendants until the depth limit or a model judgment of atomicity, then merging identical proposed errors.The solution score is the largest SUBSTANTIAL-vote count among its proposed errors, or zero if none are proposed; the solution is rejected when that score reaches the selected positive threshold.Source: §D.4 · p. 27

D.5 Online GRPO training

• Validator fine-tuning uses online GRPO, sampling 32 examples per step and generating eight fresh rollouts per example, with sampling balanced between valid- and invalid-side examples within each domain.Rollouts receive reward for matching the binary target; truncated responses and responses without a parseable verdict receive zero reward.Source: §D.5 · p. 27
• Training skips zero-variance groups, applies per-token KL penalties, and takes one policy-gradient update per step; the reported checkpoint is after 400 steps.Table 8 lists the hyperparameters.Source: §D.5 · p. 27, Table 8 · p. 28

E Representative Issues Found in Research Papers

• Appendix E presents representative issues and proposed corrections confirmed by the papers’ authors; Table 9 counts reported issues verified as real by human experts.Direct review uses the same backbone as OSVERIFY through its web interface.Source: E Representative Issues Found in… · p. 28, Table 9 · p. 28

E.1 Examples from Zhu [72]

• In Zhu [72], an ordinary flip is used where the graded flip is required, so the final Koszul correction adds an unwanted minus sign on odd ⊗odd.The expert comment says the subtle error is fixable and does not substantially affect the main result, but must be corrected for the statement to hold as written.Source: §E.1 · pp. 28–29
• The cited argument says the degree-four part has dimension at most one, so reducing verification of the action to H2 is invalid.The repair removes the degree-two generation assertion and justifies the sign formula on H2j(Grµ) for every j.Source: §E.1 · p. 29
• For G = GL2 and λ = µ = (1, 0), the shifted-intersection-complex normalization puts open-stratum stalk cohomology in degree −2, yielding q−1 instead of 1 and a later identity predicting −id instead of id.The correction must reconcile the Cµ normalization with the subsequent stalk-polynomial formulas and costalk filtration; the expert comment calls the paper internally inconsistent.Source: §E.1 · p. 29
• For n = N = 1, µ1 = (1), and β = p, the proposed convolution-fiber identification fails: the original fiber is a point, but the displayed composite has valuation 2 and an empty relative-position-zero locus.The proposed arrow and weight-index corrections restore the intended lemma and the properness of the fibers used later.Source: §E.1 · p. 29
• For G = SL2 × SL2, defining J = S \ {0} leaves an affine A1 component, making WJ infinite and the subsequent construction of wJ and longest double-coset representatives undefined.The proposed repair corrects the hyperspecial subset J and related definitions, and supplies the componentwise extension needed to retain the stated generality of G.Source: §E.1 · pp. 29–30

F.1 Proposer prompt

• The proposer must anchor each candidate in the solution, explain its failure and impact, filter out routine or immaterial issues, and provide fields tailored to localized or holistic errors.It is instructed to prefer one strong candidate over vague duplicates and to use a defined error-type list and JSON output schema.Source: §F.1 · pp. 34–35

F.2 Validator prompt

• The validator checks whether an objection targets the actual claim, respects its conditions and full context, and identifies a genuinely absent obligation before labeling it NOT_REAL, MINOR, or SUBSTANTIAL.A missing or compressed derivation alone establishes at most a gap, not a false conclusion; severity depends on whether the verified issue makes the answer rejectable under the active standard.Source: §F.2 · pp. 37–38

F.3 Dataset-specific policies

• Dataset policies set severity by benchmark standard: H2V treats missing or invalid nontrivial required arguments as substantial, whereas FirstProof-Eval accepts coherent expert sketches unless a load-bearing flaw or unattempted required component is verified.Under the FirstProof-Eval policy, local mistakes removable without changing the core proof and gaps that only call for more exposition are not by themselves evidence that the route fails.Source: §F.3 · pp. 39–40