{"id":"6b25a7fe-38de-4282-b9b1-f081e6baab5d","arxiv_id":"2507.03314","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"Using partial label learning losses, especially Libra and meritocratic losses, improves the plCoP theorem prover's solved-problem count by roughly 14 to 28 percent over the MCTS-imitation baseline.","lead":"This paper casts learning to guide an automated theorem prover as a partial label learning problem, where each theorem's multiple proofs are candidate labels. It shows that two loss functions from that literature, the Libra loss and a meritocratic loss, help the plCoP prover solve more problems than training on the shortest proof or on the prover's search statistics.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Most load-bearing threat is statistical: Fig. 2 reports large variance and unclear ordering, yet Table 2's 5-iteration gains have no error bars and may reflect single, selected runs.","rationale":"I read the central claim as empirical: PLL losses, especially Libra and 0.5-meritocratic losses, produce consistent improvements over previous approaches in plCoP. The key condition for that claim is that the measured improvements are real rather than noise or selection artifacts. The paper's own Figure 2 directly undermines this condition: it reports large variance and states that no clear ordering is visible, yet the final headline numbers in Table 2 are presented as single point values without error bars or seed information. Moreover, the text says the authors selected the best-performing models from the noisy early iterations and trained them further, which can inflate apparent gains through winner's bias. This is the weakest link in the argument: even if every loss function is implemented correctly and the baseline is fair, the \"consistent\" improvement claim is not statistically supported by the reported evidence. The reader's baseline-fairness concern is legitimate, but Section 6.5 partially mitigates it by comparing with the published pGNN numbers, where Libra also shows a 7% improvement, and Appendix A shows that even single-proof training outperforms BS, suggesting the effect is not solely due to a handicapped baseline. I therefore see the missing repeated-seed, paired-error analysis as more load-bearing than the BS fairness issue. The right verdict remains CONDITIONAL: the contribution is plausible and the loss-function analysis is useful, but the central empirical claim needs confirmation with proper repetitions and ideally code release before it can be accepted as established.","tokens_in":15081,"tokens_out":5019,"duration_ms":41289,"concrete_test":"Run the full 5-iteration protocol for BS, LIBRA, and MERIT on M2K and MPTP2078 with at least 5 independent seeds (the same seeds matched across methods), holding all hyperparameters fixed, including beta=0.5. Report per-iteration mean and standard deviation and, at each iteration, the seed-matched differences LIBRA-BS and MERIT-BS with 95% confidence intervals or a paired test. The central claim survives only if the iteration-5 differences are significant and directionally consistent with Table 2; if the confidence intervals include zero, the reported 14-28% improvements are not established.","verdict_should_be":"UNCHANGED","load_bearing_attack":"To support the central claim that PLL losses (Libra, 0.5-merit) \"consistently yield further improvement\", the paper must show the improvements are not noise. Section 6.2's Figure 2, based on 5 trials, states \"The figure shows a large variance and it is not easy to identify a clear ordering among the different methods. However, LIBRA tends to perform best and BS tends to perform worse.\" The abstract and conclusion then rest on Table 2, which reports single point values at iterations 4 and 5 with no variance, no seeds, and no paired comparison. The text also says \"We take the best performing models and train them for two additional iterations\"; selecting the best-looking methods from the same noisy early curves invites winner's-bias. The headline numbers (1205 vs 1059 on M2K; 647 vs 507 on MPTP2078) could fall inside the run-to-run spread that Figure 2 itself shows. The comparison to published pGNN in Table 4 helps against the \"handicapped baseline\" objection, but those are also single historical numbers without error bars. The central claim is therefore not yet empirically secured even if the loss definitions are sound.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes to treat learning-guided automated theorem proving (ATP) as a partial label learning (PLL) problem, where each training problem is associated with a set of proofs (allowed labels) rather than a single label. It introduces several PLL loss functions (NLL, Uniform, beta-meritocratic, Libra) and studies them in the plCoP theorem prover, comparing against a baseline (BS) that imitates MCTS statistics. Experiments on the M2K, MPTP2078, and RA-2 datasets suggest that loss functions that balance among alternative proofs (Libra and 0.5-meritocratic) improve over BS and sometimes over previously published results. The paper also reports that training on a single shortest proof is better than the MCTS-imitation baseline but weaker than the balanced PLL methods.","tokens_in":15324,"tokens_out":3441,"duration_ms":38761,"significance":"If the central empirical claim is secured, the paper makes a valuable contribution by building a systematic bridge between PLL and ATP internal guidance, offering a principled treatment of alternative proofs and introducing loss functions that are directly applicable to other learning-guided provers. The paper is well situated in the literature, compares against several prior systems on standard benchmarks (M2K, MPTP2078, RA-2), and provides a useful analysis of loss-function behavior. However, the empirical support for the headline claim is currently weakened by statistical and baseline-design issues that need to be addressed before the conclusions can be considered reliable.","major_comments":[{"comment":"The central claim that balanced PLL losses 'consistently yield further improvement' is not supported by the reported statistics. Figure 2 shows large variance and the text acknowledges that 'it is not easy to identify a clear ordering among the different methods,' yet Table 2 reports single-point iteration-5 numbers (1205 vs 1059 on M2K; 647 vs 507 on MPTP2078) with no error bars, no number of seeds, and no paired comparison. Given the overlap visible in Figure 2, these differences may plausibly lie within run-to-run variance. Please report means and standard deviations across at least the five trials used in Figure 2 for all methods and all iterations, and perform a paired statistical comparison (e.g., Wilcoxon signed-rank) between BS and each PLL method.","section":"Section 6.2, Figure 2 and Table 2"},{"comment":"The baseline BS is a deliberately simplified reimplementation of pGNN (5 message-passing layers instead of 10, 10 training epochs instead of 100, and per-tree batching). The paper itself notes that BS 'surpasses pGNN in the first 4-5 iterations, but it saturates afterwards.' The improvements of LIBRA and MERIT over BS could therefore be partly an artifact of handicapping the baseline. The comparison to published pGNN values in Table 4 partially addresses this, but those are single historical numbers without error bars. Please include a stronger baseline that matches pGNN's capacity (or at least a version with the same layer count and training epochs), or provide a sensitivity analysis showing that the PLL gains are robust to the baseline's architectural simplifications.","section":"Section 6.1, Table 1 and Section 6.5, Table 4"},{"comment":"The choice of β=0.5 for the meritocratic loss is based on 'a small grid search' and is then used in the main experiments on the same datasets that serve as evaluation. This is effectively tuning on the evaluation data and can inflate reported performance. In addition, the procedure 'We take the best performing models and train them for two additional iterations' selects methods based on the noisy curves in Figure 2, which invites winner's-bias. Please either use a validation split for tuning β and for model selection, or report results for all methods at all iterations with error bars and a pre-specified selection rule.","section":"Section 5 and Section 6.2"},{"comment":"The RA-2 experiment also reports single-run numbers without error bars, yet the performance trajectories are highly non-monotonic (e.g., MERIT drops from 337 at iteration 6 to 478 at iteration 8 only to fall to 505 at iteration 10; UNIF jumps from 136 to 440 between iterations 2 and 4). Without variance estimates or repeated trials, it is difficult to distinguish method effects from noise, and the text's conclusions about the behavior of NLL-loss rest on these unstable numbers.","section":"Section 6.3, Table 3"}],"minor_comments":[{"comment":"There are several typos: 'expentially' should be 'exponentially' in the Introduction; 'compability' should be 'compatibility' in Section 6; 'candidatates' and 'futhermore' appear in Appendix A; and 'the the' appears in the Acknowledgments section.","section":"Introduction, Section 6, Appendix A, Acknowledgments"},{"comment":"The caption says 'M2k' while the rest of the paper uses 'M2K'; please make the naming consistent.","section":"Figure 2 caption"},{"comment":"The symbol D is used both for the set of all finite derivations and for the dataset of problems; please use distinct symbols to avoid confusion.","section":"Section 3"},{"comment":"The notation '±' in Table 5 (e.g., SHORT ±, LONG ±, RAND ±) is not explained in the caption; please clarify that it refers to training with both a proof and a failed derivation.","section":"Table 5 caption"}],"recommendation":"major_revision","confidential_remarks":"The paper's central idea is interesting and the loss-function comparison is a useful contribution. The main concern is that the headline improvements over BS are not yet shown to be statistically robust, and the baseline is a deliberately simplified reimplementation. The tuning of β and the selection of 'best performing models' from noisy curves also raise circularity concerns. These issues are addressable with additional experiments or analysis, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The PLL-to-ATP framing is the real contribution here. As far as I know, this is the first paper to systematically treat internal guidance for theorem proving as partial label learning, and the adaptation to sequential, infinite-output settings is thoughtful. The comparison of NLL, Uniform, Meritocratic, and Libra losses on a connection prover is new, and the finding that balanced PLL losses beat both MCTS-imitation and shortest-proof training is a plausible and useful result for the community. So the core idea deserves attention.\n\nWhat the paper does well: the authors are candid about their baseline's limitations, they confirm the shortest-proof folklore, and they show the PLL methods improve over a simplified BS baseline across several datasets. Table 4, comparing LIBRA against published pGNN and pXGB results, provides useful external context and suggests the gains are not purely an artifact of the weakened baseline. The RA-2 experiment, where alternatives are rare, is a nice probe into mechanism.\n\nNow the soft spots, in proportion. The main one is statistical. Figure 2 shows high variance and overlapping curves after 3 iterations, and the text itself admits no clear ordering is visible, yet Table 2 reports single point values at iterations 4 and 5 with no error bars, and the authors say they \"take the best performing models\" after seeing those noisy curves. That is winner's bias. The headline numbers (1205 vs 1059 on M2K, 647 vs 507 on MPTP2078) could easily fall inside the run-to-run spread shown in Figure 2. I would want paired seed reporting or at least multiple runs for the final iterations before believing the claimed double-digit gains are real rather than selection noise. The BS baseline is also a deliberately simplified reimplementation, and while Table 4 helps, those are single historical numbers too. Minor points: beta=0.5 for the meritocratic loss is chosen via small grid search on the same evaluation data, which is a mild selection-on-evaluation issue, and no code is released, which slows reproducibility.\n\nIf the authors can present variance-aware results for the main tables and ideally release the training code, the empirical claim would be much stronger. As is, I still think the paper deserves a serious referee: the framing is novel, the question is important, and the evidence is suggestive even if not yet conclusive. I would send it to review with major revision required, not desk-reject it.","headline":"A genuinely useful bridge between PLL and ATP internal guidance, but the headline improvements rest on single runs that may not survive variance.","tokens_in":15825,"tokens_out":1975,"would_cite":true,"duration_ms":25326,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Formulating proof guidance as partial label learning and training on all discovered proofs with balanced losses yields consistent gains over MCTS-imitation and single-proof training.","keywords":["partial label learning","automated theorem proving","proof search guidance","alternative proofs","Libra loss","meritocratic loss","plCoP","Monte Carlo tree search"],"falsifier":"Redo the M2K and MPTP2078 comparisons using the original pGNN training configuration (ten message-passing layers, a hundred training epochs, batches drawn across search trees) and compare Libra and 0.5-meritocratic against published pGNN results; if the advantage over the baseline shrinks to noise or reverses, the paper's claim of consistent partial-label-learning improvement would be falsified.","tokens_in":14890,"feed_emoji":"⚖️","tokens_out":10419,"duration_ms":116814,"temperature":0.7,"pith_summary":"The paper tries to establish that learning-guided theorem proving is better treated as a partial label learning problem, where each problem has several equally acceptable proofs as candidate labels, than as imitation of search-tree statistics. It argues that the choice of loss function matters: losses that spread probability across all known proofs while suppressing non-proofs, especially Libra and the 0.5-meritocratic loss, outperform both the baseline that imitates Monte Carlo tree search and training on a single shortest proof. On M2K, Libra reaches 1205 solved problems versus 1059 for the baseline after five guided iterations; on MPTP2078, the meritocratic loss reaches 647 versus 507. This matters because theorem provers routinely collect many proofs per problem, and a principled way to exploit all of them could improve proof guidance without changing the prover or the model architecture.","feed_headline":"All-proof training beats one-proof training for theorem provers","feed_subtitle":"Libra and 0.5-meritocratic losses outrun the MCTS-imitation baseline and the shortest-proof heuristic on standard benchmarks.","key_machinery":"The load-bearing machinery is the reduction of an MCTS search tree to a partial-label training set $D_{\\mathrm{MCTS}}$, in which each prover state is an input, each discovered derivation is labelled as proof, failure, or unknown, and the model's probability of a derivation is the product of the probabilities of its atomic inference steps. The loss function then determines how the policy model uses multiple proofs. The paper compares the NLL loss (winner-take-all), the uniform loss (probability spread evenly across proofs), the $\\beta$-meritocratic loss with $\\beta = 0.5$, which weights each proof by its relative model probability raised to the power $0.5$, and the Libra loss $L_{\\mathrm{Libra}} = -\\frac{1}{k}\\sum_i y_i \\log p_i + \\log(1 - \\sum_i y_i p_i)$, which averages negative log likelihood over the acceptable proofs and adds a penalty term for disallowed derivations. Libra and the 0.5-meritocratic loss both interpolate between uniform and winner-take-all behaviour while roughly preserving the probability ratios among alternative proofs, and these are the losses that carry the measured improvements.","core_discovery":"On its own terms, the central discovery is that a policy model for proof search should be trained as if each explored search tree were a partial-label dataset: proofs are the acceptable labels, failed derivations are disallowed labels, and the loss is chosen to balance probability among the proofs instead of collapsing onto one. The paper reports that on M2K the Libra loss solves 1205 problems after five iterations against 1059 for the MCTS-imitation baseline, with the 0.5-meritocratic loss close behind at 1183; on MPTP2078, the 0.5-meritocratic loss reaches 647 against 507 for the baseline. Both balanced losses beat single-proof training, where the shortest proof is the best single choice, and they beat the NLL loss, which concentrates on one proof. The authors interpret this as evidence that previous practice left useful training signal on the table, and that partial label learning methods that maintain a balance among alternative proofs consistently yield further improvement over previous approaches.","pith_inferences":["If the loss-function ordering transfers to other calculi and proof-search architectures, proof-guidance pipelines could drop the estimation of MCTS visit statistics entirely and train directly from raw search trees, removing a costly and sensitive modelling step.","Because the paper finds that the number of alternative proofs alone does not explain method rankings, a testable extension is to compare losses on corpora with controlled proof multiplicity and check whether ratio-preserving losses such as Libra and 0.5-meritocratic excel exactly when alternative proofs differ in length or shape rather than merely in count.","The failures of NLL on RA-2 hint that winner-take-all losses are fragile when proofs are rare; a principled follow-up would use failed derivations as negative labels at scale, something the paper only probes with a single failure per proof.","Since the paper abstracts away the single-true-proof assumption, one could define the learning goal as maximizing total probability mass on the set of proofs rather than on any particular proof, which would make the partial label framing exact and might motivate new losses that are invariant to proof enumeration."],"forward_implications":["On M2K, Libra-loss solves 1205 problems after five guided iterations versus 1059 for the MCTS-imitation baseline, and 0.5-meritocratic solves 1183; both improve over the NLL loss (1136) and over single-proof training with the shortest proof (1175).","On MPTP2078, 0.5-meritocratic reaches 647 problems versus 507 for the baseline, a 28 percent gain, and Libra reaches 620.","On RA-2, where Monte Carlo tree search rarely finds multiple proofs for the same problem, three of the four partial label learning losses still improve on the baseline by 19 to 24 percent, so the benefit is not solely from balancing many alternatives; the NLL loss is the exception and learns poorly.","Over ten iterations on M2K, Libra-loss outperforms the baseline by 17 percent and the previous pGNN system by 7 percent, and trails the pXGB system by only 2 percent despite pXGB using ten times the inference budget.","Adding a single failed derivation to single-proof training generally harms performance, so the paper's gains come from how proofs are weighted rather than from simply teaching the model to avoid failures."],"supporting_citations":[{"why":"furnishes the partial label learning formalism and taxonomy that the paper uses to treat alternative proofs as partial labels.","marker":"[Tian et al., 2023]"},{"why":"introduces the beta-meritocratic loss and the derivation-sampling idea that the paper transfers to proof trees.","marker":"[Guu et al., 2017]"},{"why":"proposes the Libra loss and the analysis of winner-take-all loss dynamics that motivates the balanced losses.","marker":"[Zombori et al., 2024]"},{"why":"sets up the MCTS-guided reinforcement learning loop and the finding that most benefit comes from the policy model.","marker":"[Kaliszyk et al., 2018]"},{"why":"defines the plCoP prover and its GNN-based learner, the system all experiments run on.","marker":"[Zombori et al., 2020, 2021b]"},{"why":"supplies the property-invariant graph neural network embedding reused as the model architecture.","marker":"[Ols´ak et al., 2020]"},{"why":"reports the shortest-proof training result that the single-proof experiments reproduce and compare against.","marker":"[Kuehlwein and Urban, 2013]"},{"why":"supplies the policy-from-MCTS-statistics training scheme that the baseline reimplements.","marker":"[Silver et al., 2017]"}],"fun_headline_variants":["Partial-label learning improves automated theorem proving","All-proof training beats single-proof for theorem provers","Multiple proof labels outperform single proof in ATP","Theorem provers gain from partial label training","Balance proofs, not collapse: partial labels for theorem provers"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The experiments assume the simplified baseline BS is a fair representative of previous guided-MCTS training, even though the paper notes BS surpasses pGNN early and then saturates, likely due to its smaller model, shorter training, and more rigid batching.","fun_headline_variants_meta":{"raw":{"variants":["Partial-label learning improves automated theorem proving","All-proof training beats single-proof for theorem provers","Multiple proof labels outperform single proof in ATP","Theorem provers gain from partial label training","Balance proofs, not collapse: partial labels for theorem provers"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000611,"raw_usage":{"total_tokens":2760,"prompt_tokens":782,"completion_tokens":1978,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":398,"completion_tokens_details":{"reasoning_tokens":1907}},"tokens_in":398,"tokens_out":1978,"duration_ms":18015,"temperature":1.0,"reasoning_tokens":1907,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T20:13:00.742868+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Redo the M2K and MPTP2078 comparisons using the original pGNN training configuration (ten message-passing layers, a hundred training epochs, batches drawn across search trees) and compare Libra and 0.5-meritocratic against published pGNN results; if the advantage over the baseline shrinks to noise or reverses, the paper's claim of consistent partial-label-learning improvement would be falsified.","supporting_citations":[{"cited_title":"Partial label learning: Taxonomy, analysis and outlook","cited_arxiv_id":null,"evidence_quote":"furnishes the partial label learning formalism and taxonomy that the paper uses to treat alternative proofs as partial labels."},{"cited_title":"From language to programs: Bridging reinforcement learning and maximum marginal likelihood","cited_arxiv_id":null,"evidence_quote":"introduces the beta-meritocratic loss and the derivation-sampling idea that the paper transfers to proof trees."},{"cited_title":"Towards Unbiased Exploration in Partial Label Learning","cited_arxiv_id":"2307.00465","evidence_quote":"proposes the Libra loss and the analysis of winner-take-all loss dynamics that motivates the balanced losses."},{"cited_title":"Property invariant embedding for automated reasoning","cited_arxiv_id":null,"evidence_quote":"supplies the property-invariant graph neural network embedding reused as the model architecture."}],"review_version":1}