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

自动定理证明（ATP）面临着复杂性和计算需求的挑战。最近的研究探索了使用大型语言模型（LLMs）进行ATP行动选择，但这些方法可能需要大量资源。本研究介绍了FEAS，这是一种增强了Lean中COPRA上下文学习框架的代理程序。FEAS改进了提示生成、响应解析，并结合了特定领域的启发式方法来解决函数方程。它引入了FunEq，这是一个经过筛选的具有不同难度的函数方程问题数据集。FEAS在FunEq上表现优异，尤其是在整合特定领域的启发式方法时。结果展示了FEAS将高层次的证明策略生成和正式化为Lean证明的有效性，展示了针对特定ATP挑战的定制方法的潜力。

本论文旨在改进自动定理证明（ATP）中的COPRA框架，提出了FEAS代理，通过优化提示生成、响应解析和引入特定领域的启发式方法来提高ATP的性能，特别是在功能方程的问题上。

FEAS代理结合了COPRA框架和特定领域的启发式方法，通过在Lean证明中生成和规范化高级证明策略来提高ATP的性能。

论文提出了FunEq数据集，用于评估功能方程问题的ATP性能。实验结果表明，FEAS代理在FunEq数据集上的表现优于基线方法，特别是在引入特定领域的启发式方法后。论文还提出了一些值得进一步研究的问题，如如何将FEAS代理应用于其他ATP问题。

最近的相关研究包括使用大型语言模型（LLMs）进行ATP的行动选择，以及使用深度学习方法进行ATP。