---
title: "Приховані помилки в ПЗ: штучний інтелект Claude знайшов сотні багів"
description: "Компанія Anthropic повідомила, що модель Claude перевірила безпеку 123 бібліотек з відкритим кодом і знайшла сотні прихованих багів за допомогою математичних доведень."
date: 2026-10-23T14:38:49.051Z
lang: uk
url: https://xab.info/uk/posts/claude-znayshov-prihovani-pomilki-v-pz
tags: [claude, anthropic, artificial-intelligence, cybersecurity, software-testing, programming]
author: "Олександр Буран"
publisher: "XAB.info"
---

# Приховані помилки в ПЗ: штучний інтелект Claude знайшов сотні багів

![Ноутбук на дерев'яному столі з відкритим інтерфейсом штучного інтелекту Claude та кодом на екрані](https://xab.info/media/2026/10/23/claude-nashel-skrytye-oshibki-v-po/claude-nashel-skrytye-oshibki-v-po-1.webp)

## Ключові тези

- Модель Claude перевірила безпеку 123 бібліотек з відкритим кодом.
- ШІ використовував математичні доведення для аналізу асемблерного коду RISC-V.
- Було виявлено дефекти, які пропускалися тестувальниками роками.
- Модель здатна самостійно виправляти знайдені помилки.

Компанія Anthropic офіційно заявила про успішне застосування своєї моделі Claude для перевірки безпеки 123 бібліотек з відкритим кодом. Використовуючи передові математичні доведення, штучний інтелект зміг виявити сотні прихованих помилок та вразливостей, які традиційні методи тестування пропускали протягом багатьох років.

### Математичний підхід до верифікації коду

У межах спільного проєкту з фірмою Theorem, що спеціалізується на верифікації програм, розробники з Anthropic застосували суворі математичні доведення безпосередньо до скомпільованого машинного коду. Традиційні інструменти тестування та фаззингу генерують великий обсяг вхідних даних, але фізично не можуть перебрати всі можливі комбінації для гарантування безпеки.

Для розв'язання цього завдання модель Claude перетворила наявні фаз-тести на чіткі математичні специфікації. Це дозволило штучному інтелекту згенерувати доведення того, що 239 точок входу в 123 бібліотеках гарантовано не призведуть до збоїв за виконання певних умов в асемблерному коді архітектури RISC-V.

### Автоматизація перевірки та виправлення помилок

Для незалежної перевірки згенерованих доведень відповідності специфікаціям дослідники залучили окремий інструмент під назвою Rocq. Такий підхід повністю звільнив розробників від необхідності вручну перевіряти кожен рядок програмного коду.

Ба більше, нейромережа продемонструвала здатність не лише знаходити дефекти, а й самостійно їх виправляти, а також створювати нові доведення для оновленого програмного забезпечення. Це суттєво прискорює цикл розробки та підвищує загальну надійність критично важливих компонентів.

### Виявлені вразливості та обмеження методу

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

Попри вражаючі результати, фахівці Anthropic наголошують, що формально перевірене програмне забезпечення не стає абсолютно бездоганним. Отримані гарантії поширюються виключно на конкретні властивості, вхідні дані та припущення, закладені в кожне окреме доведення в межах змодельованого середовища Linux.

### Значення технології для майбутнього розробки

Впровадження моделей штучного інтелекту в процес математичної верифікації відкриває нові перспективи для забезпечення кібербезпеки в усьому світі. Очікується, що подальше вдосконалення технологій та можливість повторного використання доведень дозволять кратно знизити фінансові та часові витрати на аудит найскладніших програмних систем.

## Перевірка фактів і джерела

- [Скрытые ошибки в ПО: Claude нашел сотни багов, которые тесты пропускали годами](https://www.rbc.ua/ukr/news/prihovani-pomilki-pz-claude-znayshov-sotni-1792763196.html) - Основной источник подтверждает все детали заявления Anthropic о проверке 123 библиотек, использовании модели Claude и математических доказательств.

## Часті запитання

### Яке завдання виконувала модель Claude?

Claude перевірила безпеку 123 бібліотек з відкритим кодом, перетворивши фаз-тести на математичні специфікації та знайшовши сотні прихованих помилок.

### Які інструменти використовувалися для перевірки результатів?

Для незалежної перевірки згенерованих доведень дослідники застосовували окремий інструмент під назвою Rocq.

### Чи стає ПЗ повністю безпечним після такої перевірки?

Ні, отримані гарантії поширюються лише на конкретні властивості, вхідні дані та припущення, описані в кожному окремому доведенні.