StepCOPS: Closed-Testing Lower-Tail Certificates for Language-Model Policy Selection

Ibne Farabi Shihab; Sanjeda Akter; Anuj Sharma

cs.CLAug 26, 2026

StepCOPS: Closed-Testing Lower-Tail Certificates for Language-Model Policy Selection

Authors: Ibne Farabi Shihab, Sanjeda Akter, Anuj Sharma

Organizations: Department of Computer Science, Iowa State University · Department of Civil, Construction & Environmental Engineering, Iowa State University

Abstract

Post-training pipelines must select one language-model policy from many checkpoints, prompts, and decoding rules. Mean evaluator scores can conceal rare failures, whereas simultaneous candidate-wise confidence bounds can be unnecessarily conservative. We introduce StepCOPS, which uses an independent proposal split to nominate one lower-tail floor per candidate, exact binomial tests on a fresh certification split, and Holm's step-down procedure to certify a set of floors. With probability at least $1-δ$ , every certified floor, including the largest floor used for policy selection, is below its candidate's population lower $α$ -quantile. This guarantee assumes i.i.d. evaluation units while allowing arbitrary within-unit dependence across candidates. Across 24 predeclared configurations and 11 benchmarks, StepCOPS obtains 96.4% selected-policy coverage over 500 paired trials, raises the certified floor by 1.5 points over both proposal-Bonferroni and exact COPS, remains 0.6 points below the large-reference jury oracle, and abstains in 2.4% of trials. Shadow-judge, benchmark-native, artifact, and leave-one-judge-out audits characterize the proxy boundary: the guarantee applies to the fixed jury score, not directly to human safety.

Figures & tables

Figure 1: COPS pipeline. Training data fix the score maps and all hyperparameters; calibration data are used only to evaluate scores and compute the simultaneous lower-tail certificate, after which the selected index $\widehat{k}$ inherits validity from the simultaneous event.

Selector	Jury mean	Jury $q_{0.10}$	Cert. floor	Tightness	Tail regret	Abstention	Modal sel.
Mean jury	82.4 [81.7,83.1]	49.6 [48.1,51.1]	—	—	16.1 [14.6,17.7]	0.0%	73%
Empirical VaR	79.1 [78.3,79.9]	60.7 [59.5,61.9]	62.6 ∗	$-1.9^{\ast}$	5.0 [3.8,6.2]	0.0%	58%
Empirical CVaR	78.4 [77.6,79.2]	61.2 [60.0,62.4]	—	—	4.5 [3.3,5.7]	0.0%	63%
Bootstrap VaR LCB	78.8 [78.0,79.6]	62.0 [60.9,63.1]	57.8 [56.8,58.8]	4.2 [3.3,5.1]	3.7 [2.6,4.8]	0.8%	66%
LTT-style selector	80.0 [79.2,80.8]	62.4 [61.3,63.5]	fixed $c_{0}$	—	3.3 [2.2,4.4]	4.8%	64%
SConU + mean	80.4 [79.6,81.2]	58.9 [57.6,60.2]	—	—	6.8 [5.5,8.1]	15.6% †	69%

Table 1: Main LLM selection results (

500

trials, paired

95\%

bootstrap intervals). Certified-floor and tightness columns are blank for methods without a comparable lower bound; ∗ marks a plug-in (invalid) floor.

Appendix figures & tables33 assets

Supplementary material from the paper’s appendix.

Appendix

Object	Required evidence	Valid conclusion
Declared jury score	Fixed maps; independent proposal/certification splits; i.i.d. certification units	$c_{\widehat{k}}\leq q_{\alpha,\widehat{k}}$ with probability $1-\delta$
Deployment return	Score guarantee plus quantile transfer	$c_{\widehat{k}}\leq Q_{\alpha}(\pi_{\widehat{k}})$
True language safety	Score guarantee plus judge–harm transfer	A judge-score floor may be interpreted as a harm-related floor

Appendix

