vector-behavior-data

该数据集是“vector_behavior”研究的配套数据包，包含99,552个Mathlib定理的四种嵌入向量空间（均以float32存储），以及证明依赖图子集和实验结果文件。四个嵌入空间分别来自e5-mistral-7b-instruct（维度4096）、e5-large-v2（维度1024，两种文本来源）、deepseek-prover（维度4096，但为退化嵌入，仅用于对比）。数据按池顺序排列，便于直接索引。依赖图包含55,575个定理之间的证明依赖关系。数据集适用于定理嵌入行为分析、特征提取、模型对比等任务，尤其适合研究数学定理的向量表示和依赖结构。This dataset is the accompanying data package for the vector_behavior study, containing 99,552 Mathlib theorems with four embedding vector spaces (all stored as float32), as well as a subset of the proof dependency graph and experimental result files. The four embedding spaces come from e5-mistral-7b-instruct (dimension 4096), e5-large-v2 (dimension 1024, with two text sources), and deepseek-prover (dimension 4096, but as degenerate embeddings for comparison only). The data is arranged in pool order for easy direct indexing. The dependency graph includes proof dependencies between 55,575 theorems. The dataset is suitable for tasks such as theorem embedding behavior analysis, feature extraction, and model comparison, especially for studying vector representations and dependency structures of mathematical theorems.

原始信息汇总

数据集概述

名称：vector_behavior — data bundle
许可证：MIT
任务类别：特征提取（feature-extraction）
标签：mathlib、lean4、定理嵌入（theorem-embeddings）

---

内容简介

该数据集是论文/项目 vector_behavior- 的配套数据，包含 99,552 条 Mathlib 定理的四种定理嵌入空间（以 float32 存储，按池顺序排列），以及证明依赖图等辅助文件，用于定理证明行为研究。

---

数据构成

目录	嵌入空间	维度	大小
embeddings_mistral/	e5_mistral（基于 intfloat/e5-mistral-7b-instruct）	4096	1.6 GB
embeddings_corpus/	e5_large（基于 intfloat/e5-large-v2）	1024	407 MB
embeddings_fixed/	e5_large_stmt（同一模型，不同文本来源）	1024	407 MB
embeddings_deepseek/	deepseek_prover（退化，仅作对照）	4096	1.6 GB
results_shared/	pool.json、subset.json、neighbors.npz	—	27 MB
graph_uses.json.gz	证明依赖图（含 55,575 个定理）	—	2.4 MB

---

关键说明

• 行顺序：所有嵌入的行按池顺序排列，因此 pool["rows"][space] 为恒等映射；数组行数（99,552）少于原始数据（180,907 / 104,050 行），无需修改脚本。
• 数值格式：全部为 float32；使用 float16 会导致数值变化。
• 退化空间：deepseek_prover 为退化嵌入（81% 的方差集中在一个方向，且在 fp16 下提取），研究中仅作为对照，不作为证据。
• 验证保留：证明过程和依赖图作为验证集被保留，graph_uses.json.gz 仅供第三阶段重跑使用，不作为编码器输入。

---

使用方式（示例）

可通过 huggingface-cli 下载全部或部分数据（如仅下载 embeddings_corpus/、results_shared/、graph_uses.json.gz），脚本会自动适配已下载的子集进行完整流程运行。

bash huggingface-cli download davidbusbib/vector-behavior-data --repo-type dataset --local-dir vb_data --include "embeddings_corpus/" "results_shared/" "graph_uses.json.gz" "to_additive.json"

---

相关资源

• 项目代码仓库：https://github.com/david-busbib/vector_behavior-
• 数据集页面：https://huggingface.co/datasets/davidbusbib/vector-behavior-data

搜集汇总

数据集介绍

构建方式

该数据集构建于Mathlib定理库之上，精选99,552条定理，构建了四个定理嵌入空间，各空间由不同模型生成，如e5-mistral-7b-instruct和e5-large-v2等，维度各异，总计约4GB。数据以float32格式存储，按池化顺序排列，便于直接索引。同时，数据集包含了定理证明依赖图及辅助文件，如池化索引和子集划分，确保研究流程的复现性。

特点

数据集的核心特色在于其多模态的嵌入表示，覆盖不同模型和文本来源，为定理嵌入研究提供丰富对比。其中，deepseek_prover作为退化对照，其81%的方差集中单一方向，凸显其局限性，专用于对比分析。依赖图被刻意保留以支持第三阶段验证，而定理证明本体不予公开，确保数据集的验证严谨性。数据规模精炼，剔除冗余，每一部分均服务于特定研究目的。

