Thor 让语言模型把 premise-selection 难题交给 ATP hammer，确立神经生成与符号检索分工

Thor 针对语言模型难以在大型 theorem library 中选择相关 premises 的问题，把 premise selection 委托给传统 automated theorem prover 的 hammer，其余 proof decisions 交给语言模型。论文报告 PISA success rate 从 39% 提升到 57%，且 8.2% 的问题是单独语言模型和单独 ATP 都无法解决、但组合系统能解决的。