English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In learning-assisted theorem proving, one of the most critical challenges isto generalize to theorems unlike those seen at training time. In this paper, weintroduce INT, an INequality Theorem proving benchmark, specifically designedto test agents' generalization ability. INT is based on a procedure forgenerating theorems and proofs; this procedure's knobs allow us to measure 6different types of generalization, each reflecting a distinct challengecharacteristic to automated theorem proving. In addition, unlike priorbenchmarks for learning-assisted theorem proving, INT provides a lightweightand user-friendly theorem proving environment with fast simulations, conduciveto performing learning-based and search-based research. We introducelearning-based baselines and evaluate them across 6 dimensions ofgeneralization with the benchmark. We then evaluate the same agents augmentedwith Monte Carlo Tree Search (MCTS) at test time, and show that MCTS can helpto prove new theorems.

INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving