rrma-lean4-agent-traces

RRMA Lean 4 Agent Traces 是一个包含416条多智能体Lean 4证明搜索轨迹的数据集，专注于两个Erdős数学问题的自动定理证明。数据集涵盖了三个不同规模的Claude模型变体（claude-opus-4-8、claude-haiku-4-5、claude-sonnet-4-6）和四个逐步增加的难度等级：G2（在预构建框架中填充sorry空缺）、G1（根据自然语言构造描述构建证明）、G05（仅提供Mathlib提示，无构造描述）和G0（仅提供定理陈述，无额外提示）。具体数学问题包括Erdős #741(ii)（关于同时高效且不可分割的加性基的存在性）和Erdős #125（组合数学相关问题）。数据格式方面，每条轨迹包含以下字段：messages（严格交替的用户/助手角色对话轮次列表）、reward（二元奖励，1.0表示会话最后一次真实预言机运行得分为1.0，即Lean编译通过且无sorry）、n_oracle_runs（会话中检测到的真实预言机调用次数）、last_oracle_score（最终真实预言机得分，若从未运行则为null）、ever_scored_1（布尔值，表示是否有任何真实预言机运行得分为1.0）、model（生成轨迹的模型）、rung（难度等级）、problem（问题标识）、n_turns和n_tool_calls（会话统计）。工具调用以内联格式<tool_call>和<tool_result>表示，思考块以<thinking>标记。该数据集适用于强化学习训练、定理证明智能体评估、形式化方法研究以及多轮对话代理的监督微调等任务。奖励信号基于Lean 4和Mathlib编译器的硬验证，确保了评估的可靠性。RRMA Lean 4 Agent Traces is a dataset containing 416 multi-agent Lean 4 proof search traces, focusing on automated theorem proving for two Erdős mathematical problems. The dataset covers three different scales of Claude model variants (claude-opus-4-8, claude-haiku-4-5, claude-sonnet-4-6) and four progressively increasing difficulty levels: G2 (filling sorry gaps in pre-built frameworks), G1 (constructing proofs based on natural language construction descriptions), G05 (providing only Mathlib hints without construction descriptions), and G0 (providing only theorem statements without additional hints). Specific mathematical problems include Erdős #741(ii) (on the existence of simultaneously efficient and indecomposable additive bases) and Erdős #125 (a combinatorial mathematics-related problem). In terms of data format, each trace contains the following fields: messages (a list of strictly alternating user/assistant role dialogue turns), reward (a binary reward, where 1.0 indicates that the last real oracle run in the session scored 1.0, meaning Lean compilation passed without sorry), n_oracle_runs (the number of real oracle calls detected in the session), last_oracle_score (the final real oracle score, null if never run), ever_scored_1 (a boolean indicating whether any real oracle run scored 1.0), model (the model that generated the trace), rung (difficulty level), problem (problem identifier), n_turns and n_tool_calls (session statistics). Tool calls are represented in inline format with <tool_call> and <tool_result>, and thinking blocks are marked with <thinking>. This dataset is suitable for tasks such as reinforcement learning training, theorem proving agent evaluation, formal methods research, and supervised fine-tuning of multi-turn dialogue agents. The reward signal is based on hard verification by the Lean 4 and Mathlib compilers, ensuring reliable evaluation.

原始信息汇总

数据集概述

• 数据集名称：RRMA Lean 4 Agent Traces
• 许可证：Apache-2.0
• 标签：lean4, theorem-proving, agent-traces, rl, trl, formal-methods, rlvr

数据集内容

包含 416 条多智能体 Lean 4 证明搜索轨迹（traces），覆盖两个 Erdős 问题、三个模型等级和四个难度级别（rungs）。

问题（Problems）

• Erdős #741(ii)：关于同时具有高效性和不可分割性的加法基的存在性
• Erdős #125：相关的组合数学问题

难度阶梯（Rungs / ablation ladder）

