Papers Automated Theorem Proving
“Automated Theorem Proving” 태그가 달린 논문 330편 · 필터 해제
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 ProvingBenchmarking Testing in Automated Theorem Proving
Recent advances in large language models (LLMs) have shown promise in formal theorem proving, yet evaluating semantic correctness remains challenging. Existing evaluations rely on indirect proxies such as lexical overlap…
Automated Theorem ProvingCode GenerationDiscover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4
Most ATP benchmarks embed the final answer within the formal statement -- a convention we call "Easy Mode" -- a design that simplifies the task relative to what human competitors face and may lead to optimistic estimates…
Automated Theorem ProvingMechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
Recent advances in large language models (LLMs) and LLM-based agents have substantially improved the capabilities of automated theorem proving. However, for problems requiring complex mathematical reasoning, current syst…
Automated Theorem ProvingMathematical ReasoningTaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?
Automated theorem proving (ATP) benchmarks largely consist of problems formalized in MathLib, so current ATP training and evaluation are heavily biased toward MathLib's definitional framework. However, frontier mathemati…
Automated Theorem ProvingA Minimal Agent for Automated Theorem Proving
We propose a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures. This design implements the core features shared among state-of-the-art systems: iterative p…
Automated Theorem ProvingIn Transformer We Trust? A Perspective on Transformer Architecture Failure Modes
Transformer architectures have revolutionized machine learning across a wide range of domains, from natural language processing to scientific computing. However, their growing deployment in high-stakes applications, such…
Automated Theorem ProvingDrug DiscoveryRocqSmith: Can Automatic Optimization Forge Better Proof Agents?
This work studies the applicability of automatic AI agent optimization methods to real-world agents in formal verification settings, focusing on automated theorem proving in Rocq as a representative and challenging domai…
Automated Theorem ProvingVERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
Despite the syntactic fluency of Large Language Models (LLMs), ensuring their logical correctness in high-stakes domains remains a fundamental challenge. We present a neurosymbolic framework that combines LLMs with SMT s…
Automated Theorem ProvingQuantum automated theorem proving
Automated theorem proving, or more broadly automated reasoning, aims at using computer programs to automatically prove or disprove mathematical theorems and logical statements. It takes on an essential role across a vast…
Automated Theorem ProvingGDEPO: Group Dual-dynamic and Equal-right Advantage Policy Optimization with Enhanced Training Data Utilization for Sample-Constrained Reinforcement Learning
Automated Theorem Proving (ATP) represents a fundamental challenge in Artificial Intelligence (AI), requiring the construction of machine-verifiable proofs in formal languages such as Lean to evaluate AI reasoning capabi…
Automated Theorem ProvingReinforcement LearningMSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classification
Automated Theorem Proving (ATP) represents a core research direction in artificial intelligence for achieving formal reasoning and verification, playing a significant role in advancing machine intelligence. However, curr…
Automated Theorem ProvingMathematical ReasoningGödel's Poetry
Formal, automated theorem proving has long been viewed as a challenge to artificial intelligence. We introduce here a new approach to computer theorem proving, one that employs specialized language models for Lean4 proof…
Automated Theorem ProvingGold-Medal-Level Olympiad Geometry Solving with Efficient Heuristic Auxiliary Constructions
Automated theorem proving in Euclidean geometry, particularly for International Mathematical Olympiad (IMO) level problems, remains a major challenge and an important research focus in Artificial Intelligence. In this pa…
Automated Theorem ProvingSpark-Prover-X1: Formal Theorem Proving Through Diverse Data Training
Large Language Models (LLMs) have shown significant promise in automated theorem proving, yet progress is often constrained by the scarcity of diverse and high-quality formal language data. To address this issue, we intr…
Automated Theorem Proving