Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs

## Контекст Теоретическое компьютерное научное исследование (TCS) является ключевым компонентом в развитии широкого спектра компьютерных технологий. Одним из важных аспектов TCS является автоматизированное доказательство теорем (FTP), которое позволяет легко проверять различные вычислительные задачи. Однако существуют значительные проблемы в этой области, включая нехватку качественных данных и высокую стоимость их ручного создания. Эти проблемы ограничивают прогресс в развитии методов автоматической проверки математических доказательств. Мы предлагаем использовать TCS как источник строго структурированных проблем для вывода автоматических доказательств, который может быть легко масштабирован для генерации трудных задач с подтвержденными формально-историческими соответствиями. ## Метод Мы разработали фреймворк для автоматического генерирования теорем-проблем с формальными (Lean4) и информальными (Markdown) заданиями. Этот подход основывается на теоретических компьютерных науках, включая задачи типа Busy Beaver (доказательство границы жизнедеятельности Тьюринговых машин) и Mixed Boolean Arithmetic (комбинирование логических и арифметических выводов). Наша методика состоит в автоматической синтезировании проблем, которые могут быть проверены с помощью мощных теоретических методов и сравниваться с информальными описаниями задач. Это позволяет создать масштабируемую систему для генерирования доказательств с высоким уровнем сложности и строгой формальной гарантией качества. ## Результаты Мы провели исследование, используя широкий спектр теоретических задач и моделей глубокого обучения. Наши результаты показывают, что хотя модель DeepSeekProver-V2-671B демонстрирует внушительные результаты на задачах Busy Beaver (57.5% успеха), она имеет значительно меньший успех на задачах Mixed Boolean Arithmetic (только 12% успеха). Это показывает, что даже для простоты проверок, сложность генерации трудных доказательств остается высокой. Эти результаты демонстрируют значение TCS в создании новых проблем для тестирования моделей в области автоматического доказательства теорем. ## Значимость Наш подход открывает новые возможности для проверки моделей машинного обучения в сфере теоретических доказательств. Мы показали, что TCS может стать основой для создания новых вызовов в области автоматического доказательства, что может привести к новым решениям в AI, проверке логики и программной инженерии. Этот подход широко может использоваться в области развития новых методов для проверки теорем и развития теоретического компьютерного научного исследования. ## Выводы Мы усп