Rung	描述
G2	在预先构建的骨架中填充 sorry 空缺
G1	根据自然语言构造描述构建证明
G05	仅提供 Mathlib 提示，无具体构造
G0	仅提供定理陈述（冷启动）

模型与轨迹分布

模型	轨迹数	Reward=1.0（最终证明成功）
claude-opus-4-8	99	44
claude-haiku-4-5	156	67
claude-sonnet-4-6	161	4

Reward=1.0 按领域/难度分布：

• erdos-125：64
• 741ii G1：36
• G0：7
• G2：5
• G05：3

数据格式

每行包含以下字段：

• messages：严格交替的 {role, content} 对话轮次列表
• reward：1.0（会话最终真实 oracle 评分为 1.0，Lean 编译通过，无 sorry），否则为 0.0
• n_oracle_runs：会话中检测到的真实 oracle 调用次数
• last_oracle_score：最终真实 oracle 评分（若从未调用则为 null）
• ever_scored_1：是否曾在任意真实 oracle 运行中获得 1.0（13 个会话曾证明但后来回退）
• model：生成轨迹的模型
• rung：G0 / G05 / G1 / G2 / various
• problem：erdos-741ii 或 erdos-125
• n_turns、n_tool_calls：会话统计数据

工具调用以 <tool_call name="...">...</tool_call> / <tool_result>...</tool_result> 形式内联；思考块以 <thinking>...</thinking> 形式包含。

信号质量

• 使用 Lean 4 + Mathlib 编译器进行硬可验证奖励，无模糊评分。
• 轨迹真实捕捉了编辑→编译→诊断→修复的循环过程。
• 已知局限：部分 oracle 运行发生在修复共享临时目录竞态条件之前（智能体可能短暂误评相邻文件）；当前 reward 为会话内实时 oracle 信号，未经过独立重新验证。

版本说明（v2）

• 修正了原始上传中的两个缺陷：
  1. messages 字段从 JSON 字符串修正为数组
  2. reward 现在仅根据真实 oracle 输出（紧邻 SORRY_COUNT: / BUILD_EXIT: / STATUS: 行的 SCORE=）标记，仅当最后一次 oracle 评分为 1.0 时才设为 1.0
• 修正后正例数量：115/416（原为 336）

来源与相关数据集

• 使用 RRMA 框架生成，运行于 RTX 4070 Ti
• 相关数据集：vincentoh/erdos741ii-lean4-opus-traces（39 条 Opus G1 轨迹，应用了相同的 v2 修正）

搜集汇总

数据集介绍

构建方式

该数据集基于RRMA框架构建，旨在捕捉多智能体在Lean 4定理证明环境中的交互轨迹。数据集涵盖了416条完整的证明搜索轨迹，源自两项艾尔迪什数论问题（Erdős #741(ii)和#125），并跨越三种模型层级（Claude Opus-4-8、Haiku-4-5、Sonnet-4-6）与四个难度梯级（G0至G2）。每条轨迹记录了智能体与Lean编译器之间的用户/助手交替对话、工具调用及思维块内容，构建过程中特别修复了原始版本中奖励信号锚定错误的缺陷，确保最终奖励仅基于最后一次真实Oracle运行分数，实现了115条正向轨迹的准确标注。

特点

本数据集最大的特色在于采用硬可验证奖励机制——奖励信号源自Lean 4与Mathlib编译器的真实运行结果，而非模糊评分，从而保证了数据标注的客观性与可靠性。同时，数据集包含丰富的多维度元信息，如Oracle运行次数、最终得分、是否曾得满分及会话统计量，为研究证明搜索过程中的阶段性成功与退化提供了细粒度分析基础。此外，奖励信号修正后新增的'ever_scored_1'字段可识别13条曾成功但后因编辑而退化的轨迹，为分析模型在复杂推理中的稳定性提供了宝贵视角。

使用方法

