🔬 LEAP: система, решившая задачи олимпиады Putnam 2025 — 9 июня 2026 г. в 04:00:01.492
🔬 LEAP: система, решившая задачи олимпиады Putnam 2025 Google опубликовала пейпер системе LEAP, направленной на автодоказательство теорем. Она позволяет языковым моделям создавать формальные, машинно проверяемые доказательства на языке Lean. В отличие от доказательства на естественном языке, которое содержит логические пробелы, формальное доказательство записывается на машинном языке и проверяется компилятором. LEAP, используя общие модели и агентный фреймворк, разбивает задачи на части и устраняет ошибки по подсказкам компилятора. Главная победа проекта — решение всех 12 задач олимпиады Putnam 2025, в то время как Gemini 3.1 Pro и специализированный прувер Goedel-Prover-V2 не решили ни одной задачи. LEAP также проверила вспомогательную часть одной из комбинаторных задач, сгенерировав более 5000 строк кода на Lean 4 и достигла среднего результата 70% на наборе IMO-LeanProofBench. 📊 LEAP формально решила все задачи олимпиады Putnam 2025, в то время как закрытая система Aristotle показала 9 из 12 решённых задач на собственных тестах.