Shadowgraph
TrendingBuzzResearch
Chrome extension
Sign in

NJUDeepEngine/llm_based_atp

Model

LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

1

4 commits

2 linked in READMEs

updated Jun 23, 2025

See the code

README

LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

This repository contains the model used in the paper "LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation".

Model

The model is full-tuned based on Qwen2.5-Math-7B.

Usage

Please refer to GitHub page for details.

conversational
formal-mathematics
lean4
qwen2
safetensors
text-generation
theorem-proving

Similar repos

FrenzyMath/REAL-Prover

Model

1. Overview

0

bytedance-research/BFS-Prover

Model

This repository contains the latest tactic generator model checkpoint from BFS-Prover, a…

26

ByteDance-Seed/BFS-Prover-V2-7B

Model

Introduction

7

Slim205/Lean_prover_v1

Model

Lean Conjecturer

0

ByteDance-Seed/BFS-Prover-V2-32B

Model

Introduction

13

Slim205/Lean-conjecturer

Model

Lean Conjecturer

0

kaiyuy/leandojo-lean4-tacgen-byt5-small

Model

NeurIPS (Datasets and Benchmarks Track), 2023

15

purewhite42/DExplorer-8B

Model

Please refer to the 📺GitHub repo and

0

Linked in READMEs

NJUDeepEngine/llm_based_atp

Code for paper: "LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation"

4

README badge

211820252/TEMP-DoBeVi

0

README badge

NJUDeepEngine/llm_based_atp

Model

LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

1

4 commits

2 linked in READMEs

updated Jun 23, 2025

See the code

README

LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

This repository contains the model used in the paper "LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation".

Model

The model is full-tuned based on Qwen2.5-Math-7B.

Usage

Please refer to GitHub page for details.

conversational
formal-mathematics
lean4
qwen2
safetensors
text-generation
theorem-proving

Similar repos

FrenzyMath/REAL-Prover

Model

1. Overview

0

bytedance-research/BFS-Prover

Model

This repository contains the latest tactic generator model checkpoint from BFS-Prover, a…

26

ByteDance-Seed/BFS-Prover-V2-7B

Model

Introduction

7

Slim205/Lean_prover_v1

Model

Lean Conjecturer

0

ByteDance-Seed/BFS-Prover-V2-32B

Model

Introduction

13

Slim205/Lean-conjecturer

Model

Lean Conjecturer

0

kaiyuy/leandojo-lean4-tacgen-byt5-small

Model

NeurIPS (Datasets and Benchmarks Track), 2023

15

purewhite42/DExplorer-8B

Model

Please refer to the 📺GitHub repo and

0

Linked in READMEs

NJUDeepEngine/llm_based_atp

Code for paper: "LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation"

4

README badge

211820252/TEMP-DoBeVi

0

README badge