Shadowgraph
TrendingAbout
Sign in

kaiyuy/ASTactic

Model

The ASTactic model in the paper:

1

3 commits

1 linked in READMEs

updated Jun 30, 2023

See the code

README

The ASTactic model in the paper:

Learning to Prove Theorems via Interacting with Proof Assistants
Kaiyu Yang and Jia Deng
International Conference on Machine Learning (ICML) 2019

@inproceedings{yang2019coqgym,
  title={Learning to Prove Theorems via Interacting with Proof Assistants},
  author={Yang, Kaiyu and Deng, Jia},
  booktitle={International Conference on Machine Learning (ICML)},
  year={2019}
}

Please visit https://github.com/princeton-vl/CoqGym for details.

Contributors

kaiyuy

2 commits

KY
Kaiyu Yang

1 commits

Similar repos

princeton-vl/CoqGym

A Learning Environment for Theorem Proving with the Coq proof assistant

419

l3lab/ntp-mathlib-st-deepseek-coder-1.3b

Model

State-tactic model from [miniCTX: Neural Theorem Proving with

0

kaiyuy/leandojo-lean4-retriever-byt5-small

Model

Under review, NeurIPS (Datasets and Benchmarks Track), 2023

5

kaiyuy/leandojo-lean4-tacgen-byt5-small

Model

NeurIPS (Datasets and Benchmarks Track), 2023

15

deepseek-ai/DeepSeek-Prover-V1.5-Base

Model

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and…

20

deepseek-ai/DeepSeek-Prover-V1.5-SFT

Model

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and…

14

l3lab/ntp-mathlib-context-deepseek-coder-1.3b

Model

File-tuned context model from [miniCTX: Neural Theorem Proving with

3

deepseek-ai/DeepSeek-Prover-V1.5-RL

Model

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and…

65

Linked in READMEs

princeton-vl/CoqGym

A Learning Environment for Theorem Proving with the Coq proof assistant

419

README badge

kaiyuy/ASTactic

Model

The ASTactic model in the paper:

1

3 commits

1 linked in READMEs

updated Jun 30, 2023

See the code

README

The ASTactic model in the paper:

Learning to Prove Theorems via Interacting with Proof Assistants
Kaiyu Yang and Jia Deng
International Conference on Machine Learning (ICML) 2019

@inproceedings{yang2019coqgym,
  title={Learning to Prove Theorems via Interacting with Proof Assistants},
  author={Yang, Kaiyu and Deng, Jia},
  booktitle={International Conference on Machine Learning (ICML)},
  year={2019}
}

Please visit https://github.com/princeton-vl/CoqGym for details.

Similar repos

princeton-vl/CoqGym

A Learning Environment for Theorem Proving with the Coq proof assistant

419

l3lab/ntp-mathlib-st-deepseek-coder-1.3b

Model

State-tactic model from [miniCTX: Neural Theorem Proving with

0

kaiyuy/leandojo-lean4-retriever-byt5-small

Model

Under review, NeurIPS (Datasets and Benchmarks Track), 2023

5

kaiyuy/leandojo-lean4-tacgen-byt5-small

Model

NeurIPS (Datasets and Benchmarks Track), 2023

15

deepseek-ai/DeepSeek-Prover-V1.5-Base

Model

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and…

20

deepseek-ai/DeepSeek-Prover-V1.5-SFT

Model

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and…

14

l3lab/ntp-mathlib-context-deepseek-coder-1.3b

Model

File-tuned context model from [miniCTX: Neural Theorem Proving with

3

deepseek-ai/DeepSeek-Prover-V1.5-RL

Model

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and…

65

Linked in READMEs

princeton-vl/CoqGym

A Learning Environment for Theorem Proving with the Coq proof assistant

419

README badge

Contributors

kaiyuy

2 commits

KY
Kaiyu Yang

1 commits