PRT - Predicate Reasoning Test

PRT是一个用于KO7监督引擎验证拒绝中间件的公共基准测试套件，包含1,188个捕获的LLM会话，涵盖27个前沿模型，涉及九个任务家族，包括一阶原始递归终止、模式驱动方法选择、内核推理、序数完成、度量验证、候选类推理和分支现实性。

原始信息汇总

数据集概述

PRT（Predicate Reasoning Test） 是一个公开的基准测试套件，专为KO7监督引擎的验证拒绝中间件设计。该引擎对每个谓词输出四种类型裁决（T1、T3、T4、Violation），每个裁决由Lean侧的前提条件支持。PRT基准测试在涵盖1,188个捕获的LLM会话的语料库上测试该引擎，这些会话覆盖27个前沿模型、9个任务族，涉及一阶原始递归终止、模式驱动方法选择、核推理、序数补全、度量验证、候选类推理和分支现实性。

存储库布局

文件夹	内容
1.test-prompts	用于捕获会话的提示文件，每个测试族一个文件夹。
2.test-files	提示引用的支持测试文件资产。
3.lean	精选的公共Lean 4模块：答案证据固定装置、已验证的答案键行、评分使用的反例，以及PaperB定理桥审计通道。
4.TTT2-Artifacts	Schema A、Schema A新系统、Schema B和Test 01的精选TTT2/CeTA认证。
5.test-sessions	扁平化的公共测试会话文件夹，每个任务族一个文件夹。
6.extracted-data	发布的CSV语料库、模式、提取提示和归一化追溯。
7.scoring	裁决评分层：重新加载发布的CSV、公共答案键，重新计算裁决逻辑，并生成审计报告。
8.analytics	论文数据再生脚本：每个.py读取发布的CSV并生成对应的.md表。
docs	GitHub Pages登录页面，包含嵌入式JSON-LD数据集元数据。

关键组成

• 答案键：7.scoring/answer-key/中包含机器可读和人类可读的答案键，附带指向Lean模块和TTT2/CeTA认证的证据指针。
• 归一化指南：6.extracted-data/normalization/中提供每表面的方法归一化指南、方法标签表和手动审查覆盖记录。
• 可复现性：通过运行7.scoring/中的裁决评分脚本（干运行模式）和8.analytics/中的分析脚本，即可复现发布的裁决列和论文数据表。脚本仅依赖Python标准库。

支持文档

• CITATION.cff：机器可读的引用元数据。
• DATASHEET.md：发布语料库的数据表。
• DATA_STATEMENT.md：涵盖来源、覆盖范围和已知限制的数据声明。
• LICENSE：PolyForm Noncommercial 1.0.0许可证。
• CHANGELOG.md：发布历史。
• models-list.md：每个模型每个测试的会话计数。

引用与联系方式

• 引用：请使用存储库中的CITATION.cff文件。相关方法论文提交至NeurIPS数据集与基准轨道。
• 维护者：Moses Rahnama，Mina Analytics，邮箱：[e-mail]。
• 安全报告：遵循SECURITY.md中的披露流程。

搜集汇总

数据集介绍

构建方式

PRT——谓词推理测试基准套件，是专为KO7监督引擎的验证性拒绝中间件设计的公开伴随基准。该数据集基于1,188个捕获的大型语言模型会话构建，覆盖27个前沿模型，横跨九大任务族，包括一阶原始递归终止性、模式驱动方法选择、内核推理、序数补全、度量验证、候选类推理及分支真实性。每个谓词均由引擎输出四种类型判决之一（T1、T3、T4、违规），且每种判决均附带Lean侧前置条件支撑。数据集的构建通过系统化收集会话、提取CSV语料库、整合Lean答案证据资产与TTT2/CeTA认证，并辅以判决评分层与论文数值分析层，确保可复现性。

特点

该数据集的显著特征在于其层次化与可审计性。仓库结构按功能划分为九大目录，从测试提示、测试文件、Lean模块、TTT2人工制品、会话数据、提取语料，到评分与分析脚本，井然有序。每个捕获会话均附带方法归一化指南、机器可读方法标签表及人工审查覆盖账本，提供透明的归一化溯源。答案密钥以机器可读JSON与人类可读Markdown双重形式发布，并关联证据指针至Lean模块与认证人工制品。此外，数据集通过Croissant 1.0与RAI清单、数据表及数据声明文档，全面覆盖来源、覆盖范围与已知限制，彰显其科学严谨性。

