Papers with Code 아카이브
Automated Theorem Proving
태스크의 하위 분류와 논문·코드·평가·기법·데이터셋을 탐색하세요.
- 하위 태스크
- 0
- 평가표
- 9
- 보존된 평가 기록
- 63
The goal of Automated Theorem Proving is to automatically generate a proof, given a conjecture (the target theorem) and a knowledge base of known facts, all expressed in a formal language. Automated Theorem Proving is useful in a wide range of applications, including the verification and synthesis of software and hardware systems.
Source: Learning to Prove Theorems by Learning to Generate Theorems
논문
이 태스크와 하위 분야의 관련 논문입니다. 실제 성능 비교는 평가 결과에서 확인하세요.
Faithful Logic Embeddings in HOL -- Deep and Shallow
A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
Quantum Machine Learning in Precision Medicine and Drug Discovery -- A Game Changer for Tailored Treatments?
Activation Steering in Neural Theorem Provers
Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs
Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
Proving the Coding Interview: A Benchmark for Formally Verified Code Generation
ProofWala: Multilingual Proof Data Synthesis and Theorem-Proving
BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving
STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
LemmaHead: RAG Assisted Proof Generation Using Large Language Models
Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspective
Proof Recommendation System for the HOL4 Theorem Prover
HUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
Formal Mathematical Reasoning: A New Frontier in AI
Towards Scientific Discovery with Generative AI: Progress, Opportunities, and Challenges
WithdrarXiv: A Large-Scale Dataset for Retraction Study
Improving Multimodal LLMs Ability In Geometry Problem Solving, Reasoning, And Multistep Scoring
Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically
Learning Rules Explaining Interactive Theorem Proving Tactic Prediction
Beyond Autoregression: Fast LLMs via Self-Distillation Through Time
InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems
Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation
Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4
Proof Flow: Preliminary Study on Generative Flow Network Language Model Tuning for Formal Reasoning
3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes
LeanAgent: Lifelong Learning for Formal Theorem Proving
Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4
SubgoalXL: Subgoal-based Expert Learning for Theorem Proving
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
Revealed Invariant Preference
miniCTX: Neural Theorem Proving with (Long-)Contexts
Artifical intelligence and inherent mathematical difficulty
출처: Papers with Code · CC BY-SA 4.0. 아카이브 자료와 새로 수집한 논문은 별도로 관리합니다.