mlsanityData to 7 Oct 2026

INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving

arXiv 2007.02924 ↗First posted 6 Jul 2020cs.AI cs.LG cs.LOcited by 44

Not on the map. Why?

Abstract (arXiv)

In learning-assisted theorem proving, one of the most critical challenges is to generalize to theorems unlike those seen at training time. In this paper, we introduce INT, an INequality Theorem proving benchmark, specifically designed to test agents' generalization ability. INT is based on a procedure for generating theorems and proofs; this procedure's knobs allow us to measure 6 different types of generalization, each reflecting a distinct challenge characteristic to automated theorem proving. In addition, unlike prior benchmarks for learning-assisted theorem proving, INT provides a lightweight and user-friendly theorem proving environment with fast simulations, conducive to performing learning-based and search-based research. We introduce learning-based baselines and evaluate them across 6 dimensions of generalization with the benchmark. We then evaluate the same agents augmented with Monte Carlo Tree Search (MCTS) at test time, and show that MCTS can help to prove new theorems.

Key facts. Cited by 44 papers in the map (data through 7 Oct 2026). First posted on arXiv 6 Jul 2020.

Builds on

No reference list yet.

Built on by

Cited by year

Citing papers per year: 2021: 5; 2022: 10; 2023: 8; 2024: 14; 2025: 7.

44 papers.

Sort:

By area:

  1. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  2. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  3. 2022Autoformalization with Large Language Modelscited by 252
  4. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  5. 2022Exploring Length Generalization in Large Language Modelscited by 204
  6. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  7. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  8. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  9. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  10. 2023Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examplescited by 84
  11. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  12. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
32 more
  1. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  2. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
  3. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Datacited by 43
  4. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  5. 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Modelscited by 24
  6. 2023Mathematical Language Models: A Surveycited by 24
  7. 2021Subgoal Search For Complex Reasoning Taskscited by 21
  8. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  9. 2024Proving Olympiad Algebraic Inequalities without Human Demonstrationscited by 20
  10. 2025Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoningcited by 17
  11. 2023A Symbolic Framework for Evaluating Mathematical Reasoning and Generalisation with Transformerscited by 15
  12. 2022Lila: A Unified Benchmark for Mathematical Reasoningcited by 13
  13. 2022Fast and Precise: Adjusting Planning Horizon with Adaptive Subgoal Searchcited by 12
  14. 2023Mastering Symbolic Operations: Augmenting Language Models with Compiled Neural Networkscited by 12
  15. 2025A Survey on Mathematical Reasoning and Optimization with Large Language Modelscited by 12
  16. 2024Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learningcited by 11
  17. 2023Abstract Visual Reasoning: An Algebraic Approach for Solving Raven's Progressive Matricescited by 9
  18. 2024REFACTOR: Learning to Extract Theorems from Proofscited by 9
  19. 2024Writing in the Margins: Better Inference Pattern for Long Context Retrievalcited by 7
  20. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 7
  21. 2024ATG: Benchmarking Automated Theorem Generation for Generative Language Modelscited by 6
  22. 20243D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processescited by 6
  23. 2025Diverse Inference and Verification for Advanced Reasoningcited by 6
  24. 2021Generating Symbolic Reasoning Problems with Transformer GANscited by 5
  25. 2022Learning to Find Proofs and Theorems by Learning to Refine Search Strategies: The Case of Loop Invariant Synthesiscited by 5
  26. 2024Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutationcited by 3
  27. 2025Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairscited by 3
  28. 2021Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Modelscited by 2
  29. 2024BAIT: Benchmarking (Embedding) Architectures for Interactive Theorem-Provingcited by 2
  30. 2024Specification Overfitting in Artificial Intelligencecited by 2
  31. 2022Learning to Prove Trigonometric Identitiescited by 1
  32. 2024What Matters in Hierarchical Search for Combinatorial Reasoning Problems?cited by 1