Automated Theorem Proving (ATP) faces challenges due to its complexity and
computational demands. Recent work has explored using Large Language Models
(LLMs) for ATP action selection, but these methods can be resource-intensive.
This study introduces FEAS, an agent that enhances the COPRA in-context
learning framework within Lean. FEAS refines prompt generation, response
parsing, and incorporates domain-specific heuristics for functional equations.
It introduces FunEq, a curated dataset of functional equation problems with
varying difficulty. FEAS outperforms baselines on FunEq, particularly with the
integration of domain-specific heuristics. The results demonstrate FEAS's
effectiveness in generating and formalizing high-level proof strategies into
Lean proofs, showcasing the potential of tailored approaches for specific ATP
challenges.

FEAS 是一种增强了 COPRA 上下文学习框架的智能体，通过改进提示生成、响应解析和引入领域特定的功能方程启发式算法来生成和形式化高级证明策略进而解决针对具体 ATP 挑战的问题。

实现自动化功能方程证明：基准数据集与特定领域上下文智能体

Towards Automated Functional Equation Proving: A Benchmark Dataset and A  Domain-Specific In-Context Agent

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 和现有模型，在快速找到正确证明方面取得显著好处。