https://github.com/hendrycks/math
공식 코드Autoformalization in the Era of Large Language Models: A Survey
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/hkunlp/subgoal-theorem-prover
공식 코드Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving
https://github.com/ibm/ai-descartes
공식 코드AI Descartes: Combining Data and Theory for Derivable Scientific Discovery
https://github.com/ibm/neural_unification_for_logic_reasoning_over_language
공식 코드Neural Unification for Logic Reasoning over Natural Language
https://github.com/internlm/internlm-math
공식 코드Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
https://github.com/izumi-h/ccgcomp
공식 코드Logical Inferences with Comparatives and Generalized Quantifiers
https://github.com/j991222/mirb
공식 코드https://github.com/jacksun200312/ecp
공식 코드Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions
https://github.com/janicicpredrag/larus
공식 코드https://github.com/jasonrute/lean-proof-recording-public
공식 코드Proof Artifact Co-training for Theorem Proving with Language Models
https://github.com/jasonrute/lean_proof_recording
공식 코드Proof Artifact Co-training for Theorem Proving with Language Models
https://github.com/jdeschena/sdtt
공식 코드Beyond Autoregression: Fast LLMs via Self-Distillation Through Time
https://github.com/jesse-michael-han/lean-step-public
공식 코드Proof Artifact Co-training for Theorem Proving with Language Models
https://github.com/jiahao004/deeptheorem
공식 코드https://github.com/jinpz/dtv
공식 코드Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization
https://github.com/jinpz/refactor
공식 코드https://github.com/justincasher/lean-explore
공식 코드https://github.com/kfdong/STP
공식 코드STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
https://github.com/kovvalsky/LangPro
공식 코드https://github.com/krishnamrith12/proofver
공식 코드ProoFVer: Natural Logic Theorem Proving for Fact Verification
https://github.com/lean-dojo/leancopilot
공식 코드Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean
https://github.com/lean-dojo/leandojo
공식 코드LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
https://github.com/lean-dojo/leandojochatgpt
공식 코드LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
https://github.com/lean-dojo/reprover
공식 코드LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
https://github.com/leanabell-lm/leanabell-prover
공식 코드https://github.com/lenianiva/pypantograph
공식 코드https://github.com/leoprover/logic-embedding
공식 코드Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
https://github.com/liuchengwucn/fimo
공식 코드FIMO: A Challenge Formal Dataset for Automated Theorem Proving
https://github.com/liuchengwucn/safe
공식 코드https://github.com/lou1sm/fastfood
공식 코드The Proof is in the Pudding: Using Automated Theorem Proving to Generate Cooking Recipes
https://github.com/menik1126/TRIGO
공식 코드TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models
https://github.com/ml4tp/gamepad
공식 코드https://github.com/moonshotai/kimina-prover-preview
공식 코드Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
https://github.com/multimodal-art-projection/criticlean
공식 코드CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization
https://github.com/neuro-symbolic-ai/explanation_refinement
공식 코드Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving
https://github.com/njudeepengine/llm_based_atp
공식 코드LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
출처: Papers with Code · CC BY-SA 4.0. 아카이브 자료와 새로 수집한 논문은 별도로 관리합니다.