Classical Vlad

Моему аккаунту на StackOverflow стукнуло 6 лет. Время прошло удивительно быстро. Очень много чего изменилось. Сейчас 6 лет это треть моей жизни. Помню, когда смотрел на профили ребят с годами на сайте, я думал, что они крайне опытны и преисполнились в своём познании. Сейчас я понимаю, что я далеко не такой оптыный, как представлял себе этих людей. Можно было побольше вещей за 6 лет сделать

Я не знаю щас смеяться или плакать https://web4.ai/ Представляю себе кучу условных OpenClaw, которые дают друг другу деньги за saas, чтобы разработать yet another saas и так далее. Идейно напомнило rent-a-human, где тоже агентики это не средство, а цель. В каком мире мы живём🥀

Мне почему-то хочется испачкаться в агентах и вот этом всём генеративном. Мне очень нравится об этом думать, представлять какое сказочное будущее ждёт человечество со всеми этими агентами, но я вижу что это будет что-то поумнее OpenClaw или специфичных тулзов по типу ClaudeCode. Школьные проекты по типу ассистентов а-ля Джарвиса тоже принципиально ограничены в возможностях. И дело не в самих моделях, будто уже можно сделать что-то существенно получше. Но умные люди, которые могут — работают в претрене, а с агентами в текущем состоянии люди бегают как дурак со стекляшкой и крича что аги пришёл. По этому что? По этому сделаю yet another школьную поделку

https://x.com/VladKochetovv/status/2029642927916347622 РЕПОСТИМ РАСПРОСТРАНЯЕМСЯ

Симуляция микроструктуры Часть 2: один инструмент, одна биржа, спот и фьючерс Пока что комиссии, задержки и стоимость шорта на spot margin нулевая, но поменять можно легко, проект позволяет. Ничего особо нового, разве что могу написать в чём отличие basis arbitrage и funding arbitrage. - Funding Arbitrage: гонемся за прибылью от самого фандинга, который платят лонгисты шортистам или наоборот. Фандинг кстати по умолчанию не 0, а небольшой положительный, чтобы у шортистов был стимул, собственно, шортить. Ну и иначе можно было бы взять лонг плечо и не заплатить за него ничего. Если слишком много людей шортят -> платят лонгистам - выгодно войти в лонг и захеджировать спотом, ожидая сходевич - Basis Arbitrage: торгуем разницу спота с фьючерсом. По-хорошему спот примерно равен по стоимости своему фьючесу, и чтобы это выполнялось как раз существует фандинг, но он платится раз в какой-то промежуток времени (обычно 8 часов или 1 час). То есть между ними фандинг арбитражники цену не выравнивают, для этого и нужен базис арб. Раз уж мы знаем что в конце концов равновесие это равные цены, то почему бы не ровнять это уже сейчас? Расходятся графика на второй картинке попросту по причине достижения арбитражёром его максимальной абсолютной позиции Вообще сейчас бы хорошо написать про Contango и Backwardation, но это будет позже

Проектируя подобные системы всё больше задумываюсь, что нужно углубиться в паттерны проектирования и научиться более обобщённо думать что-ли.. Я задаю много вопросов "а что если", и если моя архитектура ломается после этого вопроса или нуждается в переписывании, нарушая принцип открытости-закрытости, то архитектура плохая. Часто хорошие решения попросту не приходят. По этому сколько бы не думал - сделаю случайно. В проекте с симуляцией, например, придётся изменить некоторые важные структуры клиента и биржи чтобы добавить срочные фьючерсы или опционы Вот вроде работает, вроде даже хорошо, но оно какое-то не такое Особенно узнаю себя после таких лекций: https://www.youtube.com/watch?v=9wA5yIM3pkI

Симуляция микроструктуры Часть 1: Один инструмент, одна биржа На выходе картина простая — случайное блуждание, но в текущей версии симуляции этого и ожидал. Это лишь проверка того, что движок действительно работает и выполняет веления стратегий. Такой график — это проявление взаимодействия нескольких Pure Market Making акторов и одного тейкера, который отправляет ордер раз в постоянный интервал времени со случайной стороной ордера. Первые уровни ликвидности пропадают из ордербука после исполнения тейкера, после чего мейкеры котируют уже от нового MidPrice. В последующих симуляциях хочется заставить торговать больше акторов/стратегий на разных рынках. Например, между спотовым рынком и фьючерсным будут арбитражёры. Так же между инструментами с разными quote валютами будут треугольные арбитражи. Мейкеры будут не только PMM, но и, например, Avellaneda&Stoikov. Узнал много нового и понял, как в действительности такие системы могут работать под капотом. Из интересного: - Цена маркировки: если Index почти везде стандартно является взвешенной по объёму цене спота с других бирж, то Mark может быть медианой цены последней сделки, индекса с учётом предыдущего фандинга и 30-секундного TWAP, как у Binance; ну или SMA от суммы индекса и MidPrice, как на OKX - Ликвидации происходят именно по Mark Price. Биржа хочет избежать ситуации, когда кто-то манипулирует ценой фьючерса и триггерит чужие ликвидации. Но гарантии ликвидности на выход это не даёт — если на нужном уровне книжки пусто, позиция ликвидируется частично или по худшей цене. На такой случай у бирж есть отдельный Insurance Fund, который покрывает убытки от так называемых Bankrupt Positions. Если и он не справляется — включается Auto-Deleveraging, и позиции принудительно закрываются уже у прибыльных участников с противоположной стороны. Мне это до сих пор кажется странным и не укладывается в голову. - Приоритетность Matching Engine конкретных бирж: писал в одном из постов об этом. Пока реализовал Price-time и Price-Pro-Rata. В одном из случаев (на одном уровне) филлим в порядке очереди, во втором — филлим пропорционально объёму (тут можно пойти ещё глубже, подумав над приоритетностью ордеров разной видимости) - Если у вашей биржи заполнилась очередь на исполнение — можете разделить вашу очередь на 2: приоритетную и неприоритетную. В приоритетную очередь будут идти отмены ордеров, ReduceOnly и прочие уменьшения риска, а новые ордера — в неприоритетную. И скорее будет забиваться неприоритетная очередь, чем приоритетная, и тогда можно со спокойной совестью кидать клиенту отказ с причиной Overloaded - Для избежания FlashCrash-подобных событий на некоторых биржах есть механизм, называемый Circuit Breaker, который будет останавливать торги по инструменту, если его изменение за промежуток времени вышло за допустимый предел. Так же может останавливать торги на всём рынке или бирже. Может работать как на интервалах секунд, так и минут и целых торговых сессий Кодик: https://github.com/VladKochetov007/ExchangeSimulation

