Відібрана як одна з 24 учасників з усього світу (рівень відбору ≈1,5%) до PAIR — селективної, повністю профінансованої 10-денної програми для студентів віком 16–21 рік, присвяченої штучному інтелекту, міркуванню та когнітивним наукам.

Вивчала теорію інформації, безпеку ШІ (змагальні атаки та криптографічні бекдори), регулювання й управління ШІ, нейронауку (предиктивну обробку інформації та свідомість), а також дизайн механізмів і моделей.

Працювала над проєктом із застосування ШІ для математичних відкриттів, досліджуючи межу Заранкевича (Zarankiewicz frontier). У межах дня Creation / хакатону створила дашборд для пріоритизації агентів Claude Code, який координує та ранжує завдання агентів:
https://github.com/kseniia-strelbytska/agent-dashboard

Працювала під наставництвом засновника компанії та професора машинного навчання Кембриджського університету Ференца Хусара (Ferenc Huszár). Reasonable займається формальною верифікацією програмного забезпечення — математичним доведенням того, що програма робить саме те, що від неї очікується.

Автоматизувала переклад системних протоколів із TLA+ у Verus, використовуючи цикли LLM «доводчик–рев’юер» (prover–reviewer), контрольовані детермінованими перевірками. Вивчила екосистему TLA+ (weak/strong fairness, TLC, TLAPS, PlusCal) та відфільтрувала з корпусу дублікати, тривіально істинні (vacuous) і навмисно некоректні специфікації. Опанувала формальну верифікацію та структуру доказів у Verus. Використала HDBSCAN-кластеризацію ембедингів для дослідження набору даних TLA+. Успішно переклала великий корпус специфікацій, використовуючи паралельні systemd workers на AWS EC2 та запускаючи контейнеризовані завдання через AWS Batch/Spot із checkpointing у S3, обробкою переривань Spot-інстансів і механізмом claim-and-heartbeat. Створила набір даних на рівні окремих властивостей для бенчмаркінгу та fine-tuning (RLVR) LLM на доведеннях у Verus — для подальшого використання іншими командами стартапу.

Автоматизувала доведення властивостей систем у Verus для створення даних для SFT із витягнутими ланцюжками міркувань. Розробила захищену межу цілісності між агентами-доводчиком і рев’юером, використовуючи Linux UIDs, підписані журнали (signed ledgers) і git hooks. Інтегрувала підтримку моделей через OpenRouter (opencode harness), Grok (grok-build) та GLM (opencode). Провела red-teaming пайплайна; виявила опубліковані TLA+ протоколи з доведено хибними властивостями та побудувала контрприклади для кожної з них. Також провела експерименти з потужністю рев’юера — контрольований експеримент із 48 запусками та контрольною умовою always-accept, щоб дослідити роль LLM-рев’юера у генерації доказів.

Навички: Formal Verification · Verus · Temporal Logic of Actions (TLA+) · LLM Orchestration · Experimental Design · Unsupervised Learning · Rust · Python · Docker · Linux · Git · Amazon Web Services (AWS) · AWS Batch · AWS Fargate · Amazon CloudWatch · Terraform · SQLite

• Працювала в команді над вивченням принципів дифузії в дискретному середовищі: прямого та зворотного дифузійних процесів, графіків шуму, дискретних і неперервних цільових функцій тощо.
• Реалізувала в PyTorch дифузійну модель для мовних задач на основі нещодавнього дослідження (https://arxiv.org/pdf/2406.07524). Продовжила проєкт, щоб дослідити здатність дискретних дифузійних моделей до узагальнення.
• Побудувала та оптимізувала архітектури на основі трансформерів для мовного моделювання, здобувши практичний досвід роботи з механізмами уваги та синусоїдальними позиційними кодуваннями.
• Досліджувала white-box adversarial attacks на попередньо навчені моделі класифікації зображень; вивчила та реалізувала різні black-box атаки.

Навички: PyTorch · Дифузійні моделі · Трансформерні моделі · Змагальні атаки (Adversarial Attacks) · Машинне навчання