Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs

TL;DR

This paper advocates for comprehensive, error-free benchmarks with open resources in formal reasoning to enhance progress, criticizing current practices that hinder contributions and may mislead evaluations.

Contribution

It emphasizes the need for complete, open benchmarks and discusses barriers and misleading practices in formal reasoning evaluation.

Findings

Open data and benchmarks accelerate progress

Current practices create barriers to contribution

Misleading evaluation practices exist in the field

Abstract

This position paper provides a critical but constructive discussion of current practices in benchmarking and evaluative practices in the field of formal reasoning and automated theorem proving. We take the position that open code, open data, and benchmarks that are complete and error-free will accelerate progress in this field. We identify practices that create barriers to contributing to this field and suggest ways to remove them. We also discuss some of the practices that might produce misleading evaluative information. We aim to create discussions that bring together people from various groups contributing to automated theorem proving, autoformalization, and informal reasoning.