axiom-cegis

This content is not available in your language yet.

Рабочий CEGIS-цикл. Синтезатор начинает с набора примеров, предлагает самую дешёвую программу, согласованную с ними, а затем запрашивает у axiom-symbolic либо универсальное доказательство, либо контрпример. Контрпримеры добавляются в набор примеров, пока цикл не сойдётся.

Для встроенного эксперимента abs ожидаемая траектория такая:

x        -> контрпример x < 0
-x       -> контрпример x > 0
branch   -> VALID для всех целых

Связанные исследования

Этот компонент входит в исследовательский проект Axiom. Все компоненты собраны по теме localzet-axiom. Основной язык документации — русский. Исследовательские результаты и ограничения не означают готовность к промышленному применению.

Исходный код · MIT