Guiding Automated Theorem Proving with Machine Learning

Jelle Piepenbrock • Boek • paperback

• Samenvatting
  Free download at https://doi.org/10.54195/9789465150499
  
  Mathematics can be formalized to allow a computer to execute proof steps and recognize whether a statement has been proven. Computer systems that automate mathematics are called automated theorem provers (ATP). The system has inference rules, which prescribe how the axioms and conjecture may be handled during a search for a proof. The number of possible choices at each point in the process can become very large. It would be useful to have a system that can predict which choices are better than other ones, so that a proof may be reached earlier.
  
  In this thesis, automated theorem proving is combined with machine learning, a field concerned with learning patterns in data. The machine learning component, a graph neural network, is tasked with learning to predict which choices are useful and which ones are not. This information can be learned from already finished proofs. The overall goal is to improve the performance of the automated theorem proving systems in terms of theorems proven in a particular time period. It is shown that instantiation and rewriting-based proving systems can be integrated with machine learning and that the systems improve on benchmark datasets.
• Productinformatie
  Binding : Paperback
  Distributievorm : Boek (print, druk)
  Formaat : 170mm x 240mm
  Aantal pagina's : 155
  Uitgeverij : Radboud University Press
  ISBN : 9789465150499
  Datum publicatie : 03-2025
  
• Inhoudsopgave
  niet beschikbaar
• Reviews (0 uit 0 reviews)
  Wil je meer weten over hoe reviews worden verzameld? Lees onze uitleg hier.