Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911963488976896 |
|---|---|
| author | Buali, Mahdi Hoehndorf, Robert |
| author_facet | Buali, Mahdi Hoehndorf, Robert |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_14521 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent Buali, Mahdi Hoehndorf, Robert Artificial Intelligence Computation and Language Symbolic Computation 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. |
| title | Towards Automated Functional Equation Proving: A Benchmark Dataset and A Domain-Specific In-Context Agent |
| topic | Artificial Intelligence Computation and Language Symbolic Computation |
| url | https://arxiv.org/abs/2407.14521 |