Tree Neural Networks in HOL4

TL;DR

This paper introduces an implementation of tree neural networks in HOL4, demonstrating their effectiveness in approximating functions over formulas and comparing their performance with other machine learning methods.

Contribution

The paper presents the first integration of tree neural networks into HOL4, tailored for formula-based function approximation and evaluation tasks.

Findings

Tree neural networks perform well on arithmetical expression evaluation.

They effectively estimate the truth of propositional formulas.

Comparison shows competitive performance with other predictors.

Abstract

We present an implementation of tree neural networks within the proof assistant HOL4. Their architecture makes them naturally suited for approximating functions whose domain is a set of formulas. We measure the performance of our implementation and compare it with other machine learning predictors on the tasks of evaluating arithmetical expressions and estimating the truth of propositional formulas.