Pith. sign in

REVIEW

A Mathematical Benchmark for Inductive Theorem Provers

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2304.02986 v1 pith:5DXK6SC6 submitted 2023-04-06 cs.LO

Thibault Gauthier , Chad E. Brown , Mikolas Janota , Josef Urban This is my paper
classification cs.LO
keywords benchmarkinductivemathematicaloeisoperatorsproblemsprogramsprovers
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original abstract

We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectured by a learning-guided synthesis system using a language with looping operators. The operators implement recursion, and thus many of the proofs require induction on natural numbers. The benchmark contains problems of varying difficulty from a wide area of mathematical domains. We believe that these characteristics will make it an effective judge for the progress of inductive theorem provers in this domain for years to come.

Discussion (0). Sign in to comment.

Pith tools