Abstract:
This research proposes a framework providing proof automation for the Dynamic Fault
Tree (DFT) analysis performed in the interactive theorem prover HOL4. Empowering
both seasoned experts and novices alike, this framework uses the capabilities of deep
learning models, including a Transformer-based architecture and a Convolutional Neural
Network (CNN), to overcome the complexities associated with crafting intricate tactics
and the manual proofs developed in HOL4. By employing an innovative multi-model
approach, the system seamlessly guides users through the proof generation process, start ing from a user-provided theorem or goal. Leveraging the strengths of the Transformer
model, the system intelligently generates a preliminary tactic based on the given input.
Building upon this initial step, the system deftly constructs the entire proof, employ ing the Transformer model’s proficiency in handling lengthy sequences. The ingenious
combination of the CNN and Transformer models enables the seamless integration of
goal-directed theorem proving and automated proof synthesis. The proposed approach
marks a significant milestone in enhancing the accessibility and usability of DFT analysis
available in HOL4, revolutionizing the landscape of formal DFT analysis. The AI-driven
approach pioneered in this work not only fosters efficiency and understanding but also
ensures an unmatched user experience within the DFT analysis community.
