l3lab/ntp-mathlib-instruct-context

--- tags: - theorem-proving - math - lean configs: - config_name: default data_files: - split: train path: "with_context_mathlib_only/with_context_train*" - split: dev path: "with_context_mathlib_only/with_context_dev*" - split: test path: "with_context_mathlib_only/with_context_test*" --- ## [miniCTX: Neural Theorem Proving with (Long-)Contexts]() Lean 4 tactic prediction examples extracted from Mathlib. Examples contain: - prompt: - instruction, preceding file content, proof state - instruction, proof state - completion: tactic The file content has been truncated to 1024 tokens. ### Version Generated using `ntptoolkit`'s `ntp-training-data` and `instruction_tuning.py`. It used the following config for `ntp-training-data`: ```json { "repo": "https://github.com/leanprover-community/mathlib4", "commit": "cf8e23a62939ed7cc530fbb68e83539730f32f86", "lean": "leanprover/lean4:v4.4.0", "name": "mathlib", "import_file": "Mathlib.lean", "imports": ["Mathlib"] } ``` #### 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}, } ```--- 标签： - 定理证明（theorem-proving） - 数学（math） - Lean（Lean） 数据集配置： - 配置名称：default 数据文件： - 训练集（train）：路径为`with_context_mathlib_only/with_context_train*` - 验证集（dev）：路径为`with_context_mathlib_only/with_context_dev*` - 测试集（test）：路径为`with_context_mathlib_only/with_context_test*` --- ## [miniCTX：面向（长）上下文的神经定理证明（Neural Theorem Proving）]() 从Mathlib库中提取的Lean 4 策略预测示例。 示例包含以下内容： - 提示词（prompt）： - 指令、前置文件内容、证明状态 - 指令、证明状态 - 补全项（completion）：策略 文件内容已被截断至1024个Token（Token）。 ### 版本信息 本数据集由`ntptoolkit`的`ntp-training-data`工具与`instruction_tuning.py`脚本生成。其针对`ntp-training-data`采用了如下配置： json { "repo": "https://github.com/leanprover-community/mathlib4", "commit": "cf8e23a62939ed7cc530fbb68e83539730f32f86", "lean": "leanprover/lean4:v4.4.0", "name": "mathlib", "import_file": "Mathlib.lean", "imports": ["Mathlib"] } #### 引用格式 请引用如下文献： bibtex @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}, }