Naukowcy odkryli fundamentalny problem w działaniu dużych modeli językowych: potrafią one udowodnić twierdzenia matematyczne, ale tragicznie zawodzą przy obalaniu ich fałszywych wariantów. Zjawisko, nazwane luką falsyfikacji, nie znika przy standardowym fine-tuningu - wręcz przeciwnie, może się pogorszać. Zespół zaproponował nowe podejście polegające na traktowaniu generowania kontrprzykładów jako problemu emisji świadków (witness emission) controlowanej per-twierdzeniowymi weryfikatorami w Pythonie.
Do badań przygotowano SymCE, zbiór treningowy liczący 4707 fałszywych koniunkcji z algebry undergraduate i analizy rzeczywistej, każda wyposażona w działający weryfikator. To kluczowe, bo weryfikator pełni tu podwójną rolę: jest zarówno narzędziem oceny rozwiązań, jak i źródłem sygnału nagrody. Eksperymenty z modelami Qwen3-4B i Gemma-3-4B ujawniły pułapkę naśladowania: gdy nauczano model wyłącznie na kontrprzykładach używając SFT, jego zdolność rozpoznawania prawdziwych twierdzeń spadła z 0.27 do praktycznie zera. To prawidłowość, która powtarzała się konsekwentnie na czterech niezależnych nasionach losowych.
Natomiast uczenie przez wzmacnianie z rzadkim sygnałem nagrody (GRPO z outcome-only reward) problem naprawił całkowicie - model osiągnął 0.66 dokładności i przewyższył baseline. Zaskakujące: rzadkie i gęste nagrody dały statystycznie nieodróżnialne wyniki w domenie treningowej, ale przy testowaniu na zbiorze kalibracyjnym rozbieżności sięgnęły 33 punktów procentowych. Pochodzą one z partial-credit termu w funkcji nagrody. Finalny model 4B-bitowy pokonał wszystkie testowane open-weights specjalizacje matematyczne o wielkości 7B i pozostaje konkurencyjny z sześcioma frontowymi komercyjnymi API-ami, zarazem transferując się bez zmian promptów do popularnych benchmarków (GSM8K, MATH-500, MMLU-college-math). Audyt 177 decyzji weryfikatora wykazał 99.7% precyzji.