Исследователи представили CircuitProver — агентную систему на базе Lean 4, предназначенную для автоматизированного доказательства теорем при проектировании микросхем. Система использует специализированные стратегии поиска для верификации аппаратных спецификаций, значительно повышая эффективность формальной проверки сложных логических схем по сравнению с традиционными методами, требующими ручного участия инженеров на каждом этапе доказательства.
Формальная верификация остается «узким местом» в разработке полупроводников из-за высокой трудоемкости написания доказательств. CircuitProver автоматизирует этот процесс, интегрируя языковые модели с интерактивным средством доказательства Lean 4. Агент способен самостоятельно генерировать тактики доказательства, анализировать ошибки компиляции и итеративно корректировать логические выводы, что позволяет верифицировать аппаратные блоки без необходимости глубокого погружения разработчика в синтаксис формальных языков.
Применение подобных систем в EDA-инструментах (Electronic Design Automation) открывает путь к созданию более надежных чипов с меньшим количеством багов. Автоматизация доказательств сокращает время цикла проектирования и позволяет проводить верификацию на более ранних стадиях, что критически важно для архитектур с высокой плотностью транзисторов, где ошибки в логике могут привести к многомиллионным убыткам при производстве.
Ключевые факты
- CircuitProver использует Lean 4 в качестве базового движка для формальной верификации аппаратных спецификаций.
- Агентная архитектура позволяет системе самостоятельно исправлять ошибки в процессе доказательства теорем.
- Метод ориентирован на автоматизацию проверки корректности логических схем, заменяя ручное написание формальных спецификаций.
- Система демонстрирует способность справляться с задачами верификации, которые ранее требовали значительных временных затрат квалифицированных инженеров-верификаторов.