Sep, 2023
Lyra:自动定理证明中的双重纠正策略
Lyra: Orchestrating Dual Correction in Automated Theorem Proving
TL;DR利用Lyra框架,引入Tool Correction和Conjecture Correction机制,以提高Large Language Models在形式证明领域中的效果,其中Tool Correction用于减轻幻觉,并改善证明的准确性,而Conjecture Correction用于通过与证明器的交互来细化形式证明中的猜想,并通过与环境的互动进行子目标调整。