Програмування як мистецтво — пів століття потому

💡 Усі статті, обговорення, новини про AI — в одному місці. Приєднуйтесь до AI спільноти!

Мене звати Станіслав, я .NET-розробник. У цій статті я ділюся власним досвідом і думками щодо використання ШІ та його ролі в процесі розробки. Стаття обговорює ідеї Дональда Кнута 1974 року та розглядає їх у контексті сучасної епохи штучного інтелекту. Я обговорюю історичну перспективу — від математичних основ програмування та відповідності Каррі — Говарда до використання ШІ. Також приділяю увагу тому, як змінюється сама суть програмування та яка роль залишається за людиною.

Програма як математичне доведення

У 1974 році Дональд Кнут отримував премію Тюрінга та зробив промову «Computer Programming as an Art» — Програмування як мистецтво.

Минуло понад пів століття і сьогодні його ідеї сприймаються інакше. Вперше з’явилися системи, здатні самостійно працювати з кодом і формальними структурами. Те, про що Кнут говорив обережно, сьогодні стало реальністю:

«...their aim is to create machines that write programs better than we can, given only the problem specification.»

«The Art of Computer Programming» і сама промова 1974 року Computer Programming as an Art — це послідовна позиція автора. Перші комп’ютери створювалися для математичних і наукових обчислень. у 1970-х їх дедалі частіше використовували для комерційних задач.
Але для Кнута термін Program і далі означав точне формальне розв’язання математичної задачі. Тут важливо наголосити, що сама ідея програми виросла з математики та математичної логіки. Не програма для математики, а структурно програма від самого початку була математичним об’єктом. Програма потребує точної формалізації: вона задає сувору послідовність перетворень. Теорія обчислень виникала поруч з логікою, теорією доведень, λ-численням, а не поруч із прикладною інженерією. Саме в цьому сенсі Кнут пов’язує програму з математичним доведенням. Пишучи програму, зауважує він, ми знаємо, що за потреби могли б побудувати формальний доказ її коректності. Для математика доведення завжди стосується конкретного твердження: теореми, леми чи тези. Кнут говорить про програму і доведення як про тісно пов’язані, але все ж окремі речі: програма існує, а її коректність може бути доведена.

Проте приблизно в той самий час у математичній логіці формувалася і розвивається наступна ідея. Роботи Гаскелла Каррі 1930-х років та Вільям Говарда 1969 року поступово привели до того, що згодом назвуть відповідністю Каррі-Говарда: програма і доведення виявляються не просто пов’язаними, а структурно тотожними. Згідно з відповідністю Каррі-Говарда, твердження — це сам тип. Сигнатура функції — це і є теза, яку потрібно довести. А тіло функції — це і є доведення цієї тези. Відповідність Каррі-Говарда складалася поступово.

Гаскелл Каррі у 1934 році працював над комбінаторною логікою — формальною системою для аналізу функцій та їх застосування. Каррі виявив відповідність між логікою та формальною системою опису функцій.

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

Приклад програми як доведення, виглядатиме так:
Припустімо, у нас є функція f, яка відображає значення одного типу у значення іншого. Її тип записується як: f : Number → String. У логіці Каррі-Говарда такий тип читається не як твердження про числа і рядки, а як логічна імплікація: «Якщо існує об’єкт типу Number, то можна побудувати об’єкт типу String». З цієї точки зору сама функція f — це не просто перетворення даних, а конструкція, що реалізує таке твердження.

Або більш коректний приклад з математичної точки зору. Припустімо, що маємо функцію: f : A → B. Якщо існує доведення A, то існує доведення B. Тоді функція f є конструкцією, яка перетворює будь-яке доведення A на доведення B. Таким чином між доведеннями та програмами встановлюється структурна відповідність.

Обчислення тоді відповідає перетворенню доведення, що приводить його до нормальної форми. Тобто формальні структури, які Каррі аналізував як логік, виявилися тісно пов’язаними з тими самими конструкціями, що пізніше стали основою практичних мов програмування. Саме тому комбінаторна логіка Каррі та λ-числення Чорча через кілька десятиліть стали однією з математичних основ функціональних мов програмування. На практиці це реалізовано в мовах та системах доведення Rocq Prover, Agda та Lean. У Coq було доведено Four Color Theorem. Lean використовується для побудови Mathlib. CompCert — це сертифікований компілятор C, який не вносить помилок під час компіляції.