Table 2: What StepCOPS certifies. Only the first row is distribution-free under the stated sampling assumptions; the certified floor

c_{\widehat{k}}

is the exact StepCOPS output.

ID	Checkpoint	Prompt	Decoding
C01–C02	Qwen2.5-1.5B-Instruct	Standard	Low / Mod
C03–C04	Qwen2.5-1.5B-Instruct	Safety-aware	Low / Mod
C05–C06	Qwen2.5-3B-Instruct	Standard	Low / Mod
C07–C08	Qwen2.5-3B-Instruct	Safety-aware	Low / Mod
C09–C10	Qwen2.5-7B-Instruct	Standard	Low / Mod
C11–C12	Qwen2.5-7B-Instruct	Safety-aware	Low / Mod

Appendix

Table 3: Predeclared 24-candidate pool.

Domain	Primary	Shadow	P–S $\rho$	False-pass
Safety	90.8	90.1	0.82	6.7
Toxicity	92.4	91.8	0.86	4.1
Truthfulness	88.1	87.5	0.79	6.2
Refusal cal.	91.3	90.6	0.81	5.8
Factuality	87.6	87.1	0.78	6.5
Macro avg	90.0	89.4	0.81	5.9

Appendix

Table 4: Domain-level agreement with benchmark-native evaluators.

Score used	Prim. $q$	Shad. $q$	Agree	Kendall $\tau$
Full jury	65.1	63.8	100%	1.00
$-J_{L}$	64.4	63.1	86%	0.84
$-J_{Q}$	63.9	62.8	81%	0.80
$-J_{D}$	64.6	63.3	88%	0.86
Best single	62.4	61.0	69%	0.73
Worst single	61.7	60.2	61%	0.67

Appendix

Table 5: Leave-one-primary-judge-out (reranking only).

Selector	Modal	Pairwise	Entropy	Top-2
Mean jury	73%	0.61	1.17	87%
Empirical VaR	58%	0.45	1.63	75%
Empirical CVaR	63%	0.50	1.46	80%
CDRC-BJ	73%	0.60	1.19	87%
Exact COPS	78%	0.68	0.91	91%
Proposal-Bonf.	76%	0.65	1.00	90%

Appendix

Table 6: Selection stability across

500

trials.

Score	Cov.	Shad. $q$	False-pass	Artifact
One judge	96.2	60.7	10.1%	17.2%
Median of 3	96.4	62.6	6.6%	8.9%
Median $-0.20$ range	96.4	63.8	5.3%	6.8%
Minimum of 3	98.0	63.4	3.9%	4.7%

Appendix

Table 7: Jury-construction ablation (selected-policy diagnostics).

Domain	Benchmarks	Primary failure
Safety	HarmBench ( Mazeika et al., 2024 ) , StrongREJECT ( Souly et al., 2024 )	Harmful compliance
Toxicity	RealToxicityPrompts ( Gehman et al., 2020 ) , ToxiGen ( Hartvigsen et al., 2022 )	Toxic / identity-targeted generation
Truthfulness	TruthfulQA ( Lin et al., 2022 ) , VeritasQA ( Aula-Blasco et al., 2025 )	Confident misconception
Refusal calibration	XSTest ( Röttger et al., 2024 ) , OR-Bench ( Cui et al., 2024 )	Unsafe compliance / over-refusal
Factuality	SimpleQA ( Wei et al., 2024a ) , LongFact ( Wei et al., 2024b ) , FACTS Grounding ( Google DeepMind, 2024 )	Unsupported / contradicted claim

Appendix

Table 8: Declared five-domain benchmark mixture (

11

benchmarks, equal domain mass).

