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
논문
이 태스크와 하위 분야의 관련 논문입니다. 실제 성능 비교는 평가 결과에서 확인하세요.
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
Lean-STaR: Learning to Interleave Thinking and Proving
Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent
TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
Learning Formal Mathematics From Intrinsic Motivation
FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving
Scaling Synthetic Logical Reasoning Datasets with Context-Sensitive Declarative Grammars
miniCodeProps: a Minimal Benchmark for Proving Code Properties
Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
Proving Theorems Recursively
A Certified Proof Checker for Deep Neural Network Verification in Imandra
ATG: Benchmarking Automated Theorem Generation for Generative Language Models
Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
A Survey on Deep Learning for Theorem Proving
Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving
Wu's Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry
Proceedings 12th International Workshop on Theorem proving components for Educational software
Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization
Multi-Task Learning with Multi-Task Optimization
LeanReasoner: Boosting Complex Logical Reasoning with Lean
Enhancing Formal Theorem Proving: A Comprehensive Dataset for Training AI Models on Coq Code
BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Proving
Learning Guided Automated Reasoning: A Brief Survey
A Categorization of Complexity Classes for Information Retrieval and Synthesis Using Natural Logic
On the (In)feasibility of ML Backdoor Detection as an Hypothesis Testing Problem
REFACTOR: Learning to Extract Theorems from Proofs
An Empirical Study of Data Ability Boundary in LLMs' Math Reasoning
MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data
EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages
0-1 laws for pattern occurrences in phylogenetic trees and networks
Task Success is not Enough: Investigating the Use of Video-Language Models as Behavior Critics for Catching Undesirable Agent Behaviors
Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving
Graph2Tac: Online Representation Learning of Formal Math Concepts
출처: Papers with Code · CC BY-SA 4.0. 아카이브 자료와 새로 수집한 논문은 별도로 관리합니다.