迈向自动化函数方程证明：一个基准数据集和一个领域特定的上下文智能体
人工智能
2024-07-23 v1 计算与语言
符号计算
摘要
自动定理证明（ATP）因其复杂性和计算需求而面临挑战。最近的工作探索了使用大型语言模型（LLM）进行 ATP 动作选择，但这些方法可能资源密集。本研究引入了 FEAS，一个在 Lean 中增强 COPRA 上下文学习框架的智能体。FEAS 改进了提示生成、响应解析，并整合了用于函数方程的领域特定启发式方法。它引入了 FunEq，一个包含不同难度函数方程问题的精选数据集。FEAS 在 FunEq 上优于基线，特别是在整合了领域特定启发式方法后。结果证明了 FEAS 在生成高级证明策略并将其形式化为 Lean 证明方面的有效性，展示了针对特定 ATP 挑战的定制化方法的潜力。
引用
@article{arxiv.2407.14521,
title = {Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent},
author = {Mahdi Buali and Robert Hoehndorf},
journal= {arXiv preprint arXiv:2407.14521},
year = {2024}
}
备注
11 pages