Notice: This website is continuously updated as new conference proceedings and journal volumes are published. Consequently, the figures presented here may differ from those reported in our publications.
A brief overview of our methodology is provided on the Methods page, along with references to publications documenting our approach and links to the code and data used in each study.
The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates.
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving
Authors: Yuhuai Wu, Albert Jiang, Jimmy Ba, Roger Baker Grosse
ICLR 2021 | Venue PDF | LLM Run Details | Input Tokens: 33,494 Total number of tokens sent to the LLM as input for this paper's analysis. | Output Tokens: 4,676 Total number of tokens produced by the LLM (including reasoning/thinking tokens) for this paper's analysis.
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In the following experiments, we used the proofs generated by the INT generator to perform behavior cloning. We then evaluated the success rates of trained agents in a theorem proving environment. |
| Researcher Affiliation | Academia | Yuhuai Wu , Albert Qiaochu Jiang , Jimmy Ba & Roger Grosse University of Toronto & Vector Institute EMAIL |
| Pseudocode | Yes | We provide the theorem generation algorithm in Algorithm 1. |
| Open Source Code | Yes | The code for generating theorems and conducting experiments is available at https://github.com/albertqjiang/INT. |
| Open Datasets | Yes | For each theorem distribution, we ο¬rst generated a ο¬xed test set of 1000 problems, and then produced training problems in an online fashion, while making sure the training problems were different from the test ones. |
| Dataset Splits | Yes | For each experiment, we ran 2 random seeds, and picked the one with higher validation success rates for test evaluation. |
| Hardware Specification | Yes | We used one Nvidia P100 or Tesla T4 GPU with 4 CPU cores for training. |
| Software Dependencies | No | The paper mentions 'fairseq (Ott et al., 2019)', 'Pytorch Geometric (Fey and Lenssen, 2019)', and 'DGL (Wang et al., 2019)' as libraries used, but does not provide specific version numbers for these software components. |
| Experiment Setup | Yes | We used the Adam optimizer (Kingma and Ba, 2015). We searched over the learning rates {10 5, 3 10 5, 10 4, 3 10 4} in preliminary experiments and found 10 4 to be the best choice, which was used for following experiments. |