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/

Zendy Plus

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

Zendy Tools

Zendy Open

We present an in-context learning agent for formal theorem-proving inenvironments like Lean and Coq. Current state-of-the-art models for the problemare finetuned on environment-specific proof data. By contrast, our approach,called COPRA, repeatedly asks a high-capacity, general-purpose large languagemodel (GPT-4) to propose tactic applications from within a statefulbacktracking search. Proposed tactics are executed in the underlying proofenvironment. Feedback from the execution is used to build the prompt for thenext model query, along with selected information from the search history andlemmas retrieved from an external database. We evaluate our implementation ofCOPRA on the miniF2F benchmark for Lean and a set of Coq tasks from theCompCert project. On these benchmarks, COPRA significantly outperforms few-shotinvocations of GPT-4. It also compares favorably against finetuning-basedapproaches, outperforming ReProver, a state-of-the-art finetuned approach forLean, in terms of the pass@1 metric. Our code and data are available athttps://github.com/trishullab/copra.

An In-Context Learning Agent for Formal Theorem-Proving