Automated Theorem Proving
9개 벤치마크 · 논문 330편 · 이 태스크의 논문 보기 →
Benchmarks
miniF2F-test
miniF2F-valid
HolStep (Conditional)
HOList benchmark
HolStep (Unconditional)
Metamath set.mm
miniF2F-curriculum
CompCert
CoqGym
Most implemented
miniCTX: Neural Theorem Proving with (Long-)Contexts
Llemma: An Open Language Model For Mathematics
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
Proof Artifact Co-training for Theorem Proving with Language Models
Holophrasm: a neural Automated Theorem Prover for higher-order logic
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
Papers
OpenProver: Agentic and Interactive Theorem Proving with Lean 4
In this system paper, we present OpenProver, an open-source system for LLM-driven automated theorem proving (ATP) with integrated Lean 4 formal verification. OpenProver integrates a Planner-Worker-Verifier architecture i…
Automated Theorem ProvingCode GenerationIsabeLLM: Automated Theorem Proving Applied to Formally Verifying Consensus
Advances in Artificial Intelligence (AI) have led AI for Theorem Proving to become a promising means of formally verifying computer systems. Whilst formal verification is traditionally reserved for safety-critical system…
Automated Theorem ProvingMA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis
Large Language Models (LLMs) have made notable progress in automated theorem proving, yet existing formal benchmarks remain limited in both mathematical coverage and difficulty. Most are concentrated in areas that are ea…
Automated Theorem ProvingMathematical ReasoningKeep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4
Automated theorem proving systems built on Lean 4 increasingly rely on parallel tactic search over partially specified proofs, such as those generated by Draft-Sketch-Prove (DSP) pipelines. In current systems, each searc…
Automated Theorem ProvingAgentic Proving for Program Verification
Agentic systems have recently emerged as state-of-the-art approaches for automated theorem proving in formal mathematics. To assess how far these capabilities extend to program verification, we evaluate Claude Code in an…
Automated Theorem ProvingCode GenerationRethinking Supervision Granularity: Segment-Level Learning for LLM-Based Theorem Proving
Automated theorem proving with large language models in Lean 4 is commonly approached through either step-level tactic prediction with tree search or whole-proof generation. These two paradigms represent opposite granula…
Automated Theorem Proving