REVIEW 1 cited by
Premise Selection for Theorem Proving by Deep Graph Embedding
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
We propose a deep learning-based approach to the problem of premise selection: selecting mathematical statements relevant for proving a given conjecture. We represent a higher-order logic formula as a graph that is invariant to variable renaming but still fully preserves syntactic and semantic information. We then embed the graph into a vector via a novel embedding method that preserves the information of edge ordering. Our approach achieves state-of-the-art results on the HolStep dataset, improving the classification accuracy from 83% to 90.3%.
Forward citations
Cited by 1 Pith paper
-
ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
ProofAug extracts progressively coarser valid proof skeletons from failed LLM proof attempts and fills them with automated theorem provers, improving miniF2F pass rates and sample efficiency in Isabelle and Lean.
Discussion (0). Continue with ORCID to comment.