lemexp-task1-v2-eval-results

该数据集包含了多个配置的详细信息，每个配置都有一个唯一的名称、一系列特征以及数据集分割、下载大小和数据大小的信息。特征包括各种字符串和序列数据类型，分割包括具有字节和示例数量的训练集。该数据集似乎与定理和模板相关，不同的配置侧重于不同的方面，例如贪婪或波束搜索生成，以及是否具有定义和类型。

This dataset contains detailed information for multiple configurations. Each configuration has a unique name, a collection of features, as well as metadata regarding dataset splits, download size and data size. The features cover various string and sequence data types, while the splits include training sets with specified byte counts and example quantities. This dataset appears to be related to theorems and templates, with different configurations focusing on distinct aspects such as greedy or beam search generation, and whether definitions and types are included.

原始信息汇总

数据集概述

数据集基本信息

• 数据集名称: lemexp-task1-v2-eval-results
• 数据集地址: https://huggingface.co/datasets/yalhessi/lemexp-task1-v2-eval-results

数据集配置

数据集包含多个配置，每个配置针对不同的微调和评估场景。以下是主要配置的分类：

1. 基于lemma_object的微调和评估

• 配置名称:
  • finetuned_on_lemma_object_full_eval_on_lemma_object_afp_generation_greedy
  • finetuned_on_lemma_object_full_eval_on_lemma_object_octonions_generation_beam-search
  • finetuned_on_lemma_object_full_eval_on_lemma_object_octonions_generation_greedy
  • finetuned_on_lemma_object_full_eval_on_lemma_object_small_generation_beam-search
  • finetuned_on_lemma_object_full_eval_on_lemma_object_small_generation_greedy
  • finetuned_on_lemma_object_small_eval_on_lemma_object_afp_generation_beam-search
  • finetuned_on_lemma_object_small_eval_on_lemma_object_afp_generation_greedy
  • finetuned_on_lemma_object_small_eval_on_lemma_object_octonions_generation_beam-search
  • finetuned_on_lemma_object_small_eval_on_lemma_object_octonions_generation_greedy
  • finetuned_on_lemma_object_small_eval_on_lemma_object_small_generation_beam-search
  • finetuned_on_lemma_object_small_eval_on_lemma_object_small_generation_greedy

2. 基于lemma_object_small_nodefs的微调和评估

• 配置名称:
  • finetuned_on_lemma_object_small_nodefs_eval_on_lemma_object_afp_nodefs_generation_beam-search
  • finetuned_on_lemma_object_small_nodefs_eval_on_lemma_object_afp_nodefs_generation_greedy
  • finetuned_on_lemma_object_small_nodefs_eval_on_lemma_object_octonions_nodefs_generation_beam-search
  • finetuned_on_lemma_object_small_nodefs_eval_on_lemma_object_octonions_nodefs_generation_greedy
  • finetuned_on_lemma_object_small_nodefs_eval_on_lemma_object_small_nodefs_generation_beam-search
  • finetuned_on_lemma_object_small_nodefs_eval_on_lemma_object_small_nodefs_generation_greedy

3. 基于lemma_object_small_notypes的微调和评估

• 配置名称:
  • finetuned_on_lemma_object_small_notypes_eval_on_lemma_object_afp_notypes_generation_beam-search
  • finetuned_on_lemma_object_small_notypes_eval_on_lemma_object_afp_notypes_generation_greedy
  • finetuned_on_lemma_object_small_notypes_eval_on_lemma_object_octonions_notypes_generation_beam-search
  • finetuned_on_lemma_object_small_notypes_eval_on_lemma_object_octonions_notypes_generation_greedy
  • finetuned_on_lemma_object_small_notypes_eval_on_lemma_object_small_notypes_generation_beam-search
  • finetuned_on_lemma_object_small_notypes_eval_on_lemma_object_small_notypes_generation_greedy

4. 基于template的微调和评估

• 配置名称:
  • finetuned_on_template_full_eval_on_template_afp_generation_greedy
  • finetuned_on_template_full_eval_on_template_octonions_generation_beam-search
  • finetuned_on_template_full_eval_on_template_octonions_generation_greedy
  • finetuned_on_template_full_eval_on_template_small_generation_beam-search
  • finetuned_on_template_full_eval_on_template_small_generation_greedy

数据集特征

所有配置共享以下特征：

• theory_file: 字符串类型，理论文件名称。
• lemma_name: 字符串类型，引理名称。
• lemma_command: 字符串类型，引理命令。
• lemma_object: 字符串类型，引理对象。
• template: 字符串类型，模板。
• symbols: 字符串序列，符号。
• types: 字符串序列，类型。
• defs: 字符串序列，定义。

特定特征

• 预测相关特征:
  • lemma_object_predictions_greedy: 字符串序列，贪婪搜索的引理对象预测。
  • lemma_object_predictions_beam-search: 字符串序列，束搜索的引理对象预测。
  • template_predictions_greedy: 字符串序列，贪婪搜索的模板预测。
  • template_predictions_beam-search: 字符串序列，束搜索的模板预测。
