datasets
Training and evaluation data, with the modality, task and licence stated up front. Listed live from the Hugging Face Hub.
crychic-dafny-acsl
CRYCHIC Dafny-to-ACSL-C Verified Translation Benchmark
This anonymized review artifact accompanies the NeurIPS 2026 Evaluations and Datasets submission:
CRYCHIC: A Universal Framework for Cross-Language Verified Code Translation.
CRYCHIC translates verified Dafny programs into C programs annotated with ACSL specifications, then checks the generated artifacts with Frama-C WP. This release contains the 1,679 fully verified Dafny/C+ACSL pairs used as the positive benchmark corpus.
The… See the full description on the dataset page: https://huggingface.co/datasets/neurips2026-crychic/crychic-dafny-acsl.ac-solver-dataset
AC-Solver Transformer Dataset
Training corpus for a decoder-only Transformer language model on the
Andrews-Curtis (AC) conjecture — one of the longest-standing open problems in
combinatorial group theory, and a challenging benchmark for reinforcement learning.
Paper: What Makes Math Problems Hard for Reinforcement Learning: A Case Study
Code: github.com/shehper/AC-Solver
Background: The Andrews-Curtis Conjecture
A balanced presentation of a group is a description… See the full description on the dataset page: https://huggingface.co/datasets/mhieuuu/ac-solver-dataset.