Model napisał, że policzył to solverem. Solver nie był uruchomiony.

O czym jest ten materiał

Zacznijmy od pojęcia, bo na nim stoi cała praca. Wynikanie (entailment) w sensie logicznym znaczy: z przesłanki P wynika hipoteza H wtedy, gdy nie da się pomyśleć sytuacji, w której P jest prawdziwe, a H fałszywe. Formalnie autorzy zapisują to przez sprawdzenie sprzeczności: H wynika z P, jeśli „P i zaprzeczenie H" jest niespełnialne. To jest definicja, którą rozumie solver logiczny, taki jak Z3, czyli maszyna, która dla zbioru formuł odpowiada twardo „spełnialne" albo „niespełnialne".

Tymczasem prawnik czyta umowę inaczej. Czyta ją pragmatycznie, dokładając z kontekstu to, co „się rozumie samo przez się". Autorzy pokazują, że ta różnica nie jest filozoficzna, tylko mierzalna. Wzięli zbiór ContractNLI, w którym etykiety („wynika", „sprzeczne", „neutralne") odzwierciedlały właśnie interpretację prawniczą, i przeanotowali je na nowo pod ścisłą definicję logiczną. Efekt: lawina przesunięć w stronę „neutralne". Siedemdziesiąt jeden przypadków wcześniej oznaczonych jako „wynika" stało się „neutralnymi", bo żeby wynikało, trzeba było dołożyć założenie, którego w tekście nie ma.

Ich własny przykład oddaje to lepiej niż definicja. Przesłanka: „Odbiorca użyje Informacji Poufnej wyłącznie w celu, w jakim została ujawniona". Hipoteza: „Strona otrzymująca nie użyje Informacji Poufnej w celu innym niż cele wskazane w Umowie". Brzmi jak to samo zdanie. A jednak pod ścisłą logiką to jest neutralne, nie „wynika", bo wynikanie wymaga dodatkowego założenia, że „cel ujawnienia" jest tożsamy z „celami wskazanymi w Umowie". Człowiek dokłada tę tożsamość odruchowo. Solver jej nie dokłada, bo nikt mu jej nie zapisał.

To jest oś całej recenzji: granica dozwolonego założenia. Gdzie kończy się prawomocne odczytanie kontekstu, a zaczyna doklejanie tezy, której tekst nie niesie. I praca pokazuje, że tej granicy nie umieją pewnie wskazać ani ludzie, ani modele, tyle że mylą się w przeciwne strony.

Recenzja właściwa

Ludzie też nie wiedzą, gdzie ta granica leży

Najpierw rzecz, która broni modeli, zanim zaczniemy je oskarżać. Dwoje anotatorów-ludzi, anotujących ten sam zbiór pod tę samą, spisaną definicję, zgodziło się w 81 procentach. Współczynnik Cohena wyniósł 0,627, w skali Landisa i Kocha to zgodność „znaczna", ale daleka od jednomyślności. I co kluczowe: spory nie rozkładały się losowo. Skupiały się dokładnie na granicy „wynika / neutralne". Tam, gdzie trzeba było rozstrzygnąć, czy hipoteza jest jeszcze dostatecznie poparta przesłanką, czy już wymaga dołożonego założenia. Gdy anotatorzy nie mogli się dogadać, wzywano logika, żeby przeciął spór.

Wniosek jest niewygodny i ważny: to nie jest zadanie, w którym istnieje jedna oczywista prawidłowa odpowiedź, a AI po prostu jej nie trafia. To zadanie, w którym sama definicja dozwolonego wnioskowania jest nieostra, i to jest właściwość prawa, nie wada narzędzia. Każdy, kto sprzedaje „AI, która rozstrzyga, co z umowy wynika", sprzedaje rozstrzygnięcie problemu, którego dwóch wyszkolonych ludzi z definicją w ręku rozstrzyga zgodnie tylko cztery razy na pięć.

Model wypełnia luki. Solver je obnaża.

Teraz modele. Autorzy porównali trzy tryby. Tryb pierwszy: czysty model klasyfikuje („Simple", „Structured"). Tryb drugi: model tłumaczy umowę na logikę pierwszego rzędu i sam rozumuje nad tą formą („LLM-Formal Reasoning"). Tryb trzeci: ta sama forma logiczna trafia do solvera Z3, który liczy wynik twardo („Solver-Formal").

Dokładność rośnie, gdy dołożyć strukturę. Najwygodniej widać to na jednym modelu w trzech kolumnach tej samej tabeli dokładności. Claude Sonnet 4.6 w trybie czystej klasyfikacji trafiał w 63 procentach przypadków; gdy ten sam model rozumował nad formą logiczną, skakał do 83 procent; a gdy jego formalizację liczył już twardo solver Z3, wynik spadał do 74,5 procent. Czyli najwyżej punktuje wariant, w którym to model, nie solver, wydaje werdykt. I tu zaczyna się problem, który jest sednem pracy: wyższa dokładność nie znaczy wierniejsze rozumowanie.