用户可通过HuggingFace的datasets库便捷加载该数据集，利用Python代码中的load_dataset函数获取训练集。为针对不同研究目标进行筛选，可基于'reward'字段提取最终获证的正向样例，或通过'ever_scored_1'字段获取所有曾成功证明的会话（包含后续退化的13条）。研究人员亦可按模型类型（如claude-opus-4-8）与难度梯级（如G1）进行组合筛选，从而定向分析特定模型与特定任务难度下的证明行为模式，服务于定理证明智能体的训练与评估研究。

背景与挑战

背景概述

该数据集名为RRMA Lean 4 Agent Traces，由研究团队于2025年创建，旨在系统记录多智能体在Lean 4定理证明中的搜索轨迹。核心研究问题聚焦于利用强化学习与形式化方法，探索智能体在组合数学问题（如Erdős #741(ii)和#125）上的自动化证明能力。数据集覆盖四种难度层级（G0至G2）与三个模型层级（Claude Opus、Haiku、Sonnet），共416条轨迹，其中115条成功达成最终证明。其贡献在于提供了可复现的、带硬性验证信号（Lean编译器）的智能体交互日志，对定理证明自动化与机器学习形式推理领域具有重要影响。

当前挑战

数据集面临的挑战包括：1）领域问题层面，自动化定理证明需应对复杂数学构造的稀疏性，如Erdős问题中同时满足高效性与不可分解性的加法基的存在性，传统搜索算法在此类结构中易陷入局部最优；2）构建过程中，原始标签因解析逻辑缺陷导致169条会话从未调用验证器、119条未达满分，且13条达到满分后发生回归，需通过行锚定SCORE信号与全会话重标签矫正；此外，编译验证器存在共享临时目录竞态条件，部分轨迹可能误标，需后续隔离重验证以提升标签可靠性。

常用场景

经典使用场景

在人工智能辅助定理证明领域，rrma-lean4-agent-traces数据集为研究者提供了多智能体在Lean 4环境中进行证明搜索的完整轨迹。该数据集涵盖了416条交互轨迹，跨越两个Erdős数论与组合学问题、四种抽象难度阶梯（G0至G2）以及三个Claude模型层级。经典使用场景聚焦于利用这些结构化的用户-助手对话序列与工具调用记录，训练或微调语言模型以执行定理证明中的关键步骤，包括补全证明空缺、理解自然语言构造描述并转化为形式化证明，乃至仅依据定理陈述进行独立探索。数据集的奖励信号基于Lean 4与Mathlib编译器的硬验证结果，确保每条轨迹的最终证明状态真实可靠，为强化学习环境下的证明策略优化提供了坚实基础。

实际应用

在实际应用中，该数据集可广泛服务于自动化数学证明辅助工具的构建与评估。基于这些轨迹，开发者可以训练出能够实时协助数学家填补Lean 4证明空格的智能代理，显著降低形式化验证的人力门槛。数据集覆盖的难度阶梯设计支持渐进式能力提升：从G2的填空任务到G0的冷启动证明，既适用于教学场景中培养学生的定理证明技能，也可用于工业级软件验证中复杂逻辑约束的自动推导。此外，多模型轨迹的收录使得用户能够针对特定数学问题比较不同推理引擎的表现，为集成多个证明代理的协作系统设计提供数据支撑，从而提升整体证明效率。

衍生相关工作

该数据集衍生了一系列重要的研究方向与经典工作。首先，基于其硬验证奖励机制，研究者得以构建更可靠的强化学习训练流程，如通过过滤出115条最终证明成功的轨迹（reward=1.0）与169条未执行验证器的失败轨迹，对比分析证明策略的有效性与空洞性。其次，该数据集直接支撑了RRMA框架的评估工作，并催生了诸如“vincentoh/erdos741ii-lean4-opus-traces”等子集，专注于特定模型与难度组合的深度分析。此外，数据集中观察到的13例证明后反转现象激发了对证明稳定性与记忆衰减机制的探讨，推动了在奖励信号中引入“ever_scored_1”等新指标的研究。这些后续工作共同完善了形式化定理证明中智能体行为建模的理论体系。