כתבה
arXiv cs.AI ·
LEVER: חיפוש הוכחות אדפטיבי
LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs
LEVER הוא אלגוריתם חיפוש הוכחות שמאפשר התאמה של מטרות ואופטימיזציה של עלות חישובית. הוא משפר את איכות ההוכחות ומקטין את עלות החישוב. LEVER נבדק על PutnamBench ב-Lean 4 והראה שיפורים משמעותיים.
תקציר מקורי באנגליתarXiv:2610.11862v1 Announce Type: new Abstract: 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 makes the objective over correct proofs programmable and optimizes it during search. LEVER scores partial proofs over an AND/OR proof graph, combining realized objective values with predictions for open subgoals, so the objective guides search before a proof is complete. The same mechanism optimizes computational cost, proof length, topical impurity, and even their weighted combinations, while the Lean kernel enforces correctness.
קרא במקור המקורי
arxiv.org
פתח כתבה מקורית