Математиката под сурогата

Направих списък с всяка формула, която кодовата ми база твърди, че имплементира, и после накарах три различни инструмента да проверят всяка от тях независимо. Списъкът има 174 записа. Не всички минаха чисто. Това е частта, за която си струва да се говори.

Лесно е да се довериш на невронна мрежа, защото произвежда числа, които изглеждат като физика — гладки полета, правдоподобни мерни единици, цветове в правилния диапазон. Нищо от това не казва дали твърдението отдолу — самото уравнение, което кодът казва, че решава — е уравнението, което кодът реално решава. Затова през последната седмица на юли построих нещо, което нарекох “математически печат”: пайплайн за одит на формули, който събира всяко формулно твърдение в хранилището и го проверява по три независими начина.

Първи крак: символен. Всяка формула се превръща в заявка към Full Results API на Wolfram Alpha — независим, външен авторитет без интерес формулите да излязат верни. 148 заявки успяха.

Втори крак: изведен. Скрипт със sympy и numpy извежда алгебрата от първи принципи, символно, и я сверява с това, което кодът твърди. 35 проверки, 35 успешни.

Трети крак: числен. Реалният тестов пакет, пуснат наново, върху реалния код. Само в най-новата ревизия: 996 теста минали, 85 прескочени. В останалата част от хранилището: 563 минали, нула провалени.

Честната част: рядко всичките три крака се съгласяват, и го казвам открито

От 174-те твърдения само 31 са потвърдени и от трите независими метода едновременно — маркирани VERIFIED-3WAY. Още 62 са потвърдени по два начина. 16 имат само числено потвърждение (тестовете минават, но никой външен символен инструмент не се е включил). 44 имат само символно потвърждение. 10 са цитирани, но засега непроверими с наличните инструменти. И 9 са маркирани GAP — не успях да ги проверя изобщо, и посочвам всяка поименно, вместо да ги размия в средно: FSI свързване (флуид-структура), учена квадратура, моделът на батерийна електрохимия, твърдение за корелация на локален размер на характеристика и една статистика за покритие на граница.

Искам да съм ясен защо това тежи повече от чист заглавен ред “100% проверено”. Печат, който твърди, че всичко е проверено, е печат, на който не бива да се доверяваш — толкова задълбочен одит винаги намира пропуски. Документът изрично не твърди пълна проверка. Изброява какво липсва.

Двете находки, с които съм най-доволен, са и двете за нещо, което го няма

Два записа в каталога са маркирани NOT-A-CLAIM. Не “грешна формула”, не “непроверима формула”, а изобщо липсваща формула там, където се подразбираше, че има. Единият е транспортен слой в кода без заявено управляващо диференциално уравнение зад него. Другият е набор от 26 YAML файла с физични спецификации, които описват физични конфигурации, без изобщо да записват управляващото уравнение, което би трябвало да кодират. Никое от двете не е опасно само по себе си — кодът може да е структурно наред без формула, закачена към всеки файл — но липсата е находката: показва ми точно къде да погледна, преди някой да гради върху този слой с предположение, че има извод отдолу.

Одитът улови и реални структурни ограничения, не само липсваща документация. Wolfram Alpha няма мнение дали слабата форма на CutFEM дискретизация е коректна — това е въпрос на числен анализ, който никой символен инструмент не може да отсъди, затова 44 от твърденията са символно-само по необходимост, не от мързел. Директория с тестове, към която препращат 21 docstring-а в диференцируемия симулационен код, tests/test_cutfem/, не съществува в дървото. Записах го като находка, не го помете под “пропуск”. А етикет, който бях използвал небрежно, наричайки дифузионен процес “63% завършен при характерното време”, се оказа приближение — истинското число е по-близо до 0.70. Малко, но точно от този тип малки неща се натрупват, ако никой не провери.

Нищо от това не отслабва самото инженерство отдолу. Прави твърденията около него доверими по конкретен, оборим начин: можеш сам да пуснеш същите три крака и да получиш същия отговор, или да ме хванеш, ако не съвпада. Това е реалната цел на “печата” върху машинно-обучаваща система — не сертификат, който казва “вярвай ми”, а следа, която ти позволява да не се налага.

Ако градиш ML върху физика, как проверяваш уравненията отдолу днес — или вярваш на думата на модела?