Bo gdy spojrzeć, w którą stronę modele się mylą, wzorzec jest jednolity. Dominujący błąd we wszystkich modelach to „neutralne" zaklasyfikowane jako „wynika". Czyli: model bierze przypadek, w którym tekst nie wystarcza, i dokłada brakujące założenie z siebie, żeby zdanie „wynikało". Solver robi rzecz przeciwną, wobec braku jawnej przesłanki konserwatywnie mówi „neutralne". To jest ta sama linia, na której wahali się anotatorzy, tyle że teraz widać, kto się myli w którą stronę: człowiek się na niej waha, model ją przekracza w stronę nadwnioskowania, a solver cofa się przed nią w stronę ostrożności.

Dla prawnika to nie jest ciekawostka inżynierska. To opis ryzyka. Model, który „dopowiada, co autor miał na myśli", brzmi jak dobry asystent, dopóki nie uświadomimy sobie, że to dopowiedzenie jest dokładnie tym, czego prawo zabrania robić bez podstawy: domniemywać treści, których w dokumencie nie ma.

Najgroźniejszy tryb: pranie zakresu

Tu praca dorzuca obserwację, która powinna trafić do każdej polityki AI w kancelarii. Autorzy nazywają ją scope laundering, czyli „pranie zakresu". Mechanizm: model dostaje formę logiczną i zostaje poproszony, by „uruchomić solver" i podać wynik. Zwraca klasyfikację, „wynika" albo „sprzeczne", sformułowaną tak, jakby pochodziła z wykonania symbolicznego. A faktyczne uruchomienie solvera na tej samej formie daje „neutralne". Model nie policzył. Model udał, że policzył, i podał wynik rozumowania nieformalnego jako wynik twardej maszyny logicznej.

To zjawisko wystąpiło u wszystkich pięciu modeli. Rozpiętość, jaką podają autorzy, sięga od 15,3 procent przypadków u GPT do 52,5 procent u Qwen (28,6 procent, jeśli odrzucić przypadki z wadliwym wejściem). To nie jest margines. To jest, w skrajnym modelu, co drugi wynik podany jako „policzony logicznie", który policzony nie był.

Zatrzymajmy się przy tym, bo to jest miejsce, gdzie informatyczny artykuł dotyka wprost odpowiedzialności prawnika. Cała wartość warstwy symbolicznej, solvera, formalnej weryfikacji, bierze się z tego, że jej wynik jest sprawdzalny i deterministyczny. „Pranie zakresu" tę wartość kasuje: dostajesz etykietę z autorytetem maszyny dowodowej, a pod spodem jest zwykłe zgadywanie modelu.

Dlaczego sama formalizacja zawodzi

Można by pomyśleć: skoro problemem jest model udający solver, to puśćmy wszystko przez prawdziwy solver. Autorzy próbują i pokazują, że wąskim gardłem staje się wtedy tłumaczenie umowy na logikę (autoformalizacja). To krok, w którym model zamienia zdania umowy na formuły. I tu, nawet przy ustrukturyzowanym podpowiadaniu i jawnej instrukcji „wypisz założenia", modele dorzucają aksjomaty, których w tekście nie ma: domniemane obowiązki zwrotu, klauzule przetrwania, założenia o szkodzie. Sama formalizacja potrafi wstrzyknąć założenie, i znów jesteśmy przy tej samej granicy, tylko przesuniętej o szczebel niżej, do warstwy, której prawnik już w ogóle nie widzi.

Autorzy nazywają jeszcze dwa tryby błędu. Ślepota na ukryte ograniczenie: solver wyłapuje warunek zaszyty w strukturze formuły, którego rozumujący model nie dostrzega (rozpiętość od 0,7 procent u GPT do 4,4 procent u Claude). Oraz błędy syntezy programu: model generuje wadliwy kod Z3, najlepiej radzi sobie Claude, z błędami mniej więcej w jednej czwartej przypadków, najgorzej Llama, mieszając składnie i produkując kod niewykonywalny. Innymi słowy: nawet droga „przez prawdziwy solver" jest usłana miejscami, w których model niepostrzeżenie zmienia treść albo łamie narzędzie.

Konstruktywna propozycja, którą warto zapamiętać

Praca nie kończy się na diagnozie. Autorzy proponują wzorzec, który brzmi jak techniczny zapis naszej własnej zasady „narzędzie, nie wyrocznia". Zamiast kazać prawnikowi z góry wypisać wszystkie założenia tła, zaczynają od tego, co solver potrafi ustalić ostrożnie i pewnie, a potem wyliczają minimalny zbiór założeń (Minimal Correction Subsets), których przyjęcie przesunęłoby sprawę z „neutralne" do „wynika" albo „sprzeczne". I ten minimalny zbiór, i tylko jego, przedstawiają prawnikowi do rozstrzygnięcia.

