Проблема неформализованных доказательств
Даже тщательно выверенные научные статьи часто содержат мелкие пробелы в доказательствах или неявные допущения. PaperFormalizer, представленный Jiyuan Tan, Vasilis Syrgkanis и Jose Blanchet, решает эту проблему, создавая пайплайн для автоматической формализации исследований. Система работает с исходным кодом LaTeX, транскрибируя статью в граф зависимостей утверждений.
Как работает Author-in-the-Loop
Ключевая особенность системы — принцип «автор в контуре» (Author-in-the-Loop). AI-агент (работающий внутри Claude Code или Codex) проверяет каждое утверждение на естественном языке, выявляя неоднозначности и ошибки. Однако, только автор знает истинный смысл своих формулировок. Поэтому система не принимает решения автоматически, а предлагает варианты исправления, которые автор может принять, отклонить или переопределить.
Технические детали и интеграция
Процесс формализации включает:
- Аудит утверждений на верность, неоднозначность и корректность.
- Формализацию и доказательство в Lean с использованием Mathlib, доменных библиотек и личного инструментария автора.
- Генерацию аннотированной версии статьи, отчета об изменениях и Lean-кода, где каждое объявление связано с исходным утверждением.
Результаты и доступность
Система не только исправляет текущую статью, но и накапливает знания: личный инструментарий автора растет с каждой формализованной работой. Это позволяет исследователям делиться верифицированными статьями, создавая надежную базу для последующих исследований. PaperFormalizer доступен для использования, а примеры верифицированных работ публикуются в открытом доступе.
Источник: arXiv cs.AI ↗