使用方法

用户可通过HuggingFace CLI定向下载所需子集，脚本自动适配部分数据，灵活支持定制化实验。数据组织遵循池化顺序，简化行对应关系，无需额外调整。使用时，安装相应依赖并配置环境变量，即可直接运行配套脚本执行分析。对于研究者，该数据集支持定理嵌入评估、依赖图分析与模型性能对比，特别适用于验证阶段，但需注意deepseek_prover仅作反向参照。

背景与挑战

背景概述

定理证明是人工智能领域的核心挑战之一，其目标在于实现机器自动化的数学推理。近年来，基于神经网络的定理证明器借助大规模语料库训练，取得了显著进展。在此背景下，vector-behavior-data数据集应运而生，由David Busbib等研究人员于近期创建，旨在为Mathlib中99,552条定理提供多种嵌入表示，以支持定理证明中的语义检索与表示学习研究。该数据集整合了来自不同模型的嵌入，如e5-mistral-7b-instruct和e5-large-v2，并提供了证明依赖图，为分析定理嵌入空间的行为特性提供了基准资源。其影响力在于，为定理证明中的嵌入向量行为研究提供了统一、可复现的数据基础，推动了该领域对嵌入质量与模型泛化能力的深入理解。

当前挑战

该数据集所解决的领域问题在于，定理证明中的嵌入表示往往缺乏统一评估基准，导致不同模型间的比较困难。具体挑战包括：定理表述的复杂性和多样性使得嵌入需要捕获深层的语义与逻辑结构；不同嵌入模型在维度、来源及提取精度上的差异（如deepseek_prover在fp16下提取且存在退化性），为跨模型对比带来严峻挑战。构建过程中，数据集创建者需从Mathlib中筛选定理，处理嵌入与依赖图的整合，并确保数据的一致性与可复现性，同时限制数据规模以平衡存储与计算资源。此外，部分嵌入（如deepseek_prover）被标记为退化，仅用作对照，突显了在构建中识别并标注数据质量问题的必要性。

常用场景

经典使用场景

在数学定理证明的自动化研究领域，定理嵌入的质量与特性是衡量机器学习模型理解数学语言能力的关键。vector-behavior-data数据集为这一探索提供了坚实的实证基础，其经典使用场景在于对多个定理嵌入空间进行系统性表征与对比分析。研究者可依托该数据集，针对同一批99,552条Mathlib定理，运用各异的大型语言模型（如e5-mistral-7b-instruct与e5-large-v2）生成的向量表示，展开嵌入空间的几何结构、语义聚类及维度效能等维度的深入剖析。该数据集以其规范的池化排序与定制的浮点精度，确保了实验的可复现性，从而成为验证和优化数学定理嵌入算法不可或缺的基准资源。

解决学术问题

该数据集精准回应了数学定理自动推理中嵌入表示有效性评估的学术难题。传统上，跨模型嵌入的比较因数据划分不一而难以进行，且多数研究忽略了嵌入空间的退化现象。vector-behavior-data通过提供同一定理集合在不同模型下的嵌入结果，并附带证明依赖图，使得研究者能够量化嵌入质量如何影响下游任务，如定理相似性检索和前提选择。它揭示了某些嵌入（如deepseek_prover）可能存在退化维度，这为诊断和改善嵌入模型的表示能力提供了重要线索。其意义在于，它填补了从原始定理到嵌入向量之间系统性评估的空白，促进了更稳健、更具解释性的数学嵌入方法的研发，对提升自动定理证明器的性能具有深远影响。

衍生相关工作

围绕vector-behavior-data，学术社区已涌现出一系列衍生工作，深化了对定理嵌入行为的理解。基于其所提供的多头嵌入对比，研究人员得以开展跨模型迁移性能的评估，探索不同预训练策略对数学语义编码的影响，并衍生出专门针对数学领域的嵌入模型微调方法。数据集中的证明依赖图被广泛用于图神经网络与嵌入结合的试点研究，旨在通过结构化信息增强向量表示，催生了诸如‘图增强定理嵌入’一类的新研究方向。此外，针对其标注的退化嵌入案例，后续工作提出了多种维度压缩与修正策略，有效提升了嵌入空间的鲁棒性。这些衍生研究不仅丰富了数学机器学习的方法论宝库，也反过来推动了更高质量嵌入工具与数据集的诞生，形成了积极的学术循环。