ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics

要約

学部レベルの数学の自動形式化と形式的証明のベンチマークである ProofNet を紹介します。
ProofNet ベンチマークは 371 の例で構成され、それぞれがリーン 3 の正式な定理ステートメント、自然言語定理ステートメント、および自然言語証明で構成されています。
問題は主に、人気のある学部生の純粋数学の教科書から引き出され、実数および複素数の解析、線形代数、抽象代数、トポロジーなどのトピックをカバーしています。
私たちは、ProofNet が、自動形式化と自動定理証明の進歩を促進する挑戦的なベンチマークになることを目指しています。
インコンテキスト学習によるステートメントの自動形式化に関するベースライン結果を報告します。
さらに、2 つの新しいステートメントの自動形式化方法を紹介します: 迅速な検索と蒸留された逆翻訳です。

要約(オリジナル)

We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3, a natural language theorem statement, and a natural language proof. The problems are primarily drawn from popular undergraduate pure mathematics textbooks and cover topics such as real and complex analysis, linear algebra, abstract algebra, and topology. We intend for ProofNet to be a challenging benchmark that will drive progress in autoformalization and automatic theorem proving. We report baseline results on statement autoformalization via in-context learning. Moreover, we introduce two novel statement autoformalization methods: prompt retrieval and distilled backtranslation.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google