使用方法

使用PRT数据集复现论文核心数字分为两步。首先，克隆仓库后运行判决评分层，通过执行各测试家族对应的Python脚本（如`add_schema_a_answer_verdict_columns.py --dry-run`）以干运行模式重新计算判决并生成JSON报告。其次，进入分析层目录，依次运行各测试家族的统计分析脚本（如`schema_a.py`）及聚合脚本（如`headline_results.py`），生成论文数字表格。所有脚本仅依赖Python标准库，并在预期行数或列偏移时明确报错。此外，可选的定理通道审计通过`theory_checks/check_paper_b_theory.py`调用Lean构建，虽不影响判决推导，但为证据链提供额外验证。

背景与挑战

背景概述

PRT（Predicate Reasoning Test）基准测试套件于2026年由Moses Rahnama及其团队在Mina Analytics机构创建，旨在系统评估前沿大型语言模型在谓词推理任务中的终止性推理能力。该数据集核心研究问题聚焦于模型在面对原始递归终止、模式驱动方法选择、核推理、序数补全、度量验证等九类复杂任务时的逻辑一致性与可靠性，涵盖27个前沿模型及1188个会话记录。PRT基准通过集成Lean定理证明器、TTT2/CeTA认证及多层验证引擎，为评估LLM的谓词推理鲁棒性提供了首个标准化、可复现的评估框架，在神经符号推理与形式验证交叉领域具有重要影响力，填补了现有基准在结构化逻辑推理验证方面的空白。

当前挑战

该数据集面临的核心挑战包括：领域问题方面，LLM在原始递归终止等谓词推理任务中普遍存在表示偏移瓶颈，导致模型输出频繁出现不可靠的违反判决（Violation），亟需建立严格的逻辑约束机制来确保推理正确性。构建过程中，团队需处理跨27个模型、9类任务的超大规模会话数据采集与标准化标注，难点在于设计统一的方法归一化指南和人工审查覆盖规则以消除响应噪声；同时需构建可验证的Lean证据链与TTT2/CeTA形式化认证，确保每个判决均可通过定理证明追溯，这对数据集的完整性、可审计性和跨任务一致性提出了极高要求。

常用场景

经典使用场景

PRT（谓词推理测试）数据集的核心经典用途在于评估前沿大语言模型在形式化谓词推理任务上的表现。该基准涵盖一阶原始递归终止性、模式驱动的方法选择、核推理、序数补全、度量验证、候选类推理及分支真实性等九类任务族，通过1,188个捕获的LLM会话对27个前沿模型进行系统性测试。KO7监督引擎为每个谓词输出四种类型化裁决之一，并由Lean侧前置条件提供形式化保证，使得该数据集成为验证LLM在结构化推理任务中可靠性的权威评估工具。

解决学术问题

PRT数据集着力解决大语言模型在谓词层级形式推理能力量化评估中缺乏标准化基准的学术困境。现有评估多聚焦于非形式化自然语言推理，鲜有研究涉及模型是否能够遵循严格的谓词逻辑约束并产出可形式化验证的结论。该数据集通过Lean定理证明器提供答案证据锚点，配合TTT2/CeTA认证机制，使得研究者能够区分模型的表面语言模仿行为与真正的结构化推理能力，为揭示前沿LLM在终止性推理中的表征转换瓶颈提供了关键的实验支撑。

衍生相关工作

PRT数据集催生了一系列围绕形式化推理验证的衍生产出，包括基于Lean定理桥的PaperB审计通道、面向不同任务族的方法规范化指南体系，以及覆盖多层的TTT2/CeTA认证构件。这些工作进一步拓展了数据集的应用边界，例如Schema A与Schema B的裁决逻辑被复用于新系统验证场景，而手工审核覆盖层的公共发布则为数据质量保证树立了可复现的方法论典范。此外，伴随论文提出的原始递归子与表征转换瓶颈分析框架，已成为后续LLM形式推理能力研究的重要理论基石。