Update README.md

README.md

@@ -1,26 +1,48 @@
+## [miniCTX: Neural Theorem Proving with (Long-)Contexts]()
+State-tactic model from [miniCTX: Neural Theorem Proving with
+(Long-)Contexts](). 
 
-Model from the [neural theorem proving tutorial vII](https://github.com/cmu-l3/ntptutorial-II). 
+- Base language model: `deepseek-ai/deepseek-coder-1.3b-base`
+- Data: [ntp-mathlib-instruct-st](https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-st)
 
-
-A deepseek-coder 1.3B model finetuned on [ntp-mathlib-instruct-st](https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-st).
-
-It is specifically finetuned for Lean 4 tactic prediction given proof states. See the tutorial for code and more information.
+It is specifically finetuned for Lean 4 tactic prediction given proof states. 
 
 #### Performance
 
-The model achieves 29.1% (71/244) on Lean 4 MiniF2F using the standard search setting (best-first search with beam search expansions and a beam size of 32). 
+Please see our paper.
 
+#### Example input
+```
+/- You are proving a theorem in Lean 4.
+You are given the following information:
+- The current proof state, inside [STATE]...[/STATE]
+
+Your task is to generate the next tactic in the proof.
+Put the next tactic inside [TAC]...[/TAC]
+-/
+[STATE]
+m n : ℕ
+h : Nat.Coprime m n
+⊢ Nat.gcd m n = 1
+[/STATE]
+[TAC]
+```
+
+#### Example output
+```
+rw [Nat.Coprime] at h
+[/TAC]
+```
 
 #### Citation
 
-Until an associated preprint is available, please cite the tutorial's repository:
+Please cite:
 ```
-@misc{ntptutorialII,
-  author = {Sean Welleck},
-  title = {Neural theorem proving tutorial II},
+@misc{hu2024minictx,
+  author = {Jiewen Hu and Thomas Zhu and Sean Welleck},
+  title = {miniCTX: Neural Theorem Proving with (Long-)Contexts},
   year = {2024},
-  publisher = {GitHub},
-  journal = {GitHub repository},
-  howpublished = {\url{https://github.com/cmu-l3/ntptutorial-II}},
+  eprint={},
+  archivePrefix={arXiv},
 }
 ```