Коли математик доводить теорему в Coq, Agda чи Lean, він пише λ-вираз потрібного типу. Те, що Чорч придумав у 1936 році як абстрактну модель обчислень, те, що Каррі у 1934 році помітив як цікаву відповідність, і те, що Говард у 1969 році довів як теорему, виявилося одночасно:

— фундаментом теорії обчислюваності;
— основою функціональних мов програмування;
— робочим інструментом для доведення теорем.

Три різні дисципліни — одна формальна структура. Саме в цьому полягає зміст фрази «програма є доведенням»: те, що ви пишете в редакторі коду, буквально є тим самим об’єктом, який використовує математик. Просто в різних контекстах за ним стоять різні інтерпретації та різні прикладні застосування. Тобто, програма — це не абстракція і не довільна інженерна практика. Відповідність Каррі-Говарда дає змогу розглядати програму як об’єкт, що підпорядковується внутрішнім структурним закономірностям. Це не просто зручна модель для інженерів, а факт про природу формальних систем. Мови програмування є інженерним втіленням цих закономірностей.

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

Код, який пише машина

Неминуче постає питання, згадане на самому початку: у 1974 році Кнут припустив, що машини ніколи повністю не досягнуть мети писати програми краще за людину. Значною мірою ця мета вже досягнута. Сьогодні ШІ пише код: інколи погано, часто прийнятно, дедалі частіше добре — це факт, який важко заперечити. Питання Кнута формально зводиться до такої схеми:
Що саме робить людина під час програмування і який результат отримує?
Що саме робить ШІ і який результат отримує?
Чи збігаються ці множини?

Чому ШІ здатний генерувати працездатний код, можна навести кілька причин.

Жорстка формальна структура. Мови програмування спроєктовані для однозначної інтерпретації; синтаксис і типи радикально звужують простір допустимих варіантів у будь-якому місці коду.

Ідіоматична кластеризація. Переважна частина корисного коду є повторенням відомих патернів у відомих контекстах. Програмісти розв’язують схожі задачі схожими способами; це статистично регулярність. Дешева зовнішня перевірка. Компілятор, система типів, тести та виконання програми — кожен із цих механізмів миттєво подає сигнал про валідність результату. Модель, яка побачила мільйони програм, здатна з високою надійністю генерувати локально валідні фрагменти коду. Це структурна властивість самої галузі, яку можна вимірювати й кількісно описувати.

Пояснення архітектури сучасних LLM може зайняти досить багато часу, але можна показати фундамент, який лежить в основі. Базовим елементом є штучний нейрон. Ще в 1943 році В. Маккалохом та В. Піттс запропонували математичну модель штучного нейрона. Їхня стаття називалася «A Logical Calculus of the Ideas Immanent in Nervous Activity». Потім Розенблат у 1958 році реалізував мережу як комп’ютерну програму і далі як електронний пристрій — перцептрон. Перцептрон була перша система, яка могла навчатися на прикладах.
Формальний штучний нейрон з функцією активації сигмоїда може виглядати так:

 
double z = inputs.Zip(weights, (x, w) => x * w).Sum() + bias;
double y = 1.0 / (1.0 + Math.Exp(-z));

Вся суть зведена до однієї дії. Систему не програмують правилами, для системи знаходять ваги за умови зменшення помилки, рухаючись градієнтним спуском. Суттєве інше: поведінку тут не виводять, її знаходять.
Окремий нейрон — це локальна функція. Мережа — композиція функцій: вихід одного шару стає входом наступного, і формально це орієнтований граф диференційовних перетворень. Повністю формальний об’єкт, у якому кожна операція визначена, але зміст не заданий: ми задаємо лише структуру й ціль, а поведінка з’являється з даних. Виразна сила береться не з нейрона (він майже не змінився з 1950-х), а з того, як функції з’єднані.

Цікаво, що ранні кроки до багатошарових мереж були зроблені ще у 1960-х роках у Києві. Олексій Івахненко разом із Валентином Лапою розробили перші робочі алгоритми навчання багатошарових мереж, а вже до 1971 року навчали мережі у вісім шарів.

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