• 评分相关特征:
  • lemma_object_levenshtein_scores_greedy: 整数类型，贪婪搜索的Levenshtein分数。
  • lemma_object_levenshtein_scores_beam-search: 整数类型，束搜索的Levenshtein分数。
  • template_levenshtein_scores_greedy: 整数类型，贪婪搜索的模板Levenshtein分数。
  • template_levenshtein_scores_beam-search: 整数类型，束搜索的模板Levenshtein分数。
• 成功标志:
  • lemma_object_success_greedy: 布尔类型，贪婪搜索的成功标志。
  • lemma_object_success_beam-search: 布尔类型，束搜索的成功标志。
  • template_success_greedy: 布尔类型，贪婪搜索的模板成功标志。
  • template_success_beam-search: 布尔类型，束搜索的模板成功标志。

数据集分割

所有配置均包含一个train分割，具体信息如下：

• 示例数量: 从350到16362不等。
• 字节大小: 从342718到61778904不等。
• 下载大小: 从43410到5862235不等。
• 数据集大小: 从342718到61778904不等。

搜集汇总

数据集介绍

构建方式

在自动定理证明领域，lemexp-task1-v2-eval-results数据集通过多配置评估框架构建而成。该数据集整合了多种微调策略下的模型输出结果，包括beam-search和greedy解码方法，覆盖了完整定义、无类型定义以及无定义等多种理论条件。每个配置都包含理论文件、引理对象及其预测结果，通过编辑距离分数和成功标志系统评估模型性能，形成了层次化的评估体系。

特点

该数据集展现出显著的多元化特征，包含20种不同配置的实验结果，涵盖AFP、Octonions和小型理论库等多个数学领域。每个样本均包含完整的理论上下文信息，包括符号表、类型系统和定义集合。数据集特别提供了两种解码策略的并行结果，并配备精确的Levenshtein编辑距离评分，为定理证明生成任务提供了多维度的性能评估基准。不同配置间的样本量呈现合理梯度分布，从350到16362条不等，确保了评估的全面性和代表性。

使用方法

研究人员可通过加载特定配置名称访问不同实验设置下的评估结果，例如finetuned_on_lemma_object_full_eval_on_lemma_object_afp_generation_beam-search。每个配置提供完整的预测序列及其对应的编辑距离评分，支持直接进行模型输出质量分析。数据集支持对比研究，允许跨配置比较不同解码策略和理论条件对生成性能的影响。用户可基于lemma_object_success字段快速筛选成功案例，或利用levenshtein_scores进行细粒度的误差分析，为自动定理证明模型的改进提供数据支撑。

背景与挑战

背景概述

形式化数学证明自动化是定理证明领域的前沿研究方向，lemexp-task1-v2-eval-results数据集作为该领域的重要评估基准，专注于引理对象生成任务的性能验证。该数据集由形式化方法研究团队构建，通过整合Isabelle/HOL定理证明器中的理论文件与引理命令，为机器学习模型提供了结构化评估框架。其核心价值在于推动神经符号系统在数学推理中的泛化能力研究，通过多配置评估方案显著提升了自动证明系统的可解释性与可靠性。

当前挑战

该数据集主要解决形式化数学中引理生成的语义一致性挑战，要求模型在严格逻辑约束下生成符合类型理论和符号定义的表达式。构建过程中面临三重挑战：一是需要精确对齐理论文件、引理命令与对象之间的逻辑依赖关系，二是处理八元数等抽象代数结构的特殊符号系统，三是平衡beam-search与greedy解码策略在生成准确性与计算效率间的矛盾。数据标注需依赖定理证明器的严格验证机制，确保每个生成结果均满足形式化正确性标准。

常用场景

经典使用场景

在自动定理证明领域，该数据集通过评估不同配置下引理对象的生成效果，为形式化数学的自动化推理提供基准测试平台。其经典使用场景聚焦于比较贪婪搜索与束搜索策略在引理生成任务中的性能差异，通过编辑距离评分和成功率的量化指标，系统评估生成结果与标准引理对象的匹配程度。

解决学术问题

该数据集有效解决了形式化数学中引理自动生成的评估难题，为定理证明系统的性能量化提供标准化方案。通过引入多维度评估指标，它不仅克服了传统方法中生成结果难以客观衡量的局限，还推动了神经网络与符号推理相结合的研究范式，对提升自动推理系统的可靠性和可解释性具有重要学术价值。

衍生相关工作

该数据集衍生了多项基于神经符号计算的经典研究工作，特别是在结合Transformer模型与形式化方法的交叉领域。相关成果推动了神经定理证明器的发展，激发了诸如基于注意力的引理预测架构、多模态数学推理模型等创新方向，为自动化推理社区提供了持续的研究动力和基准参照体系。