Name: arc-cola/flc-n2l-splits
Creator: arc-cola
Published: 2026-04-15 17:12:49
License: 暂无描述

下载链接：

https://hf-mirror.com/datasets/arc-cola/flc-n2l-splits

下载链接

链接失效反馈

官方服务：

资源简介：

--- dataset_info: - config_name: rl features: - name: id dtype: int64 - name: statement dtype: string - name: lean_code dtype: string - name: compile_result struct: - name: env dtype: int64 - name: messages list: - name: data dtype: string - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: severity dtype: string - name: sorries list: - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: goal dtype: string - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: proofState dtype: int64 - name: stderr dtype: string - name: tactics list: - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: goals dtype: string - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: proofState dtype: int64 - name: tactic dtype: string - name: eval_reasons dtype: string - name: difficulty dtype: int64 - name: difficulty_rationale dtype: string - name: domain list: string - name: domain_summary dtype: string - name: source dtype: string splits: - name: train num_bytes: 27121318 num_examples: 9262 download_size: 13704073 dataset_size: 27121318 - config_name: sft features: - name: id dtype: int64 - name: statement dtype: string - name: lean_code dtype: string - name: compile_result struct: - name: env dtype: int64 - name: messages list: - name: data dtype: string - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: severity dtype: string - name: sorries list: - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: goal dtype: string - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: proofState dtype: int64 - name: stderr dtype: string - name: tactics list: - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: goals dtype: string - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: proofState dtype: int64 - name: tactic dtype: string - name: eval_reasons dtype: string - name: difficulty dtype: int64 - name: difficulty_rationale dtype: string - name: domain list: string - name: domain_summary dtype: string - name: source dtype: string splits: - name: train num_bytes: 406834421 num_examples: 138935 download_size: 204794029 dataset_size: 406834421 - config_name: test features: - name: id dtype: int64 - name: statement dtype: string - name: lean_code dtype: string - name: compile_result struct: - name: env dtype: int64 - name: messages list: - name: data dtype: string - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: severity dtype: string - name: sorries list: - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: goal dtype: string - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: proofState dtype: int64 - name: stderr dtype: string - name: tactics list: - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: goals dtype: string - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: proofState dtype: int64 - name: tactic dtype: string - name: eval_reasons dtype: string - name: difficulty dtype: int64 - name: difficulty_rationale dtype: string - name: domain list: string - name: domain_summary dtype: string - name: source dtype: string splits: - name: train num_bytes: 13557731 num_examples: 4630 download_size: 6868038 dataset_size: 13557731 - config_name: unused features: - name: id dtype: int64 - name: statement dtype: string - name: lean_code dtype: string - name: compile_result struct: - name: env dtype: int64 - name: messages list: - name: data dtype: string - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: severity dtype: string - name: sorries list: - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: goal dtype: string - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: proofState dtype: int64 - name: stderr dtype: string - name: tactics list: - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: goals dtype: string - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: proofState dtype: int64 - name: tactic dtype: string - name: eval_reasons dtype: string - name: difficulty dtype: int64 - name: difficulty_rationale dtype: string - name: domain list: string - name: domain_summary dtype: string - name: source dtype: string splits: - name: train num_bytes: 895044511 num_examples: 305660 download_size: 449962132 dataset_size: 895044511 - config_name: val features: - name: id dtype: int64 - name: statement dtype: string - name: lean_code dtype: string - name: compile_result struct: - name: env dtype: int64 - name: messages list: - name: data dtype: string - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: severity dtype: string - name: sorries list: - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: goal dtype: string - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: proofState dtype: int64 - name: stderr dtype: string - name: tactics list: - name: endPos struct: - name: column dtype: int64 - name: line dtype: int64 - name: goals dtype: string - name: pos struct: - name: column dtype: int64 - name: line dtype: int64 - name: proofState dtype: int64 - name: tactic dtype: string - name: eval_reasons dtype: string - name: difficulty dtype: int64 - name: difficulty_rationale dtype: string - name: domain list: string - name: domain_summary dtype: string - name: source dtype: string splits: - name: train num_bytes: 13557731 num_examples: 4630 download_size: 6853874 dataset_size: 13557731 configs: - config_name: rl data_files: - split: train path: rl/train-* - config_name: sft data_files: - split: train path: sft/train-* - config_name: test data_files: - split: train path: test/train-* - config_name: unused data_files: - split: train path: unused/train-* - config_name: val data_files: - split: train path: val/train-* ---

应用场景：