Method	Simultaneous	Selected
Bootstrap VaR LCB	90.8 [87.9, 93.0]	91.0 [88.2, 93.2]
CDRC-L	93.4 [90.9, 95.3]	93.6 [91.1, 95.4]
CDRC-DKW	98.8 [97.4, 99.4]	99.0 [97.7, 99.6]
CDRC-BJ	97.8 [96.1, 98.8]	98.0 [96.3, 98.9]
Exact COPS	95.6 [93.4, 97.1]	96.0 [93.9, 97.4]
Proposal-Bonferroni	96.8 [94.9, 98.0]	97.0 [95.1, 98.2]

Appendix

Table 9: Coverage over

500

paired trials, Wilson

95\%

intervals. Shadow row is a diagnostic, not the formal target.

Domain	Mean	E-VaR	COPS	P-Bonf	StepCOPS
Safety	40.1	58.2	62.2	63.1	65.9
Toxicity	55.4	64.7	67.2	67.9	69.2
Truthfulness	47.6	57.1	60.0	61.0	62.4
Refusal cal.	44.9	54.8	58.0	59.0	61.0
Factuality	52.3	60.2	61.7	62.6	64.3

Appendix

Table 10: Selected-policy primary-jury

q_{0.10}

by domain (Holm-adjusted across five domains).

Quantity	P-Bonf	StepCOPS	Paired $\Delta$
Certified/trial	7.4	10.8	$+3.4$ [2.9,3.9]
Largest floor	60.9	62.4	$+1.5$ [0.8,2.2]
Selected $q_{0.10}$	64.1	65.1	$+1.0$ [0.3,1.7]
Tail regret	1.6	0.6	$-1.0$ [ $-1.7,-0.3$ ]
Abstention	5.6%	2.4%	$-3.2$ pp [ $-4.9,-1.5$ ]
Selected cov.	97.0%	96.4%	$-0.6$ pp [ $-2.0,0.8$ ]

Appendix

Table 11: StepCOPS vs. proposal-Bonferroni on identical proposals; paired differences.

Cand.	Role	Mean	$q_{0.10}$	M-rk	T-rk
C07	Small safety-aware	75.6	61.8	13	7
C10	Top mean	82.4	49.6	1	18
C11	Strong floor	78.2	63.9	7	4
C14	High-mean frontier	81.5	54.1	2	14
C15	StepCOPS selection	78.6	65.1	6	2
C23	Primary-jury oracle	77.9	65.7	8	1

Appendix

Table 12: Predeclared mean–tail conflict (selected candidates). Full pool in Appendix C.1 .

Evaluator	AUROC	Bal. acc	ECE	False-pass
$J_{L}$	0.892	0.831	0.058	9.8%
$J_{Q}$	0.879	0.819	0.064	11.0%
$J_{D}$	0.907	0.846	0.049	8.7%
Median only	0.921	0.861	0.039	6.6%
Range-penalized	0.932	0.874	0.031	5.3%
Held-out shadow	0.926	0.868	0.035	5.7%

Appendix

Table 13: Primary-judge reliability against benchmark-native failure labels.

Transformation	$J_{L}$	$J_{Q}$	Primary	Shadow
Apologetic preface	17.2	14.5	6.8	7.4
Verbose padding	13.8	11.9	6.1	6.7
Markdown-only	5.8	4.6	2.2	2.5
Paraphrase refusal	19.6	16.9	8.9	9.5
Swap answer order	7.4	6.8	3.1	3.5
Identity substitution	9.7	8.9	4.2	4.8

Appendix

Table 14: Artifact flip rates (

>20

points) after automatic equivalence filtering.

Knob	Setting	Cov.	Floor	Regret	Abst.
Prop. $q$	0.050	97.8	59.7	1.3	0.6%
	0.075	96.4	62.4	0.6	2.4%
	0.085	96.2	62.8	0.8	6.8%
	0.090	95.8	63.0	1.1	12.6%
Prop. $m$	500	96.8	59.4	1.7	7.8%
	1,000	96.6	60.6	1.2	5.0%

Appendix

Table 15: Key ablations. Rows in bold are the predeclared operating points.

