“`html
Автоматизация математического рассуждения в искусственном интеллекте
Автоматизация математического рассуждения давно является целью искусственного интеллекта. Формальные фреймворки, такие как Lean 4, Isabelle и Coq, играют значительную роль в этом процессе. Они позволяют пользователям писать машинно-проверяемые доказательства математических теорем, предоставляя структурированную среду для решения сложных проблем. Разработка нейронных теоремных доказателей, направленных на автоматизацию этого процесса, требует строгих бенчмарков для оценки их эффективности и дальнейших исследований.
PUTNAMBENCH: новый бенчмарк для оценки нейронных теоремных доказателей
Исследователи из Университета Техаса в Остине представили PUTNAMBENCH – новый бенчмарк, разработанный для оценки нейронных теоремных доказателей с использованием задач из математического конкурса Уильяма Лоуэлла Патнэма. Этот конкурс известен в Северной Америке своими сложными задачами по математике уровня колледжа, что делает его идеальным источником для строгого бенчмарка. PUTNAMBENCH включает 1697 формализаций 640 задач, доступных в Lean 4 и Isabelle, а также значительное подмножество в Coq. Такой многоязычный подход обеспечивает всестороннюю оценку в различных средах теоремных доказательств.
Оценка PUTNAMBENCH
Оценка PUTNAMBENCH использовала несколько нейронных и символьных теоремных доказателей, включая Draft-Sketch-Prove, COPRA, GPT-4, Sledgehammer и Coqhammer. Эти методы были протестированы на 1697 формализациях, и результаты показали, что текущие методы могут решить лишь небольшую часть задач PUTNAMBENCH. Например, GPT-4 решил всего одну из 640 задач в Lean 4 и Coq, в то время как Sledgehammer решил три из 640 задач в Isabelle.
Значение PUTNAMBENCH
PUTNAMBENCH подчеркивает сложность синтеза новых лемм и оркестрации их в сложные доказательства. Это означает, что необходимы более продвинутые нейронные модели, способные использовать глубокие математические знания и рассуждения. Многоязычный характер PUTNAMBENCH отличает его от предыдущих бенчмарков, позволяя более всестороннюю оценку методов теоремных доказательств.
Выводы
PUTNAMBENCH, предоставляя разнообразный набор формализаций задач конкурса Патнэма на нескольких языках формальных доказательств, устраняет ограничения существующих бенчмарков и устанавливает новый стандарт строгости и всесторонности. Результаты текущих оценок показывают, что, несмотря на прогресс, развитие нейронных теоремных доказателей, способных решать сложные математические задач, все еще находится в начале пути. PUTNAMBENCH будет несомненно важен для дальнейших исследований и инноваций.
Источник: MarkTechPost
“`