У 2017 році стаття «Attention Is All You Need» запропонувала прибрати рекурсію і використовувати механізм уваги: кожний елемент послідовності може взаємодіяти зі всіма іншими, незалежно від відстані між ними, а ваги цих зв’язків навчаються. Трансформер тут — не просто інженерне покращення. Автори запропонували змінити цілий апарат і виявилося, що це спрощує і робить систему ефективнішою. Після появи трансформерної архітектури розвиток нейромереж пішов не стільки шляхом нових базових елементів, скільки через масштабування і перебудову режимів навчання. Масштабування, інструкційна адаптація, вирівнювання поведінки — три основних напрями куди рухається розвиток.

Успіх моделей, які генерують код, скоріше говорить про природу програмування: це пошук у структурованій множині. Коли програміст або ШІ пише код, він не вигадує спосіб — він знаходить його в просторі вже існуючих формальних можливостей. Саме так можна визначити діяльність.

Відкривати, а не відтворювати

Якщо програма є формалізацією структури, а не довільним твором, із цього випливає ще один наслідок.

У просторі формальних систем різні рішення виявляються нерівнозначними. Одні конструкції виглядають випадковими, механічно складеними; інші мають внутрішню неминучість: зміна будь-якого елемента погіршує систему. Досвідчений математик, фізик або програміст зазвичай розпізнає це майже миттєво. Йдеться ще не про «красу» в психологічному сенсі й не про особистий смак. Йдеться про структуру: мінімальність припущень, щільність зв’язків, симетрію, здатність великої кількості наслідків випливати з невеликої кількості засновків. Саме тому різні галузі — математика, фізика, логіка, програмування — знову й знову приходять до схожих оцінок. Деякі структури сприймаються як більш фундаментальні не тому, що вони подобаються спостерігачеві, а тому, що всередині самої системи вони мають вищий ступінь узгодженості.

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

Відповідність Каррі-Говарда важлива для нас не лише тим, що пов’язує програми та доведення. Вона усуває можливість розглядати програмування як суто довільну інженерну діяльність. Програма виявляється окремим випадком більш загальної проблеми: існування формальних систем, усередині яких одні конструкції є стійкими, а інші руйнуються. Складовими формальної системи є символи, аксіоми та правила виведення, які визначають, які саме перетворення вважаються допустимими. Формальну систему можна зрозуміти так: аксіома є вихідним твердженням, прийнятим без доведення; логіка — це правила, за якими з аксіом отримують наслідки. Логіка не створює істину, а зберігає істинність під час переходу від одних тверджень до інших. Аксіоми — це початкова позиція в шахах, а логіка — правила руху фігур.

Повчальна історія, що відкриває новий погляд на формальні системи — це п’ятий постулат Евкліда. Евклід вважав свої аксіоми «самоочевидними істинами» про простір: точка, пряма, через дві точки проходить одна пряма тощо. Але одна з них — постулат про паралельні прямі — виглядала підозріло складною, і протягом двох тисяч років математики намагалися довести його з решти аксіом, вважаючи, що насправді це теорема. Нікому це не вдалося. У XIX столітті Лобачевський, Бойяї та Гаусс незалежно один від одного зробили зворотний крок: а що, якщо його заперечити? У результаті виникла несуперечлива геометрія — неевклідова. А згодом, на початку XX століття, з’ясувалося, що саме неевклідова геометрія описує реальний простір-час у загальній теорії відносності.

Цікаво, що аксіоми, які здавалися самоочевидними істинами про світ, насправді є вибором, і різні вибори дають різні результати. Отже, аксіоми — це не обов’язкові істини, а вихідні припущення, які визначають, який саме простір можливий усередині системи. Зміна аксіом змінює сам простір можливих істин. Однак слід зазначити, що більшість можливих наборів аксіом виявляються нежиттєздатними. Одні призводять до суперечностей і руйнують систему. Інші виявляються надто слабкими: з них неможливо вивести нічого, окрім повторення самих себе.

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

Типізоване λ-числення в чистому вигляді працює як логіка: типи — це твердження, програми — це доведення. Додавання необмеженої загальної рекурсії руйнує властивості, необхідні для інтерпретації програм як конструктивних доведень: у такій системі стає можливим будь-яке твердження, включно з хибним. Тому мови, що зберігають логічну коректність — Coq, Agda та Lean, — не допускають загальної рекурсії (general recursion): кожна функція повинна гарантовано завершуватися. Натомість Haskell і більшість мейнстримних функціональних мов загальну рекурсію дозволяють. Усі ці приклади — п’ятий постулат, парадокс Рассела, стійкість шахів, тонка рівновага типізованих мов та багато іншого — показують одне й те саме. Те, що здавалося самоочевидною істиною або єдино можливою структурою, насправді є вибором. Але цей вибір не є довільним. Простір можливих аксіом обмежений: лише небагато комбінацій породжують стійкі та несуперечливі системи. Тому аксіоми не винаходять — їх відкривають.

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