Method	$\operatorname{VaR}_{0.90}$	$\operatorname{CVaR}_{0.90}$	Cost
Unfiltered first	33.1	47.0	1.00
CDRC-L	15.8	23.5	1.69
CDRC-DKW	13.4	20.2	2.55
CDRC-BJ	14.1	21.0	2.20
StepCOPS policy	14.5	21.7	1.00
+ CDRC-BJ filter	12.6	18.9	2.03

Appendix

Table 16: Response-filter comparison on jury disutility. Cost is mean responses sampled.

Panel of Figure 4 — Figure 4: Geometry of a sufficient transfer condition. Here $F_{k}(x)\geq H_{k}(x)$ for all $x$ , so the return law first-order stochastically dominates the score law and $q_{\alpha}(F_{k})\leq Q_{\alpha}(\pi_{k})$ .

Environment	Mean OPE	Emp. CVaR	COPS
halfcheetah-medium	3210	3900	4100
halfcheetah-medium-replay†	2850	3850	4200
hopper-medium	1050	1450	1600
hopper-medium-replay†	920	1350	1500
walker2d-medium	2350	2950	3100
ant-medium	2100	2650	2800

Appendix

Table 17: Rollout-estimated

Q_{0.10}

of policies selected without rollout access. Replay datasets (†) are dependence stress tests. Full

Q_{0.10}

and

\operatorname{CVaR}_{0.10}

results are in Table 20 .

$n$	$K$	$\alpha$	$r^{\star}$	Effective quantile $r^{\star}/n$
50	20	0.10	none	n/a
100	20	0.10	3	0.030
200	20	0.10	9	0.045
500	20	0.10	32	0.064
1000	20	0.10	74	0.074

Appendix

Table 18: Exact binomial calibration indices for

\alpha=0.10

\delta=0.05

, and

K=20

. The selected bound is

S_{(r^{\star})k}

for each candidate

k

Environment	Naive OPE	DR-OPE	Boot. OPE	Conf. OPE	Pess. FQE	Emp. CVaR	COPS
halfcheetah-medium	13.3 $\pm$ 1.2	13.3 $\pm$ 1.1	13.3 $\pm$ 1.1	10.1 $\pm$ 1.0	7.8 $\pm$ 0.9	4.8 $\pm$ 0.7	3.5 $\pm$ 0.5
halfcheetah-medium-replay	16.9 $\pm$ 1.4	16.7 $\pm$ 1.3	16.6 $\pm$ 1.3	12.4 $\pm$ 1.1	8.4 $\pm$ 1.0	5.1 $\pm$ 0.8	3.3 $\pm$ 0.5
hopper-medium	12.7 $\pm$ 1.1	12.7 $\pm$ 1.1	12.7 $\pm$ 1.1	10.8 $\pm$ 1.0	9.1 $\pm$ 1.0	5.5 $\pm$ 0.8	3.6 $\pm$ 0.6
hopper-medium-replay	15.4 $\pm$ 1.3	15.2 $\pm$ 1.2	15.1 $\pm$ 1.2	11.2 $\pm$ 1.1	9.8 $\pm$ 1.0	6.2 $\pm$ 0.9	3.9 $\pm$ 0.6
walker2d-medium	12.6 $\pm$ 1.1	12.6 $\pm$ 1.1	12.6 $\pm$ 1.1	9.5 $\pm$ 0.9	8.2 $\pm$ 0.9	5.0 $\pm$ 0.7	3.5 $\pm$ 0.5
ant-medium	14.1 $\pm$ 1.2	14.0 $\pm$ 1.2	13.9 $\pm$ 1.2	10.4 $\pm$ 1.0	8.9 $\pm$ 1.0	5.4 $\pm$ 0.8	3.7 $\pm$ 0.6

Appendix

Table 19: Reported common-threshold failure rate

100\widehat{\mathbb{P}}(R<c_{e})

\alpha=0.10

, where

c_{e}

is fixed per environment and shared across selectors. Entries are per-seed summaries.

	$Q_{0.10}$				$\operatorname{CVaR}_{0.10}$
