Recycling Proof Patterns in Coq: Case Studies
Development of Interactive Theorem Provers has led to the creation of big libraries and varied infrastructures for formal proofs. However, despite (or perhaps due to) their sophistication, the re-use of libraries by non-experts or across domains is a challenge. In this paper, we provide detailed case studies and evaluate the machine-learning tool ML4PG built to interactively data-mine the electronic libraries of proofs, and to provide user guidance on the basis of proof patterns found in the existing libraries.
Code (0)
등록된 구현이 없습니다.
Tasks
BIG-bench Machine LearningSimilar Papers 제목 키워드 기반
Recycling controls membrane domains
We study the coarsening of strongly microphase separated membrane domains in the presence of recycling of material. We study the dynamics of the domain size distribution under both scale-free and size-dependent recycling…
Efficient Battery Usage in Wireless-Powered Cell-Free Systems with Self-Energy Recycling
This paper investigates wireless-powered cell-free systems, in which the users send their uplink data signal while simultaneously harvesting energy from network nodes and user terminals - including the transmitting user …
Do Not Waste Your Rollouts: Recycling Search Experience for Efficient Test-Time Scaling
Test-Time Scaling enhances the reasoning capabilities of Large Language Models by allocating additional inference compute to broaden the exploration of the solution space. However, existing search strategies typically tr…
Transfer learning-based method for automated ewaste recycling in smart cities
Sorting a huge stream of waste accurately within a short period can be done with the support of digitalization, particularly Artificial Intelligence, instead of traditional methods. The overlap of Artificial Intelligence…
Transfer LearningProof Recommendation System for the HOL4 Theorem Prover
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…
Automated Theorem ProvingRecommendation Systems