Theory of Models (Model Theory) вивчає зв’язок між аксіомами та структурами, у яких вони виконуються.
Theory of Proofs (Proof Theory) досліджує силу формальних систем, їхню несуперечливість і межі довідності.
Theory of Computability (Computability Theory) та Algorithmic Information Theory показують, що змістовні теорії мають високий ступінь структурованості.
Reverse Mathematics досліджує, які мінімальні набори аксіом необхідні для різних розділів математики.
Category Theory розглядає математику як систему перетворень, а не як набір окремих сутностей.

Також деякі філософські позиції:
— Платонізм. Формальні структури існують незалежно — у власному просторі, як «речі самі по собі». Платон у міфі про печеру описує це так: в’язні, прикуті в печері, бачать на стіні лише тіні фігур, що проходять позаду них, і сприймають ці тіні як реальність. Дослідник виходить із печери та бачить самі фігури. Формалізовані структури — це «фігури» за межами досвіду, а аксіоматика є спробою їх описати. Працездатний набір аксіом потрапляє в реальну формальну структуру.
— Формалізм. Жодної реальності за формальними системами немає — це лише правила гри зі знаками. Єдиним критерієм залишається несуперечливість системи.
— Емпіризм. Теорії відбираються відповідністю досвіду. Аксіоматики виживають там, де дозволяють робити передбачення та будувати працездатні машини. Про це говорять Мілль, Квайн і сучасна філософія науки.
— Конструктивізм. Існує лише те, що ми можемо побудувати за допомогою скінченної процедури. Нескінченні множини без конструктивного опису існують не більше, ніж єдиноріг.
— Структуралізм. Математичні об’єкти — це не речі, а позиції в структурі. Що таке «число 7» — неважливо; важливим є його місце серед інших чисел і його відношення всередині структури.
— Натуралізм. Інтуїції є продуктом адаптації когнітивної системи до світу. Ми вважаємо певні структури «природними» або «красивими» не тому, що вони мають самостійний онтологічний статус, а тому, що такий спосіб організації мислення виявився еволюційно ефективним для передбачення та виживання.
Усі перелічені підходи — математичні та філософські — по-різному відповідають на одне й те саме питання: що саме робить формальну структуру працездатною. Проте попри всі відмінності залишається спільний факт: людина виділяє з безлічі можливих формальних систем саме ті, які виявляються стійкими та продуктивними.

Дональд Кнут у своїх міркуваннях наголошував, що значна частина процесу дослідження належить до сфери artistry: «everything we learn about programming helps us to improve our own artistry. The mysterious insights that people have when speaking, listening, creating, and even when they are programming, are still beyond the reach of science.» Здатність виявляти й відокремлювати те, що не задано явно всередині формальної системи, і є одним із механізмів створення нового. Тут важливо розрізняти різні типи нового.
Перший — нове як нова комбінація всередині вже існуючих правил. У 2016 році AlphaGo зіграла проти Лі Седоля партію, у якій її 37-й хід став знаменитим. Коментатори називали цей хід «прекрасним», «геніальним», «таким, що виходить за межі людського розуміння гри». Це справді вихід за межі людської вибірки. Але вихід — усередині правил ґо. AlphaGo не винайшла нову гру; не змінила умову перемоги; не поставила під сумнів самі правила. Вона знайшла раніше невідому точку в уже заданому просторі можливих партій. Новизна є — але вона існує всередині системи.
Другий тип — нове як нова система. Кантор створює математику актуальних нескінченностей. Галуа створює теорію груп. Ейнштейн переосмислює простір і час — те, що раніше вважалося абсолютною основою фізики. Це новизна іншого роду: вона не лежить у просторі вже існуючих правил, а створює нові правила.
Між цими двома типами новизни лежить структурна прірва. Машина здатна породжувати новизну першого типу. Новизну другого типу вона не породжує — і не через технічні обмеження, а через принципову природу самого процесу навчання. Машина може зіграти як AlphaGo, але чи здатна вона стабільно породжувати нові простори правил — відкрите питання. І не лише тому, що моделі швидко змінюються. Саме поняття «нового» не має однозначного визначення. Будь-який приклад відкриття нового можна інтерпретувати як варіацію всередині ширшого простору, але не як самостійний тип. У цьому сенсі «нове» перестає бути стійкою категорією: воно описує не особливий клас явищ, а зміну способу організації та інтерпретації вже існуючого. Водночас важливо, що така інтерпретація залежить від обраної позиції: у різних філософських рамках те, що виглядає як новизна, може розумітися як відкриття вже існуючої структури, наслідок правил системи або результат когнітивної конструкції.