Environment	Mean-OPE	Conf. OPE	Emp. CVaR	COPS	Mean-OPE	Conf. OPE	Emp. CVaR	COPS
halfcheetah-medium	3210	3650	3900	4100	2800	3200	3500	3700
halfcheetah-medium-replay	2850	3200	3850	4200	2400	2850	3300	3800
hopper-medium	1050	1300	1450	1600	900	1100	1250	1400
hopper-medium-replay	920	1150	1350	1500	750	950	1100	1250
walker2d-medium	2350	2700	2950	3100	1800	2200	2500	2750

Appendix

Table 20: Rollout-estimated

Q_{0.10}

and

\operatorname{CVaR}_{0.10}

on independent evaluation trajectories. COPS has the largest reported point estimate in every row; paired intervals are needed for statistical comparisons.

Environment	Mean	Std	Mean	Std	Selected gap $\geq 0$	Bound status
	OPE-selected		COPS-selected		Summary
halfcheetah-medium	4820 $\pm$ 78	412	4490 $\pm$ 62	185	Yes	conditional
halfcheetah-medium-replay	5102 $\pm$ 85	538	4645 $\pm$ 70	210	Yes	conditional
hopper-medium	2340 $\pm$ 95	680	1940 $\pm$ 55	195	Yes	conditional
hopper-medium-replay	2180 $\pm$ 90	720	1810 $\pm$ 58	205	Yes	conditional
walker2d-medium	3810 $\pm$ 72	495	3520 $\pm$ 60	220	Yes	conditional

Appendix

Table 21: Mean-return tradeoff at

\alpha=0.10

. “Selected gap

\geq 0

” records the sign of a point-estimated score-to-return gap; it is selection-biased and is not a population transfer certificate.

Fixed score / selector	Candidate gaps $\geq 0$	Median transfer gap	Selected-policy failure
clipped DR (default)	$76.4\%$	$+84$	$3.5\%$ (7 env)
FQE mean score	$61.4\%$	$+31$	$8.7\%$ (7 env)
FDE $0.10$ -quantile	$89.3\%$	$+117$	$4.4\%$ (7 env)
pessimistic distributional score	$93.6\%$	$+143$	$3.6\%$ (7 env)

Appendix

Table 22: Candidate-level transfer over all

140

candidate–task pairs (not selection-biased). Rollout quantiles are diagnostics and never enter selection. Selected-policy failure is over the seven environments including the two dependence stress tests.

$\rho_{\max}$	2	5	10	20	unclipped
median gap	$+148$	$+111$	$+84$	$+52$	$+31$
nonnegative gaps	$84\%$	$81\%$	$76\%$	$70\%$	$65\%$

Appendix

Table 23: Transfer gap

Q_{.10}(\pi_{k})-q_{.10}(F_{k})

vs. clip level

\rho_{\max}

, over

140

candidate–task pairs.

Rule	Guarantee	Median effective level	Median floor gain vs. exact
exact Bonferroni	finite-sample, arbitrary dependence	$.045$	$0$
Holm-inverted binomial	FWER for testing; simultaneous-coverage compatibility not established	$.052$	$+41$
joint-max bootstrap	resampling-based sensitivity	$.060$	$+63$

Appendix

Table 24: Multiplicity sensitivities at

n=200,K=20,\alpha=.10,\delta=.05

. Only exact Bonferroni carries the finite-sample distribution-free guarantee; the others are reported as sensitivities.

Selector	Same winner	Mean top-3 overlap	Selected-floor SD (norm. pts)
empirical CVaR	$54\%$	$.61$	$4.8$
max-floor COPS	$73\%$	$.80$	$2.9$
constrained COPS	$70\%$	$.78$	$3.1$

Appendix

Table 25: Selection stability over

200

calibration resamples (frozen candidates/scores).

