نسخة أولية وصول مفتوح
LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs
Mathematicians value proofs for more than correctness: among correct proofs, simplicity, purity and the computational cost of finding them vary widely. Yet LLM-powered theorem provers largely search for any correct proof, and improve its quality only after it is found. We propose LEVER, a proof search algorithm that ma …