Proof Recommendation System for the HOL4 Theorem Prover
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866929668591976448 |
|---|---|
| author | Dekhil, Nour Rashid, Adnan Tahar, Sofiene |
| author_facet | Dekhil, Nour Rashid, Adnan Tahar, Sofiene |
| contents | We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns from extensive libraries of HOL4 containing proofs of theorems. Consequently, it can accurately predict the next tactic(s) (proof step(s)) based on the history of previously employed tactics. The tool operates by reading a given sequence of tactics already used in a proof process (in our case, it contains at least three tactics), referred to as the current proof state, and provides recommendations for the next optimal proof step(s). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_05463 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Proof Recommendation System for the HOL4 Theorem Prover Dekhil, Nour Rashid, Adnan Tahar, Sofiene Logic in Computer Science Artificial Intelligence We introduce a proof recommender system for the HOL4 theorem prover. Our tool is built upon a transformer-based model [2] designed specifically to provide proof assistance in HOL4. The model is trained to discern theorem proving patterns from extensive libraries of HOL4 containing proofs of theorems. Consequently, it can accurately predict the next tactic(s) (proof step(s)) based on the history of previously employed tactics. The tool operates by reading a given sequence of tactics already used in a proof process (in our case, it contains at least three tactics), referred to as the current proof state, and provides recommendations for the next optimal proof step(s). |
| title | Proof Recommendation System for the HOL4 Theorem Prover |
| topic | Logic in Computer Science Artificial Intelligence |
| url | https://arxiv.org/abs/2501.05463 |