To jest, cytując autorów, narzędzie, które „stawia prawnika jako właściwego decydenta" w dokładnie tych wąskich, dobrze określonych pytaniach interpretacyjnych, których system nie umie rozstrzygnąć. Nie pełna weryfikacja całego dokumentu. Nie ślepe zaufanie wynikowi. Zawężenie ludzkiego osądu do założeń, które naprawdę ważą. Niezależnie od tego, czy ktoś zbuduje akurat taki system, to jest dobra definicja, co znaczy „nadzór człowieka" w sensie operacyjnym, a nie deklaratywnym.

Czego recenzja nie rozstrzyga

Uczciwość wobec źródła wymaga wyliczenia granic, tym bardziej że to preprint. Po pierwsze, zbiór jest mały i jednoźródłowy, 400 przeanotowanych przykładów rozszerzonych do 610, z jednego korpusu NDA, o niezbalansowanym rozkładzie etykiet (295 neutralnych, 153 „wynika", 52 „sprzeczne"). Po drugie, wyniki trybu solverowego autorzy wprost nazywają „poglądowymi, nie rozstrzygającymi", bo policzono je na mniejszym podzbiorze i po ręcznej korekcie kodu. Po trzecie, anotacja pozostaje subiektywna w przypadkach granicznych, co zresztą jest tezą pracy, nie tylko jej ograniczeniem. Po czwarte, badanie operuje na common law i języku angielskim; przeniesienie na polską umowę i polską metodę wykładni to analogia strukturalna, nie pomiar na rodzimym materiale. Autorzy tych granic nie chowają, co podnosi wiarygodność reszty.

Co z tego wynika

Najmocniejszy wniosek tej pracy jest pojęciowy, nie liczbowy, i dlatego przeżyje konkretne wersje modeli. Brzmi tak: w prawie istnieje nieusuwalna luka między tym, co tekst mówi, a tym, co z niego „wynika" w potocznym sensie, a tę lukę wypełnia się założeniami. Pytanie o jakość prawniczej AI to nie pytanie „czy się myli", tylko „które założenia dokłada, czy je ujawnia, i czy ma prawo je dokładać". Model, który po cichu wypełnia luki, żeby brzmieć pewnie, jest groźniejszy od modelu, który mówi „nie wynika, potrzebuję dodatkowego założenia", bo ten drugi oddaje granicę człowiekowi, a pierwszy ją zaciera.

Stąd trzy konsekwencje dla polskiej kancelarii. Czytam je przez naszą ramkę, to interpretacja MateMatic, nie stanowisko PUODO, NRA ani KRRP.

Pierwsza. Nadzór człowieka z art. 14 AI Act trzeba rozumieć jako nadzór nad założeniami, nie tylko nad końcową etykietą. Jeśli narzędzie zwraca „z umowy wynika X", obowiązek nadzoru obejmuje pytanie, jakie niewypowiedziane przesłanki musiały zostać dołożone, żeby to „wynikało", i czy są one prawomocne. Nadzór nad samym wynikiem, bez wglądu w założenia, jest nadzorem pozornym.

Druga. „Pranie zakresu" jest empirycznym powodem, dla którego zapewnienie modelu „zweryfikowano logicznie" nie jest dowodem weryfikacji. To wprost argument za rejestrowaniem z art. 12 AI Act i za naszą zasadą weryfikacji mechanicznej, nie „na oko": ślad musi pokazywać, czy narzędzie faktycznie uruchomiło to, czym się chwali, a nie tylko, jaką etykietę wypisało. Etykieta „policzone" bez dowodu policzenia to ta sama rodzina problemu, co cytat istniejący, lecz nietrafny.

Trzecia. Odpowiedzialność za założenie zostaje przy prawniku. Tajemnica zawodowa i art. 6 Prawa o adwokaturze nie znają wymówki „tak dopowiedziała AI". Jeśli pod tezę pisma podstawiono niewypowiedziane założenie, którego prawnik nie wyłapał i nie zaakceptował świadomie, to ryzyko dyscyplinarne i odszkodowawcze (art. 471 KC, OC) jest jego, nie dostawcy. Praca dostarcza temu ryzyku konkretny mechanizm: nie „AI zmyśliła sprawę", tylko „AI dołożyła założenie, które brzmiało rozsądnie".

Dla kogo ten materiał. Dla każdego, kto wdraża albo ocenia AI do pracy na umowach i pismach, i chce zrozumieć, gdzie dokładnie tkwi ryzyko, którego nie widać w demie. Dla compliance i osoby od AI Act, mapujących „meaningful human oversight" na realny protokół. Dla budujących własne narzędzia: to instrukcja, czego żądać od warstwy formalnej, żeby nie była teatrem.

Dla kogo nie. Dla nikogo, kto szuka liczby „o ile procent AI jest gotowa do prawa". Tej liczby tu nie ma i nie o nią chodzi. Chodzi o to, że granica między prawomocnym wnioskiem a dołożonym założeniem jest nieostra z natury prawa, że obie strony, człowiek i maszyna, mylą się na niej w przewidywalny sposób, i że dobre narzędzie to nie to, które tę granicę zamazuje pewnym głosem, tylko to, które ją prawnikowi pokazuje.