Pith. sign in

REVIEW 1 cited by

The Isabelle ENIGMA

Not yet reviewed by Pith; the record is open.

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

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

arxiv 2205.01981 v1 pith:UEMNADFT submitted 2022-05-04 cs.AI cs.LGcs.LO

Zarathustra A. Goertzel , Jan Jakubův , Cezary Kaliszyk , Miroslav Olšák , Jelle Piepenbrock , Josef Urban This is my paper · ORCID
classification cs.AIcs.LGcs.LO
keywords isabelleenigmaproblemstargetedbestpremisepreviousselection
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance for the Isabelle problems, targeted versions of neural premise selection, and targeted strategies for E. The methods are trained in several iterations over hundreds of thousands untyped and typed first-order problems extracted from Isabelle. Our final best single-strategy ENIGMA and premise selection system improves the best previous version of E by 25.3% in 15 seconds, outperforming also all other previous ATP and SMT systems.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis

    cs.LG 2025-01 conditional novelty 7.0 of 10

    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.

Pith tools