ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics
원문 초록
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.
함께 살펴볼 논문
공통 태그를 근거로 연결했습니다. 실제 인용 관계나 논문의 우수성을 뜻하지 않습니다.
On Finetuning Tabular Foundation Models
How to Retrieve Examples in In-context Learning to Improve Conversational Emotion Recognition using Large Language Models?
Case-based Reasoning Augmented Large Language Model Framework for Decision Making in Realistic Safety-Critical Driving Scenarios
Vela: Scalable Embeddings with Voice Large Language Models for Multimodal Retrieval
On Automating Security Policies with Contemporary LLMs
Retrieval-Augmented Generation as Noisy In-Context Learning: A Unified Theory and Risk Bounds
토론
이 논문과 연결된 포럼 글이 아직 없습니다.