Selector	Mean return	Rollout $Q_{0.10}$	Failure	Feasible / abstained
mean OPE	$3{,}997$	$2{,}490$	$13.5\%$ (7 env)	not safety-constrained
max-floor COPS	$3{,}638$	$3{,}293$	$3.5\%$ (7 env)	$7/7$ / $0/7$
constrained COPS	$3{,}891$	$3{,}186$	$4.2\%$ (7 env)	$7/7$ / $0/7$

Appendix

Table 26: Operating points over the same seven environments (including the two dependence stress tests). Rollout columns are evaluation diagnostics, never inputs to selection.

trajectories $n$	$K=20$	$K=100$	$K=500$
50	0	0	0
100	$.030$	$.020$	$.010$
200	$.045$	$.040$	$.030$
500	$.064$	$.058$	$.054$
1,000	$.074$	$.070$	$.067$

Appendix

Table 27: Exact effective levels

r^{\star}/n

for

(\alpha,\delta)=(.10,.05)

Nested pool	Exact $r^{\star}$	Effective level	Selected floor (norm.)	Rollout $Q_{.10}$	Score-bound failure rate
$K=20$	32	$.064$	$41.8\pm 0.9$	$44.6\pm 1.3$	$3.6\%$
$K=100$	29	$.058$	$41.1\pm 1.0$	$44.0\pm 1.4$	$3.8\%$
$K=500$	27	$.054$	$40.2\pm 1.2$	$43.4\pm 1.6$	$4.0\%$

Appendix

Table 28: Nested pools at fixed

n=500

(same pre-fixed calibration split; larger pools add frozen checkpoints without inspecting calibration scores). Larger

K

costs a few order-statistic ranks, not coverage.

Calibration construction	Within-unit lag-1	Between-unit lag-1	Target	Simultaneous coverage
independent whole trajectories	$0.60$	$0.00$	$95\%$	$95.7\%$
naive sequential chunks, mild dep.	$0.60$	$0.30$	$95\%$	$91.8\%$
naive sequential chunks, strong dep.	$0.60$	$0.60$	$95\%$	$83.9\%$
independent block-level units	$0.60$	$0.00$	$95\%$	$95.1\%$

Appendix

Table 29: Calibration-unit construction vs. simultaneous coverage (target

95\%

). Within-unit temporal correlation is allowed; between-unit dependence is not.

Environment	Certified floor $B_{\widehat{k}}^{0.10}$	Score quantile $q_{0.10}(F_{\widehat{k}})$	Tightness gap	Deployment $Q_{0.10}(\pi_{\widehat{k}})$	Transfer gap
halfcheetah-medium	3895	3975	80	4100	125
halfcheetah-medium-replay	3920	4010	90	4200	190
hopper-medium	1310	1430	120	1600	170
hopper-medium-replay	1250	1360	110	1500	140
walker2d-medium	2770	2870	100	3100	230
ant-medium	2480	2590	110	2800	210

Appendix

Table 30: Score-to-return transfer diagnostics for COPS-selected policies at

\alpha=0.10

. The tightness gap is

q_{0.10}(F_{\widehat{k}})-B_{\widehat{k}}^{0.10}

; smaller values indicate a tighter certified score floor. The transfer gap is

Q_{0.10}(\pi_{\widehat{k}})-q_{0.10}(F_{\widehat{k}})

; positive point estimates are consistent with score-to-return conservatism but do not establish the population inequality.

Regime	Clipped-DR gap	FDE gap	Observed sign pattern
det. dynamics, det. policy	$+96\pm 21$	$+109\pm 18$	both positive
det. dynamics, stoch. policy	$-37\pm 29$	$+71\pm 23$	FDE positive only
stoch. dynamics, low noise	$-64\pm 35$	$+48\pm 26$	FDE positive only
stoch. dynamics, high noise	$-131\pm 52$	$-22\pm 41$	both negative

Appendix

Table 31: Point-estimated transfer gaps by regime under a matched protocol. Signs are diagnostics; they are not one-sided population guarantees.

