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
논문
이 태스크와 하위 분야의 관련 논문입니다. 실제 성능 비교는 평가 결과에서 확인하세요.
Formal Specifications from Natural Language
Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesis
Autoformalization with Large Language Models
NaturalProver: Grounded Mathematical Proof Generation with Language Models
From Width-Based Model Checking to Width-Based Automated Theorem Proving
HyperTree Proof Search for Neural Theorem Proving
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers
The Isabelle ENIGMA
Logically Consistent Adversarial Attacks for Soft Theorem Provers
Adversarial Learning to Reason in an Arbitrary Logic
The Proof is in the Pudding: Using Automated Theorem Proving to Generate Cooking Recipes
Automated Reasoning in Non-classical Logics in the TPTP World
Selection Strategies for Commonsense Knowledge
From the String Landscape to the Mathematical Landscape: a Machine-Learning Outlook
Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers
Formal Mathematics Statement Curriculum Learning
Proceedings 10th International Workshop on Theorem Proving Components for Educational Software
Proceedings of the 13th International Conference on Automated Deduction in Geometry
Proving Theorems using Incremental Learning and Hindsight Experience Replay
Linear algebra with transformers
Learning Symbolic Rules for Reasoning in Quasi-Natural Language
Logically Sound Arguments for the Effectiveness of ML Safety Measures
Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof
An energy-based model for neuro-symbolic reasoning on knowledge graphs
Neural Unification for Logic Reasoning over Natural Language
Proceedings 37th International Conference on Logic Programming (Technical Communications)
Conjectures, Tests and Proofs: An Overview of Theory Exploration
AI Descartes: Combining Data and Theory for Derivable Scientific Discovery
The Horn Non-Clausal Class and its Polynomiality
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
ProoFVer: Natural Logic Theorem Proving for Fact Verification
Graph Contrastive Pre-training for Effective Theorem Reasoning
Learning Theorem Proving Components
Learning to Guide a Saturation-Based Theorem Prover
The Role of Entropy in Guiding a Connection Prover
출처: Papers with Code · CC BY-SA 4.0. 아카이브 자료와 새로 수집한 논문은 별도로 관리합니다.