Amazon: Інвестиції в Lean для надійних та безпечних ШІ-агентів

Інвестиції Amazon у Lean для безпеки ШІ-агентів

Amazon оголосила про надання значної та довгострокової фінансової підтримки команді Lean Focused Research Organization (FRO), яка відповідає за розробку відкритої мови програмування Lean. Цей крок є частиною посиленої уваги Amazon до розробки ШІ-агентів, зокрема до їхньої безпеки та надійності.

Lean, що існує з 2014 року, є популярною мовою програмування в таких галузях, як математика, фізика та комп'ютерні науки. Amazon вже використовує її всередині компанії для розробки агентного ШІ.

Роль Lean у верифікації ШІ

Привабливість Lean для Amazon полягає в її здатності допомагати в розробці та тонкому налаштуванні можливостей міркування ШІ. Мова програмування використовується разом з «помічником доведення» — програмним забезпеченням, що перевіряє код для виявлення та усунення помилок або недоліків. Саме ці «доведення коректності» роблять Lean кращим вибором для академічних дослідників та фахівців у наукових галузях.

Amazon зазначає, що «генерація формальних доведень ШІ в Lean стала ключовим методом для навчання моделей з нижчим рівнем помилок, до того, що вони тепер створюють правильні рішення для проблем дослідницького рівня». Компанія вважає, що поєднання генеративного ШІ з математичною строгістю Lean допоможе створити перевірених, надійних ШІ-агентів.

Практичне застосування та виклики

Amazon вже застосовує верифікацію на основі Lean у своєму сервісі Bedrock AgentCore, де вона допомагає «довести коректність мови політики», що забезпечує роботу агентів у суворих межах. Lean також лежить в основі таких систем, як SampCert, яка надає «математичні гарантії» для захисту конфіденційності на платформі аналітики AWS Clean Rooms, та AWS Neuron. Нещодавно вчений використав велику мовну модель (LLM) з Lean для доведення коректності протоколу відновлення сегментів Amazon Aurora, що є критично важливим для довговічності розподіленим протоколом, за значно менший час, ніж це зайняло б вручну.

Пітер Ван дер Путтен, доцент ШІ в Лейденському університеті та директор лабораторії ШІ Pegasystems, вітає інвестиції AWS у Lean. Він підкреслює, що такі відкриті технології, як Lean, мають потенціал для забезпечення сильніших гарантій формальної верифікації для програмного забезпечення та систем ШІ. Він зазначає, що в міру того, як агентні ШІ-системи стають все більш автономними, технології, що можуть надати сильніші гарантії коректності та безпеки, ніж традиційне тестування, стануть надзвичайно важливими.

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

Відкритий вихідний код та прозорість

Підтримка FRO служить ширшій меті, ніж просто доповнення власного використання Lean Amazon. Компанія зазначає, що «легше довіряти доведенню, коли ви можете самостійно оцінити інструменти, що стоять за ним». Клієнти, аудитори та регулятори можуть незалежно перевіряти та валідувати роботу, виконану в інструментах, керованих спільнотою, що забезпечує прозорість, необхідну для критично важливого для безпеки ШІ. У довгостроковій перспективі зростаюча популярність Lean принесе користь індустрії ШІ, надаючи «більше бібліотек, більше інструментів та більше формалізованих доведень для всіх».

Що це означає для розробників

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

Ключові факти

Amazon надає «значну, довгострокову» фінансову підтримку команді Lean Focused Research Organization (FRO).
FRO очолює розробку відкритої мови програмування Lean, яку Amazon вже використовує для розробки агентного ШІ.
Lean існує з 2014 року і популярна в математиці, фізиці та комп'ютерних науках.
Amazon використовує Lean разом з «помічником доведення» для перевірки коду та виявлення помилок, що забезпечує «доведення коректності».
«Генерація формальних доведень ШІ в Lean стала ключовим методом для навчання моделей з нижчим рівнем помилок».