Partial Label Learning for Automated Theorem Proving

Bal\'azs Indruck; Zsolt Zombori

REVIEW 4 major objections 4 minor 36 references

Partial Label Learning for Automated Theorem Proving

T0 review · 4 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read 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.

desk verdict A genuinely useful bridge between PLL and ATP internal guidance, but the headline improvements rest on single runs that may not survive variance. read the letter →

arxiv 2507.03314 v1 pith:L3VQUYXO submitted 2025-07-04 cs.LO cs.AI

Zsolt Zombori , Balázs Indruck This is my paper · ORCID

classification cs.LOcs.AI

keywords partiallabellearningautomatedtheoremprovingproofsearchguidancealternativeproofsLibralossmeritocraticplCoPMonteCarlotree

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

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.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the 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.

What 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.

Now 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.

If 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.

Referee Report

4 major / 4 minor

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.

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 (4)

[Section 6.2, Figure 2 and Table 2] 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 6.1, Table 1 and Section 6.5, Table 4] 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 5 and Section 6.2] 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 6.3, Table 3] 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.

minor comments (4)

[Introduction, Section 6, Appendix A, Acknowledgments] 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.
[Figure 2 caption] The caption says 'M2k' while the rest of the paper uses 'M2K'; please make the naming consistent.
[Section 3] 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.
[Table 5 caption] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation; the central claim is an external benchmark result, not a consequence of the loss definitions or fitted parameters.

full rationale

The paper's main contribution is a reformulation: it maps learning to guide proof search onto Partial Label Learning and then empirically compares several existing PLL losses (NLL, Uniform, beta-merit, Libra) inside the plCoP system. The reported improvements are measured by the number of problems solved by guided MCTS on external benchmarks (M2K, MPTP2078, RA-2), not derived from the loss equations by construction. The losses are imported from previous literature; Libra-loss is taken from Zombori et al. (2024), a paper that shares an author with the present work, but that prior paper is a general PLL analysis that does not include the ATP experiments reported here, so the citation is not load-bearing for the new empirical result. The beta=0.5 choice for the meritocratic loss is based on a small grid search, and the paper chooses the best-performing models for additional iterations; these are hyperparameter-selection and winner's-bias concerns that could threaten statistical validity, but they are not examples of a fitted parameter being renamed as a prediction or of an equation reducing to its inputs. The paper explicitly acknowledges large variance in Figure 2 and the difficulty of ordering methods, and the final tables lack error bars; this is a robustness limitation, not circularity. Similarly, the BS baseline is a simplified reimplementation of pGNN, which may make the comparison less fair, but it does not make the result equivalent to the input by definition. No step in the derivation chain equates the claimed improvement with the training objective or with a self-citation, so no significant circularity is present.

Assumptions & free parameters 1 free parameters · 4 assumptions · 0 invented entities

No new physical or mathematical entities are introduced. The central empirical claim depends on one tuned hyperparameter (beta=0.5) and on several domain assumptions about the adequacy of policy-only, MCTS-sampled training.

free parameters (1)

beta in 0.5-meritocratic loss = 0.5
Selected by a small grid search on the evaluation datasets (Section 5: 'Based on a small grid search, we use beta = 0.5'). The MERIT results in Tables 2 and 3 depend on this choice.

assumptions (4)

domain assumption The probability of a derivation is the product of the policy probabilities at each step (Section 3, Sequential Prediction).
This factorization connects atomic policy predictions to derivation-level losses and is used to apply PLL losses to the policy model.
domain assumption The value model has minor effect on plCoP performance, so policy-only training is sufficient (Section 4, citing Kaliszyk et al. 2018).
All experiments use policy-only training; if the value model contributed substantially, the loss comparisons could change.
domain assumption PLL's single-true-label assumption does not affect learning because the true label is unknown during training (Section 3, No Single True Proof).
This justifies applying PLL theory to a setting where all proofs are equally valid demonstrations of the theorem.
domain assumption The derivations discovered by MCTS form an adequate sample of the infinite derivation space (Section 3, Infinite Output Space).
The partial dataset DMCTS is the only supervision considered; unobserved proofs and derivations are ignored.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Partial Label Learning for Automated Theorem Proving." pith.science (2026). https://pith.science/paper/L3VQUYXO

@misc{pith2026250703314,
  author       = {Pith},
  title        = {Pith review of: Partial Label Learning for Automated Theorem Proving},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/L3VQUYXO}},
  note         = {Machine review of arXiv:2507.03314}
}

read the original abstract

