lemexp-task1-v3-eval-result-updated

该数据集包含多个配置，记录了大型语言模型在Isabelle/HOL定理证明任务上的生成结果与评估指标。核心内容涉及定理证明中的引理对象和模板生成任务，每个数据样本包括定理的基本信息（如引理名称、命令、对象、相关符号、类型和定义）以及模型在特定配置下的预测输出。评估指标涵盖基于编辑距离的匹配度、在Isabelle中的解析成功标志和完全成功标志。数据集覆盖了不同模型（如Llama-3.2-1B和DeepSeek-Coder-1.3b-base）、不同训练/评估数据规模（full/small）以及不同解码策略（greedy/beam-search）的组合实验，数据规模从2,813到18,975个样本不等。适用于研究基于大型语言模型的自动定理证明、代码生成任务的评估与比较，以及模型在形式化数学领域的性能分析。

This dataset includes multiple configurations that record the generation results and evaluation metrics of large language models on Isabelle/HOL theorem proving tasks. The core content involves lemma object and template generation tasks in theorem proving, with each data sample containing basic theorem information (such as lemma name, command, object, related symbols, types, and definitions) and model predictions under specific configurations. Evaluation metrics include Levenshtein distance-based matching scores, parsing success flags in Isabelle (isabelle_*_success), and full success flags. The dataset covers combined experiments with different models (e.g., Llama-3.2-1B and DeepSeek-Coder-1.3b-base), varying training/evaluation data scales (full/small), and different decoding strategies (greedy/beam-search), with data sizes ranging from 2,813 to 18,975 samples. It is suitable for research on automatic theorem proving based on large language models, evaluation and comparison of code generation tasks, and performance analysis of models in the field of formal mathematics.

原始信息汇总

数据集详情：lemexp-task1-v3-eval-result-updated

数据集概述

该数据集包含多个配置（config），用于评估不同模型在 Isabelle/HOL 引理（lemma）生成任务上的表现。每个配置对应一组特定的模型、微调数据、评估数据以及生成策略。

配置列表

该数据集共有 9 个配置，可分为三类：

1. 基于模板的评估

配置名称	训练集大小	数据集大小
afp-2026-template-full-1p3b__lemexp-task1-v3-template_full-deepseek-coder-1.3b-base-8lr-12epochs-normal-eos__template_afp_2026_entries	2,813 条	8.41 MB

2. 基于 Llama-3.2-1B 的评估

配置名称	训练集大小	数据集大小
model_Llama-3.2-1B_finetuned_on_lemma_object_full_eval_on_lemma_object_afp_generation_beam-search	18,975 条	41.36 MB
model_Llama-3.2-1B_finetuned_on_lemma_object_full_eval_on_lemma_object_afp_generation_greedy	18,975 条	33.92 MB
model_Llama-3.2-1B_finetuned_on_lemma_object_full_eval_on_lemma_object_small_generation_beam-search	4,740 条	11.07 MB
model_Llama-3.2-1B_finetuned_on_lemma_object_full_eval_on_lemma_object_small_generation_greedy	4,740 条	9.05 MB

3. 基于 DeepSeek-Coder-1.3B 的评估

配置名称	训练集大小	数据集大小
model_deepseek-coder-1.3b-base_finetuned_on_lemma_object_small_eval_on_lemma_object_afp_generation_greedy	18,975 条	34.03 MB
model_deepseek-coder-1.3b-base_finetuned_on_lemma_object_small_eval_on_lemma_object_small_generation_greedy	4,740 条	9.10 MB
model_deepseek-coder-1.3b-base_finetuned_on_template_small_eval_on_template_afp_generation_greedy	18,975 条	33.61 MB
model_deepseek-coder-1.3b-base_finetuned_on_template_small_eval_on_template_small_generation_greedy	4,740 条	8.97 MB

特征字段

所有配置共享一组核心特征，但每个配置在预测和评估相关字段上有所差异。核心特征包括：

字段名	类型	描述
comparison_method	string	比较方法
theory_file	string	理论文件名
lemma_name	string	引理名称
lemma_command	string	引理命令
lemma_object	string	引理对象
template	string	模板
symbols	list of string	符号列表
types	list of string	类型列表
defs	list of string	定义列表

预测与评估字段（因配置而异）

常见字段包括：

• 预测字段：template_predictions_greedy、lemma_object_predictions_greedy、lemma_object_predictions_beam-search
• Levenshtein 分数：template_levenshtein_scores_greedy、lemma_object_levenshtein_scores_beam-search
• 成功标志：template_success_greedy、lemma_object_success_beam-search
• Isabelle 匹配结果：isabelle_template_matches_greedy、isabelle_lemma_object_matches_beam-search
• 成功计数与任意成功标志：isabelle_template_success_count、isabelle_template_any_success、isabelle_template_full_success_count、isabelle_template_full_any_success

评估方式

所有配置仅包含 train 分割，没有其他分割（如 validation 或 test）。数据集用于评估模型在 greedy（贪心） 和 beam-search（束搜索） 两种生成策略下的表现，包括：

• Levenshtein 距离分数
• 预测是否成功
• 与 Isabelle 模板或引理对象的匹配程度及成功率统计

