Language agents, which use a large language model (LLM) capable of in-context
learning to interact with an external environment, have recently emerged as a
promising approach to control tasks. We present the first language-agent
approach to formal theorem-proving. Our method, COPRA, uses a high-capacity,
black-box LLM (GPT-4) as part of a policy for a stateful backtracking search.
During the search, the policy can select proof tactics and retrieve lemmas and
definitions from an external database. Each selected tactic is executed in the
underlying proof framework, and the execution feedback is used to build the
prompt for the next policy invocation. The search also tracks selected
information from its history and uses it to reduce hallucinations and
unnecessary LLM queries.
We evaluate COPRA on the miniF2F benchmark for Lean and a set of Coq tasks
from the Compcert project. On these benchmarks, COPRA is significantly better
than one-shot invocations of GPT-4, as well as state-of-the-art models
fine-tuned on proof data, at finding correct proofs quickly.

使用大型语言模型和 COPRA 方法进行定理证明中的策略选择和反馈建议，相较于 GPT-4 和现有模型，在快速找到正确证明方面取得显著好处。

一种语言代理方法用于形式证明

A Language-Agent Approach to Formal Theorem-Proving

For artificial intelligence to be beneficial to humans the behaviour of AI
agents needs to be aligned with what humans want. In this paper we discuss some
behavioural issues for language agents, arising from accidental
misspecification by the system designer. We highlight some ways that
misspecification can occur and discuss some behavioural issues that could arise
from misspecification, including deceptive or manipulative language, and review
some approaches for avoiding these issues.

人工智能需要与人类价值观保持一致，本文研究了自然语言代理程序中存在的一些行为问题，重点讨论了系统设计者意外错误规定可能导致的一些问题，如使用欺诈或操纵性语言，以及避免这些问题的一些方法。