We formulate learning guided Automated Theorem Proving as Partial Label Learning, building the first bridge across these fields of research and providing a theoretical framework for dealing with alternative proofs during learning. We use the plCoP theorem prover to demonstrate that methods from the Partial Label Learning literature tend to increase the performance of learning assisted theorem provers.

Figures

Figures reproduced from arXiv: 2507.03314 by the authors.

**Figure 1.** Complete leanCoP search DAG of a simple theorem. Each node represents a leanCoP tableau, which is a directed tree whose nodes are labelled by first order literals. Tableau trees and further details are provided in Appendix D. In Section 6 we compare different PLL methods for training policy and evaluate them via the guided MCTS of plCoP. 5 PLL Methods for Policy Training In this section, we give an overview of recen… view at source ↗

**Figure 2.** Number of problems solved on the M2k and MPTP dataset by guided MCTS. The curves [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗

**Figure 3.** Aggregate model predicted probability of the proof derivations in the training data, for [PITH_FULL_IMAGE:figures/full_fig_p016_3.png] view at source ↗

Figures from the paper (2 more)

**Figure 4.** Figure 4: Complete leanCoP search DAG of a simple theorem (pelletier21). Each node represents a leanCoP tableau, which is a directed tree whose nodes are labelled by first order literals. Tableau trees are provided in [PITH_FULL_IMAGE:figures/full_fig_p017_4.png]

**Figure 5.** Figure 5: Tableau trees 19 [PITH_FULL_IMAGE:figures/full_fig_p019_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

36 extracted references · 27 canonical work pages

[1]

Premise selection for mathematics by corpus analysis and kernel methods

Jesse Alama, Tom Heskes, Daniel K\" u hlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning, 52 0 (2): 0 191--213, 2014. ISSN 0168-7433. doi:10.1007/s10817-013-9286-5

doi:10.1007/s10817-013-9286-5 2014
[2]

Alemi, Fran c ois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban

Alexander A. Alemi, Fran c ois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban. Deepmath - D eep S equence M odels for P remise S election. In Proceedings of the 30th International Conference on Neural Information Processing Systems, NIPS'16, pages 2243--2251, USA, 2016. Curran Associates Inc. ISBN 978-1-5108-3881-9. URL http://dl...

work page arXiv 2016
[3]

Thinking fast and slow with deep learning and tree search

Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. In Proceedings of the 31st International Conference on Neural Information Processing Systems, NIPS'17, page 5366–5376, Red Hook, NY, USA, 2017 a . Curran Associates Inc. ISBN 9781510860964

work page 2017
[4]

Thinking fast and slow with deep learning and tree search

Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. CoRR, abs/1705.08439, 2017 b . URL http://arxiv.org/abs/1705.08439

arXiv 2017
[5]

Lucas, Peter I

Cameron Browne, Edward Jack Powley, Daniel Whitehouse, Simon M. Lucas, Peter I. Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez Liebana, Spyridon Samothrakis, and Simon Colton. A survey of monte carlo tree search methods. IEEE Transactions on Computational Intelligence and AI in Games, 4: 0 1--43, 2012

work page 2012
[6]

XGBoost : A scalable tree boosting system

Tianqi Chen and Carlos Guestrin. XGBoost : A scalable tree boosting system. In Proceedings of the 22Nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD '16, pages 785--794, New York, NY, USA, 2016. ACM. ISBN 978-1-4503-4232-2. URL http://doi.acm.org/10.1145/2939672.2939785

arXiv 2016
[7]

Learning from partial labels

Timothee Cour, Ben Sapp, and Ben Taskar. Learning from partial labels. Journal of Machine Learning Research, 12 0 (5): 0 1501--1536, 2011. URL https://www.jmlr.org/papers/volume12/cour11a/cour11a.pdf

work page 2011
[8]

A deep reinforcement learning approach to first-order logic theorem proving

Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. A deep reinforcement learning approach to first-order logic theorem proving. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Inno...

2021

Show all 36 references

[9]

Partial label learning with self-guided retraining

Lei Feng and Bo An. Partial label learning with self-guided retraining. In AAAI, 2019. URL https://dl.acm.org/doi/10.1609/aaai.v33i01.33013542

2019 doi
[10]

Provably consistent partial-label learning

Lei Feng, Jiaqi Lv, Bo Han, Miao Xu, Gang Niu, Xin Geng, Bo An, and Masashi Sugiyama. Provably consistent partial-label learning. In NeurIPS , 2020. URL https://dl.acm.org/doi/abs/10.5555/3495724.3496643

2020
[11]

From language to programs: Bridging reinforcement learning and maximum marginal likelihood

Kelvin Guu, Panupong Pasupat, Evan Liu, and Percy Liang. From language to programs: Bridging reinforcement learning and maximum marginal likelihood. In ACL , 2017. URL https://aclanthology.org/P17-1097

2017
[12]

Holden and Konstantin Korovin

Edvard K. Holden and Konstantin Korovin. Heterogeneous heuristic optimisation and scheduling for first-order theorem proving. In Fairouz Kamareddine and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Rom...

2021 doi
[13]

ENIGMA: efficient learning-based inference guiding machine

Jan Jakub u v and Josef Urban. ENIGMA: efficient learning-based inference guiding machine. In Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings , pages 292--302, 2017. doi:10.1007/978-3-319-62075-6\_20. UR...

2017 doi
[14]

Learning with multiple labels

Rong Jin and Zoubin Ghahramani. Learning with multiple labels. In NeurIPS , 2002. URL https://dl.acm.org/doi/10.5555/2968618.2968733

2002
[15]

Mizar40 dataset, 2015

Cezary Kaliszyk and Josef Urban. Mizar40 dataset, 2015. https://github.com/JUrban/deepmath

2015
[16]

M2K dataset, 2018

Cezary Kaliszyk and Josef Urban. M2K dataset, 2018. https://github.com/JUrban/deepmath/blob/master/M2k_list

2018
[17]

Reinforcement learning of theorem proving

Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Ols \' a k. Reinforcement learning of theorem proving. In NeurIPS, pages 8836--8847, 2018

2018
[18]

Learning from multiple proofs: First experiments

Daniel Kuehlwein and Josef Urban. Learning from multiple proofs: First experiments. In Pascal Fontaine, Renate A. Schmidt, and Stephan Schulz, editors, PAAR-2012. Third Workshop on Practical Aspects of Automated Reasoning, volume 21 of EPiC Series in Computing, pages 82--94. E...

2012 doi
[19]

Males: A framework for automatic tuning of automated theorem provers

Daniel K \" u hlwein and Josef Urban. Males: A framework for automatic tuning of automated theorem provers. J. Autom. Reason., 55 0 (2): 0 91--116, 2015. doi:10.1007/S10817-015-9329-1. URL https://doi.org/10.1007/s10817-015-9329-1

2015 doi
[20]

A conditional multinomial mixture model for superset label learning

Liping Liu and Thomas Dietterich. A conditional multinomial mixture model for superset label learning. In NeurIPS , 2012. URL https://dl.acm.org/doi/10.5555/2999134.2999196

2012
[21]

Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk

Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In 21st International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2017

2017
[22]

Classification with partial labels

Nam Nguyen and Rich Caruana. Classification with partial labels. In KDD, 2008. URL https://doi.org/10.1145/1401890.1401958

2008
[23]

Property invariant embedding for automated reasoning

Miroslav Ols \' a k, Cezary Kaliszyk, and Josef Urban. Property invariant embedding for automated reasoning. In Giuseppe De Giacomo, Alejandro Catal \' a , Bistra Dilkina, Michela Milano, Sen \' e n Barro, Alberto Bugar \' n, and J \' e r \^ o me Lang, editors, ECAI 2020 - 24t...

2020
[24]

leanCoP : lean connection-based theorem proving

Jens Otten and Wolfgang Bibel. leanCoP : lean connection-based theorem proving. J. Symb. Comput., 36: 0 139--161, 2003

2003
[25]

Loos, Markus N

Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. CoRR, abs/1905.10006, 2019. URL http://arxiv.org/abs/1905.10006

1905 arXiv
[26]

Atpboost: Learning premise selection in binary setting with atp feedback

Bartosz Piotrowski and Josef Urban. Atpboost: Learning premise selection in binary setting with atp feedback. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning, pages 566--574, Cham, 2018. Springer International Publishing. ISBN 978-3-319-94205-6

2018
[28]

Breeding theorem proving heuristics with genetic algorithms

Simon Sch \" a fer and Stephan Schulz. Breeding theorem proving heuristics with genetic algorithms. In Georg Gottlob, Geoff Sutcliffe, and Andrei Voronkov, editors, Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015 , volume 36 of EP...

2015 doi
[29]

Sifre, Dharshan Kumaran, Thore Graepel, Timothy P

David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, L. Sifre, Dharshan Kumaran, Thore Graepel, Timothy P. Lillicrap, Karen Simonyan, and Demis Hassabis. Mastering chess and shogi by self-play with a general reinforceme...

2017 arXiv
[30]

Partial label learning: Taxonomy, analysis and outlook

Yingjie Tian, Xiaotong Yu, and Saiji Fu. Partial label learning: Taxonomy, analysis and outlook. Neural Networks, 161 0 (C): 0 708--734, 2023. URL https://doi.org/10.1016/j.neunet.2023.02.019

2023 doi
[31]

Malarea: a metasystem for automated reasoning in large theories

Josef Urban. Malarea: a metasystem for automated reasoning in large theories. In Geoff Sutcliffe, Josef Urban, and Stephan Schulz, editors, Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007 , vo...

2007
[32]

Blistr: The blind strategymaker

Josef Urban. Blistr: The blind strategymaker. In Georg Gottlob, Geoff Sutcliffe, and Andrei Voronkov, editors, Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015 , volume 36 of EPiC Series in Computing, pages 312--319. EasyChair, 201...

2015 doi
[33]

Premise selection for theorem proving by deep graph embedding

Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, 4-9 December 2017, Long Beach, CA, USA , p...

2017
[34]

Leveraged weighted loss for partial label learning

Hongwei Wen, Jingyi Cui, Hanyuan Hang, Jiabin Liu, Yisen Wang, and Zhouchen Lin. Leveraged weighted loss for partial label learning. In ICML, 2021. URL http://proceedings.mlr.press/v139/wen21a.html

2021
[35]

Zsolt Zombori, Josef Urban, and Chad E. Brown. Prolog technology reinforcement learning prover - (system description). In Nicolas Peltier and Viorica Sofronie - Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4...

2020 doi
[37]

The role of entropy in guiding a connection prover

Zsolt Zombori, Josef Urban, and Miroslav Ols \' a k. The role of entropy in guiding a connection prover. In Anupam Das and Sara Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 30th International Conference, TABLEAUX 2021, Birmingham, UK, Septem...

2021 doi
[38]

Towards unbiased exploration in partial label learning

Zsolt Zombori, Agapi Rissaki, Krist\' o f Szab\' o , Wolfgang Gatterbauer, and Michael Benedikt. Towards unbiased exploration in partial label learning. Journal of Machine Learning Research, 2024. URL https://arxiv.org/abs/2307.00465

2024 arXiv

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.

[1] [1]

Premise selection for mathematics by corpus analysis and kernel methods

Jesse Alama, Tom Heskes, Daniel K\" u hlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning, 52 0 (2): 0 191--213, 2014. ISSN 0168-7433. doi:10.1007/s10817-013-9286-5

doi:10.1007/s10817-013-9286-5 2014

[2] [2]

Alemi, Fran c ois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban

Alexander A. Alemi, Fran c ois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban. Deepmath - D eep S equence M odels for P remise S election. In Proceedings of the 30th International Conference on Neural Information Processing Systems, NIPS'16, pages 2243--2251, USA, 2016. Curran Associates Inc. ISBN 978-1-5108-3881-9. URL http://dl...

work page arXiv 2016

[3] [3]

Thinking fast and slow with deep learning and tree search

Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. In Proceedings of the 31st International Conference on Neural Information Processing Systems, NIPS'17, page 5366–5376, Red Hook, NY, USA, 2017 a . Curran Associates Inc. ISBN 9781510860964

work page 2017

[4] [4]

Thinking fast and slow with deep learning and tree search

Thomas Anthony, Zheng Tian, and David Barber. Thinking fast and slow with deep learning and tree search. CoRR, abs/1705.08439, 2017 b . URL http://arxiv.org/abs/1705.08439

arXiv 2017

[5] [5]

Lucas, Peter I

Cameron Browne, Edward Jack Powley, Daniel Whitehouse, Simon M. Lucas, Peter I. Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez Liebana, Spyridon Samothrakis, and Simon Colton. A survey of monte carlo tree search methods. IEEE Transactions on Computational Intelligence and AI in Games, 4: 0 1--43, 2012

work page 2012

[6] [6]

XGBoost : A scalable tree boosting system

Tianqi Chen and Carlos Guestrin. XGBoost : A scalable tree boosting system. In Proceedings of the 22Nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD '16, pages 785--794, New York, NY, USA, 2016. ACM. ISBN 978-1-4503-4232-2. URL http://doi.acm.org/10.1145/2939672.2939785

arXiv 2016

[7] [7]

Learning from partial labels

Timothee Cour, Ben Sapp, and Ben Taskar. Learning from partial labels. Journal of Machine Learning Research, 12 0 (5): 0 1501--1536, 2011. URL https://www.jmlr.org/papers/volume12/cour11a/cour11a.pdf

work page 2011

[8] [8]

A deep reinforcement learning approach to first-order logic theorem proving

Maxwell Crouse, Ibrahim Abdelaziz, Bassem Makni, Spencer Whitehead, Cristina Cornelio, Pavan Kapanipathi, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. A deep reinforcement learning approach to first-order logic theorem proving. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Inno...

2021