Prefer a chat interface with context about you and your work?
Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic
The paper describes a deep reinforcement learning framework based on self-supervised learning within the proof assistant HOL4. A close interaction between the machine learning modules and the HOL4 library is achieved by the choice of tree neural networks (TNNs) as machine learning models and the internal use of HOL4 terms …