下载PDF摘要：我们给出了一个在校对助手HOL4中实现树神经网络的方法。它们的体系结构使它们自然适合于以一组公式为定义域的函数的近似。我们测量了我们的实现的性能，并将它与其他机器学习预测器在计算算术表达式和估计命题公式真值的任务中进行了比较。