🧠 Lean Copilot: Новый шаг в автоматизации доказательства теорем
В мире искусственного интеллекта (AI) появился новый инструмент, который может кардинально изменить процесс доказательства теорем - Lean Copilot. Этот инструмент представляет собой совместную работу человека и языковой модели большого масштаба (LLM) для создания математических доказательств.
Традиционно, математические доказательства требуют внимательной проверки и часто выполняются вручную. Искусственный интеллект в этом процессе ранее не использовался из-за недостаточной надежности, особенно в задачах, связанных с математикой и логикой. Однако Lean Copilot изменяет это, предлагая подход, в котором LLM помогает предлагать тактику доказательства, в то время как человек может вмешаться и вносить изменения.
Основные особенности Lean Copilot:
- LLM предлагает шаги доказательства, помогает в поиске доказательств и выбирает полезные леммы из обширной математической библиотеки.
- Lean Copilot легко интегрируется в среду разработки VS Code с использованием Lean.
- Вы можете использовать встроенные модели от LeanDojo или применять свои собственные, которые работают как локально (с использованием GPU или без), так и в облаке.
Lean Copilot, распространяемый по лицензии MIT, делает LLM более доступными для пользователей Lean, что, как ожидается, приведет к созданию лучших данных для улучшения LLM в области математики.
Github: https://github.com/lean-dojo/LeanCopilot
Demo: https://leandojo.org
P.S. Интересно, что Sam Altman в одном из последних подкастов рассуждал на тему что же такое AGI, что каждый определяет его по своему и т.д. Для себя он определяет появление AGI поментом, когда AI сможет создать какое-то новое докозательство в науке.
#ai #llm #math #copilot #science #agi #sam_altman