4 года

А вообще, господа, скоро будет сказ о том, как я симулировал торги на бирже с разными типами участниками Полезно? - вряд ли Интересно - да

Я постепенно разочаровываюсь в кодинг-агентах. Когда дело касается инженерных вещей хоть сколько-то значимого размера, написать самому даст куда больше понимания и уверенности в коде. Я стал забывать, что по маленьким шагам, постепенно повышая уровень абстракции можно быть сильно увереннее в отсутствии слопа и банальных багов в кодовой базе Не думаю, что буду использовать их меньше, ведь работа работается, а количество головной боли всё равно существенно меньше, чем если бы я всё писал руками. Результат в некоторых случаях не принципиально хуже, а различия в потраченном мыслетоплеве колоссальны Сложно словами вложить всё понимание бинес-логики и представления о хорошем в ассистента. К сожалению, всё ещё приходится думать😥 Думать о структурах данных, о сущностях, об их взаимодействиях и зонах ответственности Когда-то мой Claude Code обязательно заведётся и я буду делать коммиты на 2к строчек с сообщением "idk, something changed"

Lean — насколько я понял, это прям честный функциональный язык программирования, который можно использовать для математических доказательств. Он решает головную боль с верифицированием доказательства. Вы объявляете все структуры и их свойства, пишите доказательство своего утверждения формально, и если код скомпилировался — ваша теорема / лемма / etc. доказана. Например, объявление группы — это конкретная структура с полями и аксиомами. В Lean (и mathlib) это уже есть из коробки:

class Group (G : Type u) extends Mul G, One G, Inv G :=
  (mul_assoc : ∀ a b c : G, (a * b) * c = a * (b * c))
  (one_mul  : ∀ a : G, 1 * a = a)
  (mul_one  : ∀ a : G, a * 1 = a)
  (mul_left_inv : ∀ a : G, a⁻¹ * a = 1)

При этом почти всегда писать такое вручную не нужно: в mathlib уже есть готовые структуры (Semigroup, Monoid, Group, Ring, Field, и т.д.) и огромная иерархия, где все свойства автоматически подтягиваются через typeclasses. Если у типа есть [Group G], Lean знает, что у него есть нейтральный элемент, обратные, ассоциативность и может использовать это в доказательствах без явных аргументов. Проблемы Lean 3 (предыдущая версия) Основная боль 3 версии была не в логике (она корректна), а в автоматизации и тактиках. Классический пример — solve_by_elim. Эта тактика пытается закрыть цель, перебирая леммы и гипотезы из контекста с бэктрекингом. Проблема в том, что порядок перебора зависел от внутреннего состояния и структуры контекста В результате один и тот же корректный код мог: - проходить мгновенно; - внезапно падать по таймауту; - зависать при малейшем изменении окружения; Похожие вещи были и в других конструкциях: simp, repeat, комбинациях try / first, а также при разрешении метапеременных. Таймауты считались по реальному времени, из-за чего скорость машины и нагрузка влияли на результат. Это не приводило к доказательству ложных теорем, но делало валидный код хрупким, нестабильным и плохо воспроизводимым -- что для формальной математики критично. А что сейчас В Lean 4 это решили радикально: язык переписали на самом себе, ввели детерминированную модель исполнения (heartbeats вместо wall-clock time), переработали систему тактик и убрали неявную недетерминированность. В результате одинаковый код теперь либо всегда работает, либо всегда падает — независимо от машины и запуска. Дока языка Всех с наступающим или уже наступившим

сегодня наконец дописал статью про то как я делал minimodal контекст: modal.com это очень крутая серверлесс платформа для машинного обучения было очень много всего сделано - точно такой же sdk, control plane который собирает образы, переправляет запросы воркерам (делать шедулер запросов было очень интимно), воркеры которые исполняют код в изолированных песочницах и возвращают результаты на сокетах. есть и батч операции, и стриминг, и все это вроде должно работать благодаря ретраям, DLQ и circuit breaker ну и всякие удобные штуки типа секретов, вольюмов и вебпоинтов тоже поддерживаются мне прям супер понравилось порисовать архитектуру неделю и заимплементить кучу штук которые прочитал за последние пару лет читаем тут - distributedhatemachine.github.io/posts/modal не читаем тут - github.com/wtfnukee/minimodal