Deep Learning Recommendations for the ACL2 Interactive Theorem Prover