태스크의 하위 분류와 논문·코드·평가·기법·데이터셋을 탐색하세요.
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
출처에 같은 태스크 이름으로 연결된 데이터셋입니다. 동명 태스크가 포함될 수 있으므로, 비교할 때는 평가 결과의 조건도 확인하세요.
MiniF2F is a dataset of formal Olympiad-level mathematics problems statements intended to provide a unified cross-system benchmark for neural theorem proving. The miniF2F benchmark currently targets Metamath, Lean, and Isabelle and consists of 488 problem statements drawn from the AIME, AMC, and the International Mathematical Olympiad (IMO), as well as material from high-school and undergraduate mathematics courses.
A new large-scale geometry problem-solving dataset - 3,002 multi-choice geometry problems - dense annotations in formal language for the diagrams and text - 27,213 annotated diagram logic forms (literals) - 6,293 annotated text logic forms (literals)
ProofNet is a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3, a natural language theorem statement, and natural language proof. The problems are primarily drawn from popular undergraduate pure mathematics textbooks and cover topics such as real and complex analysis, linear algebra, abstract algebra, and topology. Source: ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics Image Source: https://arxiv.org/pdf/2302.12433v1.pdf
MED is a new evaluation dataset that covers a wide range of monotonicity reasoning that was created by crowdsourcing and collected from linguistics publications. The dataset was constructed by collecting naturally-occurring examples by crowdsourcing and well-designed ones from linguistics publications. It consists of 5,382 examples. Source: https://github.com/verypluming/MED Image Source: https://www.aclweb.org/anthology/W19-4804v2.pdf
HolStep is a dataset based on higher-order logic (HOL) proofs, for the purpose of developing new machine learning-based theorem-proving strategies. Source: HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
This relational database consists of 24 unique names in two families (they have equivalent structures). Source: https://archive.ics.uci.edu/ml/datasets/kinship
The official HOList benchmark for automated theorem proving consists of all theorem statements in the core, complex, and flyspeck corpora. The goal of the benchmark is to prove as many theorems as possible in the HOList environment in the order they appear in the database. That is, only theorems that occur before the current theorem are supposed to be used as premises (lemmata) in its proof. Source: HoList Image Source: https://sites.google.com/view/holist/home
GamePad that can be used to explore the application of machine learning methods to theorem proving in the Coq proof assistant. Source: GamePad: A Learning Environment for Theorem Proving
출처: Papers with Code · CC BY-SA 4.0. 아카이브 자료와 새로 수집한 논문은 별도로 관리합니다.