Блог*

Разумеется, это работает не всегда, поэтому вторым шагом задействуется алгоритм, который пытается синтезировать нужное выражение перебором. При этом эффективность поиска повышается за счёт затравочных термов. Их получают, символически вычисляя RFS на списке некоторой фиксированной длины и заменяя конкретные константы в полученных выражениях на новые дырки.

Почему это работает? Потому что, хоть задача и сводится к синтезу выражений, вместо синтеза online алгоритма целиком метод пытается синтезировать отдельные независимые кусочки итоговой программы и при этом эксплуатирует индуктивность итоговой программы. Авторы провели сравнение своей реализации с синтезаторами программ общего назначения и обнаружили, что их метод значительно эффективнее. Из 51 задачи генерации online алгоритма их метод справился со всеми, кроме одной: вычисление kurtosis, четвёртого центрального предела. Соответствующая online программа в одном месте имела терм, слишком большой для поиска перебором.

Разумеется, у этого метода есть и ограничения.

Самое очевидное — он полагается на тот факт, что исходный алгоритм можно представить в функциональном виде. На практике это, впрочем, не является проблемой, поскольку функциональный язык со свёрткой достаточно выразителен.

Другое ограничение, чуть менее явное — метод существенным образом полагается на предположение, что очередной шаг можно вычислить, опираясь на конечное число скалярных значений, подсчитанных на предыдущих значениях, и что RFS можно представить в виде коньюкции равенств.

Ещё одно ограничение, которое авторы почему-то не упоминают в разделе "Limitations" и упоминают лишь мельком:

Ideally Opera [так авторы назвали реализацию] would check equivalence between the online and offline expressions over all possible input streams. However, since automatically checking equivalence is out of scope for existing techniques, Opera resorts to unsound equivalence checking methods based on testing and bounded verification. However, in practice, we have not come across any cases where the equivalence checker yielded an incorrect result.

Ещё авторы пишут, что их метод стремится получить точный эквивалент, в то время как для многих практических применений может быть достаточно приближённого решения. На мой взгляд, это не является серьёзным недостатком.

А вот напоследок хочется попенять сам папир. Исходники Opera авторы не выложили. Также в некоторых местах для теорем отсутствуют доказательства, за которыми авторы отсылают к "extended version of paper", но таковой в открытом доступе, судя по всему, пока не существует и не будет раньше июня. 😒

arXiv.org

From Batch to Stream: Automatic Generation of Online Algorithms

Online streaming algorithms, tailored for continuous data processing, offer substantial benefits but are often more intricate to design than their offline counterparts. This paper introduces a...

❤2🔥2

1.14K views01:40