ШІ проти людини. Хто така людина в цій дискусії? Якщо людина — це те саме, тобто модель, навчена на досвіді, тоді суперечка «ШІ чи людина» зводиться до економіки процесу. Не до суперечки про онтологію, не до суперечки про природу діяльності, а до простого підрахунку: скільки кіловат-годин потрібно одному й іншому, щоб отримати однаковий результат. Людський мозок — нейронна мережа, навчена на життєвому досвіді та культурному корпусі. ШІ — нейронна мережа, навчена на оцифрованому корпусі. У такій картині artistry Кнута, mysterious insights і вихід за межі корпусу — це або метафори, які описують складніші, але не принципово інші форми тієї самої статистичної роботи, або самообман. Питання про те, чи є людське мислення чимось більшим, ніж система, здатна до навчання, існувало тисячоліттями. Але майже всю історію воно залишалося суто філософським: порівнювати було ні з чим. Людина спостерігала лише саму себе. Будь-яка відома форма інтелекту була біологічною, еволюційною та вбудованою в той самий світ людського досвіду. Тепер у нас є з чим порівнювати. ШІ — це система, яка демонструє інтелектуальну поведінку, залишаючись при цьому свідомо статистичним механізмом навчання. Сьогодні людина може поставити поруч із собою систему, яка вміє писати код, доводити теореми, вести діалог, створювати тексти та знаходити неочікувані рішення — і водночас залишається всередині простору статистично засвоєних структур. І саме тут питання перестає бути технічним. Тому що йдеться вже не про те, чи здатна машина писати код краще за людину. Йдеться про те, що саме робить людина, коли створює, розуміє та обирає підстави. Саме тут починається момент вибору. По-новому починає звучати і питання про природу формалізації — формалізм, емпіризм, натуралізм, структуралізм, конструктивізм. Кожну з цих позицій тепер можна перевірити простим запитанням: чи зберігає вона структурну відмінність між людиною та моделлю, що навчається, чи розчиняє її в простій різниці ефективності? Цю перевірку я залишаю читачеві, оскільки деякі позиції породжують доволі цікаві наслідки.
Якщо за формальними системами стоїть певна реальність, тоді доступ до цієї реальності є вже не статистичною властивістю, а онтологічним відношенням. У такій картині людина й ШІ займаються різною діяльністю: людина відкриває, ШІ відтворює. На мій погляд, те, як людина відкриває реальні структури — саме наближення до «речей самих по собі» — проявляється не у висловлюваннях, а в самій діяльності. Дрібні вибори в повсякденному житті — можливо, це і є слід відкриття та момент прийняття рішення. Значна частина людського мислення справді будується через повторення, адаптацію та засвоєння патернів. Однак повністю жити як система, що навчається й тренується, означає нею і бути — без здатності відкривати.

У 1974 році Кнут назвав свою промову Computer Programming as an Art. Тоді слово «мистецтво» означало майстерність ремісника — те, що відрізняє досвідченого програміста від початківця: відчуття стилю, вибір архітектури, розуміння задачі. Це було мистецтво в античному значенні techne — високий ступінь володіння ремеслом. Через п’ятдесят років слово «мистецтво» в цій назві набуває глибшого значення. Коли ремесло переходить до машини, у людини залишається те, що не зводиться до відтворення навчального корпусу: здатність відкривати. Здатність працювати там, де навчального корпусу ще немає. Здатність наблизитися до самих структур — і з цього наближення створити нову формалізацію, якої раніше не існувало, а також мати сміливість прийняти нову аксіому.