CoolFace
Datasetpublic

Anon987281293/ProofRank-outputs

ProofRank: Evaluation Outputs Companion artifact to the NeurIPS 2026 submission "Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness". This dataset contains the complete LLM-judge outputs behind every number reported in the paper, so that all results can be recomputed without re-querying any model. It covers the ten evaluated models (GPT-5.4, Gemini-3.1-Pro, Gemini-3-Flash, GLM-5, DeepSeek-v3.2, Kimi-K2.5-Think, StepFun-3.5-Flash, Qwen3.5-397B… See the full description on the dataset page: https://huggingface.co/datasets/Anon987281293/ProofRank-outputs.

sourceHugging Facecc-by-sa-4.0updated 2mo agoView on Hugging Face
0likes254downloads
Dataset Card

ProofRank: Evaluation Outputs

Companion artifact to the NeurIPS 2026 submission "Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness".

This dataset contains the complete LLM-judge outputs behind every number reported in the paper, so that all results can be recomputed without re-querying any model. It covers the ten evaluated models (GPT-5.4, Gemini-3.1-Pro, Gemini-3-Flash, GLM-5, DeepSeek-v3.2, Kimi-K2.5-Think, StepFun-3.5-Flash, Qwen3.5-397B, Grok-4.1-Fast, and GPT-OSS-120B) on the 382 benchmark problems, across all five proof-quality metrics (conciseness, computational ease, cognitive simplicity, diversity, and adaptivity) plus the correctness verification.

The benchmark problems themselves (with the human solution summaries and requested techniques) are released separately as the ProofRank dataset.

Contents

Each configuration of this repository is one evaluation artifact:

Config(s)RowsDescription
answer_checker*, completeness_checker*~25kFinal-answer and completeness judgments (GPT-OSS-120B) for the main, diversity, adaptivity, and conciseness-prompting runs (Sec. 3.3)
verbosity_rephrase, verbosity_rephrase_2/3~6.5kRephraser outputs used for the compressibility-based conciseness metric, for the default and the two concise prompts (Sec. 3.2, 4.2)
verbosity_verifier3,425Validity judgments of the rephrasings (App. C.2)
technique_verifier4,406Judgments of whether a solution follows the requested technique (adaptivity, Sec. 3.2)
summary_diversity_clustering_main, _with_human1,183Technique clusterings of the sampled solutions, without and with the human solutions (Sec. 3.2, 4.3)
topic_classifier382Topic labels per problem
pairwise_judgments~102kPairwise computational-ease / cognitive-simplicity verdicts, per evaluation setting (Sec. 3.2)
pairwise_raw27,626The underlying raw pairwise judge files, needed to recompute the Bradley–Terry ratings from scratch
correctness_raw600GPT-5.4 reference judgments and the corresponding checker judgments on the 200 sampled solutions used to validate the correctness filter (App. B.4)
clustering_raw755Clusterings of the human solutions (and human + initial LLM solutions), used for diversity problem selection (Sec. 3.3)
correctness_labels~15kDerived per-solution correctness labels (informational; re-derived from the checker outputs during evaluation)
diversity_samples, human_solutions, all_solutions, raw_problems~17.6kThe compiled solution samples and problem/solution data files consumed by the evaluation scripts

Usage

Run the following command using the code file provided in this repository to regenerate the samples (pickled for caching, but full outputs can be restored):

python scripts/data/import_review_datasets.py --from-hub --repo-id Anon987281293/ProofRank-outputs --overwrite```

## License

This artifact is released under the [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/) license, matching the license of the submission's main data release.