数据集大小

指标	数值
总下载大小	约 18.6 MB（各配置之和）
总数据集大小	约 183.4 MB（各配置之和）
总示例数	78,778 条（各配置之和）

搜集汇总

数据集介绍

构建方式

在定理证明的自动化评估领域，LemExp任务1的评估结果数据集汇聚了多种模型与配置下的引理生成性能数据。该数据集通过对比不同微调策略与解码方法，系统性地记录了模型在Isabelle定理证明器上的表现。构建时，研究团队选取了DeepSeek-Coder-1.3B与Llama-3.2-1B等基础模型，在引理对象（lemma object）与模板（template）两种预测目标上进行了微调，并分别采用贪心搜索（greedy）与束搜索（beam-search）两种解码策略进行生生成。每个配置下的预测结果、编辑距离得分、语法匹配状态及形式化验证成功情况均被详细记录，形成了涵盖多个子集的结构化评估数据。

特点

该数据集的核心特点在于其多维度的评估指标与细粒度的成功判定机制。除了基础的预测字符串与编辑距离评分外，每一项预测均通过Isabelle验证器进行语法匹配和完整证明的逐条检查，从而区分部分成功与完全成功。此外，数据集中包含了丰富的元信息，如理论文件来源、引理名称、符号表、类型定义与上下文定义，使得评估结果可追溯至具体的数学环境。不同子集覆盖了从少量样例（small）到全部AFP条目（afp）的多种测试规模，为分析模型在不同复杂度任务上的泛化能力提供了可靠数据基础。

使用方法

使用本数据集时，研究者可通过Hugging Face Datasets库加载指定配置，每个配置对应一组特定的模型、微调数据与解码策略组合。数据集以训练集（train）形式提供，包含从模型输入到输出验证的全链路字段。用户可借助'isabelle_*_success'系列布尔型字段快速筛选成功案例，或通过'*_levenshtein_scores'字段评估预测质量。该数据集适用于对比不同模型架构、微调策略与解码算法在形式化数学引理生成任务上的效能，也支持对Isabelle语法匹配与完整证明成功率的深入统计分析。

背景与挑战

背景概述

该数据集创建于人工智能辅助定理证明领域蓬勃发展的时期，其核心致力于解决形式化定理证明中引理自动生成的评估难题。由LemExp项目组主导，基于Isabelle证明助手和Archive of Formal Proofs (AFP)构建，汇集了多种模型（如DeepSeek-Coder、Llama）在不同配置下的引理生成结果与验证反馈。通过系统化记录模型预测、编辑距离、Isabelle验证状态等指标，该数据集为评估大语言模型在数学形式化推理中的表现提供了基准，推动了定理证明自动化进程。

当前挑战

该数据集面临的主要挑战在于形式化定理证明本身的高复杂性，即如何精准生成符合Isabelle语法与语义的正确引理，模型常因符号定义或类型约束的微小偏差而失败。构建过程中遭遇的多重困难包括：不同模型架构（如Llama与DeepSeek-Coder）间的评估一致性难以保证；贪婪搜索与束搜索策略产生的异构结果增加了比较难度；大规模数据集（超2.8万样本）的清洗与标准化处理，以及对模板与引理对象双任务输出的协同验证均构成显著技术壁垒。

常用场景

经典使用场景

该数据集的核心用途在于评估与比较不同深度学习模型在Isabelle定理证明环境中生成的引理（lemma）与模板（template）的质量。通过记录模型在贪婪解码（greedy）与束搜索（beam-search）策略下的预测输出，并结合Levenshtein距离与Isabelle验证框架的匹配结果，研究者能够系统性地衡量生成内容的语法正确性与语义保真度。这一场景尤其适用于检验经过微调的语言模型（如Llama-3.2-1B与deepseek-coder-1.3b-base）在形式化数学推理任务上的表现，从而推动神经符号方法在程序合成与自动证明领域的融合。

实际应用

在实际工程应用中，该数据集所评估的生成能力可被用于辅助形式化软件验证与数学库的自动扩充。例如，在Isabelle/HOL的Archive of Formal Proofs（AFP）项目中，研究者可利用微调后的模型自动产出候选引理和模板，减轻数学专家手动撰写Isar证明脚本的负担。此外，该数据集揭示的模型在完整引理与模板上的成功率差异，有助于指导开发者在编译器后端优化、高安全性系统规范生成以及基于强化学习的证明策略搜索等场景中，选择最合适的模型架构与解码参数，从而提升形式化工具的自动化程度与实用性。

衍生相关工作

围绕该数据集衍生出的经典工作包括对神经符号系统中模型泛化能力的深度剖析。例如，研究者基于其提供的多个配置（如lemma_object与template预测结果）对比了Llama-3.2-1B与deepseek-coder-1.3b-base在域内（small）与域外（afp）引理生成上的表现差异，揭示了模型在训练时所见符号分布对迁移学习的影响。此外，该数据集启发了对束搜索与贪婪解码在不同任务难度下效果权衡的定量研究，并催生了以Isabelle验证反馈作为自动化强化学习奖励信号的后续方法，进一步推动了端到端证明生成模型的迭代优化与评估标准的确立。