PRT-Corpus: Termination-Reasoning Sessions for Frontier LLMs at the Primitive Recursor
收藏DataCite Commons2026-05-01 更新2026-05-03 收录
下载链接：
https://dataverse.harvard.edu/citation?persistentId=doi:10.7910/DVN/WWXHPE
下载链接
链接失效反馈官方服务：
资源简介：
PRT-Corpus is a benchmark of frontier large language model behavior on nine formal-methods termination-reasoning task families, evaluated at the minimal first-order primitive recursor F(x,y,Z) -> x, F(x,y,S(n)) -> G(y,F(x,y,n)). The release covers 27 frontier models and 1,188 sessions, graded on three axes (termination, witness adequacy, rule-extracted boundary admissibility) against externally-checkable answer keys fixed by archived TTT2/CeTA termination certifications and a companion mechanized Lean 4 theorem stack. This Dataverse archive is the anonymized version prepared for NeurIPS 2026 Evaluations & Datasets Track double-blind review; the canonical de-anonymized version will be republished after acceptance.
提供机构：
Harvard Dataverse
创建时间：
2026-04-27
