60 lines
1.3 KiB
Markdown
60 lines
1.3 KiB
Markdown
---
|
||
license: mit
|
||
---
|
||
## [miniCTX: Neural Theorem Proving with (Long-)Contexts]()
|
||
File-tuned context model from [miniCTX: Neural Theorem Proving with
|
||
(Long-)Contexts]().
|
||
|
||
- Base language model: `deepseek-ai/deepseek-coder-1.3b-base`
|
||
- Data: [ntp-mathlib-instruct-context](https://huggingface.co/datasets/l3lab/ntp-mathlib-instruct-context)
|
||
|
||
It is specifically finetuned for Lean 4 tactic prediction given proof states and optional file contexts.
|
||
|
||
#### Performance
|
||
|
||
Please see our paper.
|
||
|
||
#### Example input
|
||
```
|
||
/- You are proving a theorem in Lean 4.
|
||
You are given the following information:
|
||
- The file contents up to the current tactic, inside [CTX]...[/CTX]
|
||
- 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]
|
||
-/
|
||
[CTX]
|
||
import Mathlib.Data.Nat.Prime
|
||
|
||
theorem test_thm (m n : Nat) (h : m.Coprime n) : m.gcd n = 1 := by
|
||
|
||
[/CTX]
|
||
[STATE]
|
||
m n : ℕ
|
||
h : Nat.Coprime m n
|
||
⊢ Nat.gcd m n = 1
|
||
[/STATE]
|
||
[TAC]
|
||
```
|
||
|
||
#### Example output
|
||
```
|
||
rw [Nat.Coprime] at h
|
||
[/TAC]
|
||
```
|
||
|
||
#### Citation
|
||
|
||
Please cite:
|
||
```
|
||
@misc{hu2024minictx,
|
||
title={miniCTX: Neural Theorem Proving with (Long-)Contexts},
|
||
author={Jiewen Hu and Thomas Zhu and Sean Welleck},
|
||
year={2024},
|
||
eprint={2408.03350},
|
||
archivePrefix={arXiv},
|
||
primaryClass={cs.AI},
|
||
url={https://arxiv.org/abs/2408.03350},
|
||
}
|
||
``` |