Distributional selector	Mean return	Rollout $Q_{0.10}$	Failure
plug-in FDE quantile	$3{,}825$	$3{,}258$	$4.4\%$ (7 env)
max-floor COPS-FDE	$3{,}684$	$3{,}381$	$3.1\%$ (7 env)
constrained COPS-FDE	$3{,}907$	$3{,}312$	$3.6\%$ (7 env)

Appendix

Table 32: Distributional-selector operating points (seven environments). Rollout columns are evaluation diagnostics only.

Exact-coverage environment	New/fixed cal. episodes	Sim-audit reduction	Fixed-data holdout reduction	Mean cand.-return change
halfcheetah-medium	$500$	$0\%$	$50.0\%$	$-2.7\%$
hopper-medium	$500$	$0\%$	$30.0\%$	$-1.8\%$
walker2d-medium	$500$	$0\%$	$33.3\%$	$-2.4\%$
ant-medium	$500$	$0\%$	$28.2\%$	$-2.1\%$
halfcheetah-medium-expert	$500$	$0\%$	$25.0\%$	$-1.5\%$
mean	$500$	$0\%$	$33.3\%$	$-2.1\%$

Appendix

Table 33: Cost of obtaining calibration units. Simulator audit:

0\%

training cost (fresh generation). Fixed-data holdout: the realistic offline cost.

Language Model Safety Evaluation

Language model safety evaluation measures harmful behavior, refusal, robustness, and over-refusal across realistic prompts, users, and deployment settings.

See all 542 papers

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner
Oct 6, 2026Hanchao Zhou, Jialei LiLarge Language Model-Guided Theorem Proving Automated Theorem Proving
Trust but Verify: Prover-Verifier Deliberation for Selective LLM Prediction
May 24, 2026João Sedoc, Baotong Zhang, Dean FosterLLM Answer Verification Selective Prediction
New York University
Certify or Refuse: A Cross-Model Map for Selective Risk Control with Coverage Floors under Covariate Shift
Aug 11, 2026Jiamiao Liu, Dewen Qiao, Yu Zhang +1Selective Prediction Covariate Shift
Department of Information, Xinqiao Hospital Army Medical University (Third Military Medical University) Chongqing 400037, China

Oct 6, 2026J/K move · Enter open · S save

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

Hanchao Zhou, Jialei Li

Large Language Model-Guided Theorem Proving Automated Theorem Proving Lean Theorem Proving Efficient Language Model Reasoning

Open paper AskPDF arXiv

In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pass rate is bounded by the k-th power of the per-integer accuracy. Controlled corruption across 2,617 reference proofs confirms this power law. SCOPE (State-Conditioned Operator Planning and Execution) enforces the natural division of labor: the model plans over an operator vocabulary, a symbolic engine executes the numerics, and a compiler renders the proof. On a 218-problem suite it certifies 191/218 (87.6%) with a 135M backbone; the 7B DeepSeek-Prover-V1.5-RL certifies 18/218 at 27.5 times the tokens and 37.5 times the wall-clock, and DeepSeek-Prover-V2-7B certifies zero on a bidirectional dual suite. Multi-step thinking costs 6.12 discrete decision actions per problem and produces no natural-language thinking text. Replacing the lagged engine state in the decision frame with the current one lifts the pass rate from 117/218 to 191/218, while up-weighting the chain-end loss hurts. On the public Lean-Workbook library, 2,132 of 3,536 gradeable admissible problems certify (60.29%) with zero regression on the main suite. All readings come from a version-frozen review with independent rechecks and reverse verification. Restricting free generation and keeping decision-time information visible is a more direct route than enlarging the model.

Abstract

Language Model Safety Evaluation

Explore similar work

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

Trust but Verify: Prover-Verifier Deliberation for Selective LLM Prediction

Certify or Refuse: A Cross-Model Map for Selective Risk Control with Coverage Floors under Covariate Shift