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
코드
관련 논문과 평가 결과에 연결된 구현입니다. 출처에서 확인된 저자 구현에는 공식 코드 표시가 있습니다.
https://github.com/Kerram/Deephol-Bert-Zpp
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
https://github.com/Kerram/holist-train
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
https://github.com/atpcurr/atpcurr
https://github.com/augustepoiroux/LeanInteract
https://github.com/cmu-l3/llmlean
Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
https://github.com/cmu-l3/ntp-toolkit
https://github.com/facebookresearch/clutrr
Measuring Systematic Generalization in Neural Proof Generation with Transformers
https://github.com/giomasce/mmpp
Holophrasm: a neural Automated Theorem Prover for higher-order logic
https://github.com/heplean/physlean
https://github.com/ibm/torchlogic
https://github.com/iv4xr-project/aplib
https://github.com/justin941208/SPIA-Project
Holophrasm: a neural Automated Theorem Prover for higher-order logic
https://github.com/lean-dojo/LeanAgent
https://github.com/lean-dojo/leaninfer
Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
https://github.com/ml4sci/symbahep
https://github.com/mluszczyk/deepsat
Automated proof synthesis for propositional logic with deep neural networks
https://github.com/rah4927/lean-dojo-mew
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
https://github.com/tensorflow/deepmath/tree/master/deepmath/deephol
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
https://github.com/tensorflow/deepmath/tree/master/deepmath/holstep_baselines
HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving
https://github.com/thejohncrafter/flows
https://github.com/waylonli/match
https://github.com/wellecks/llemma_formal2formal
https://github.com/yangky11/minif2f-lean4
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
출처: Papers with Code · CC BY-SA 4.0. 아카이브 자료와 새로 수집한 논문은 별도로 관리합니다.