Искусственный интеллект AxiomProver успешно решил задачи олимпиады Putnam

Стартап Axiom представил ИИ AxiomProver, способный генерировать формально верифицированные доказательства математических задач. Уникальность системы заключается в том, что каждое решение представлено в виде полного доказательства на языке Lean, который не допускает ошибок и может быть проверен автоматически.

В ходе тестирования AxiomProver продемонстрировал впечатляющие результаты в решении сложных задач. Разработали три категории задач для оценки возможностей ИИ:

• Математический анализ: Указанные задачи, кажущиеся простыми для решения человеком, требуют от ИИ огромного объема формального кода для записи доказательства в Lean.
• Комбинаторика и геометрия: AxiomProver неожиданно показал высокую эффективность в решении задач из этих областей, включая нерешенные задачи олимпиады Putnam 2024 и 2025.
• Различные подходы к решению: В некоторых задачах ИИ и люди использовали разные подходы. Например, в задаче A4 человек пришел к решению интуитивно, используя алгебру, в то время как AxiomProver применил геометрический метод.

Исследователи отмечают, что сложность математических задач для ИИ и для человека различна. У людей присутствует интуиция, в то время как у ИИ пока отсутствует способность к такому же пониманию. Теория машинной сложности, изучающая структурные особенности задач, облегчающих или затрудняющих автоматическое доказательство, является перспективным направлением исследований.