Towards Automated Proof Strategy Generalisation
The ability to automatically generalise (interactive) proofs and use such generalisations to discharge related conjectures is a very hard problem which remains unsolved. Here, we develop a notion of goal types to capture key properties of goals, which enables abstractions over the specific order and number of sub-goals arising when composing tactics. We show that the goal types form a lattice, and utilise this property in the techniques we develop to automatically generalise proof strategies in order to reuse it for proofs of related conjectures. We illustrate our approach with an example.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Deep Learning for Two-Sided Matching
We initiate the study of deep learning for the automated design of two-sided matching mechanisms. What is of most interest is to use machine learning to understand the possibility of new tradeoffs between strategy-proofn…
Deep LearningvalidVocal Bursts Valence PredictionLLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
Recent advancements in large language models (LLMs) have sparked considerable interest in automated theorem proving and a prominent line of research integrates stepwise LLM-based provers into tree search. In this paper, …
Automated Theorem ProvingSynthetic Data GenerationDifferentiable Economics for Randomized Affine Maximizer Auctions
A recent approach to automated mechanism design, differentiable economics, represents auctions by rich function approximators and optimizes their performance by gradient descent. The ideal auction architecture for differ…
Facility Reallocation on the Line
We consider a multi-stage facility reallocation problems on the real line, where a facility is being moved between time stages based on the locations reported by $n$ agents. The aim of the reallocation algorithm is to mi…
The Role of Diverse Replay for Generalisation in Reinforcement Learning
In reinforcement learning (RL), key components of many algorithms are the exploration strategy and replay buffer. These strategies regulate what environment data is collected and trained on and have been extensively stud…
Diversityreinforcement-learningReinforcement LearningReinforcement Learning (RL)