🤖 machine learning

Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

Dit artikel introduceert het Verduisterde Natuurlijke Getallenspel als een benchmark om "Architectonisch Redeneren" te evalueren—het vermogen om bewijzen te synthetiseren met uitsluitend lokale axioma's zonder semantische aanwijzingen—en toont aan dat, terwijl algemene grote taalmodellen prestatieverlies lijden onder verduistering, gespecialiseerde redeneringsmodellen hun nauwkeurigheid behouden, waardoor er een onderscheid wordt gemaakt tussen echt logisch redeneren en patroonherkenning.

Oorspronkelijke auteurs: Lixing Li

Gepubliceerd 2026-05-04

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC0 1.0

Oorspronkelijke auteurs: Lixing Li

Oorspronkelijk artikel vrijgegeven aan het publieke domein onder CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een student leert een wiskundepuzzel op te lossen. Meestal komt de puzzel met behulpzame labels zoals "Optellen", "Vermenigvuldigen" of "Opvolger". Een slimme student begrijpt de regels van het spel misschien niet echt; ze herkennen misschien gewoon het woord "Optellen" en roepen een ingesleten truc op die ze eerder hebben gezien.

Dit artikel stelt een moeilijke vraag: Doen deze AI-modellen daadwerkelijk wiskunde, of zijn ze gewoon goed in het herkennen van woorden?

Om dit uit te vinden, creëerden de onderzoekers een "geblinddoekte" versie van een beroemd wiskundespel genaamd de Natural Number Game. Hieronder wordt uitgelegd hoe ze dit deden en wat ze ontdekten, in eenvoudige bewoordingen:

Het Experiment: Het "Buitenaardse" Spel

De onderzoekers namen een standaard wiskundespel waarbij elke regel en elk getal een duidelijke naam heeft (zoals add of zero). Vervolgens voerden ze een "scrambler" uit. Ze vervingen elke betekenisvolle naam door willekeurige, nonsens-strings zoals x9z, q22 en b7a.

Het Originele Spel: Je ziet add en weet dat het optellen betekent.
Het Gescrambelde Spel (Obfuscated NNG): Je ziet x9z en hebt geen idee wat het betekent. Je kunt niet raden; je moet naar de logica kijken van hoe de stukjes in elkaar passen om uit te zoeken wat x9z doet.

Dit test iets wat de auteurs "Architectural Reasoning" noemen. Het is het vermogen om een oplossing te bouwen met uitsluitend de structurele blauwdrukken (de logica), waarbij je de behulpzame borden op de deuren (de namen) negeert.

De Resultaten: De "Latency Tax"

De onderzoekers testten verschillende top-AI-modellen op zowel het originele spel als het gescrambelde spel. Ze vonden twee belangrijke dingen:

1. De "Universele Latency Tax" (Iedereen wordt trager)
Toen de namen gescrambeld waren, duurde het bij elk AI-model langer om de problemen op te lossen.

Analogie: Stel je voor dat je naar een bekend koffiezetapparaat rijdt. Je kent de borden, de straatnamen en de herkenningspunten. Stel je nu voor dat iemand alle borden heeft overgeschilderd en de straten heeft hernoemd met willekeurige letters. Je weet nog steeds hoe je moet rijden, maar je moet stoppen, naar de kaart kijken en bij elke bocht harder nadenken. Je komt uiteindelijk wel aan, maar het kost veel langer.
De Bevinding: De AI-modellen moesten deze "mentale kaartreconstructie" voor elk probleem uitvoeren. Ze konden niet alleen vertrouwen op het geheugen; ze moesten de ruwe logica verwerken, wat hen tijd kostte.

2. De "Redeneren versus Bijleren" Scheiding
Hoewel iedereen trager werd, splitste de nauwkeurigheid van de modellen zich in twee duidelijke groepen:

De "Algemene" Modellen (bijv. GPT-4o, Claude): Deze modellen zijn als studenten die geweldig zijn in het memoriseren van flashcards. Toen de namen gescrambeld waren, raakten ze in de war. Hun slagingspercentage daalde aanzienlijk.
- Wat dit betekent: Ze vertrouwden op de "borden" (de namen) om de puzzel op te lossen. Toen de borden weg waren, konden ze zich niet meer vinden.
De "Redenerende" Modellen (bijv. DeepSeek-R1, GPT-5, DeepSeek-Prover-V2): Deze modellen zijn als studenten die de regels van het spel daadwerkelijk begrijpen. Zelfs toen de namen gescrambeld waren, bleef hun slagingspercentage exact hetzelfde.
- Wat dit betekent: Ze hadden de labels niet nodig. Ze keken naar de logische structuur (de "architectuur") en bedachten de oplossing net zo goed als daarvoor.

De Conclusie

Het artikel concludeert dat er een echt verschil is tussen AI die alleen patronen matcht (zoals het herkennen van het woord "add") en AI die echt kan redeneren door logische structuren.

Algemene modellen zijn als toeristen die een reisgids met namen nodig hebben. Als je de reisgids wegneemt, raken ze verdwaald.
Redenerende modellen zijn als architecten die de blauwdrukken kunnen lezen. Zelfs als het gebouw geen borden heeft, kunnen ze nog steeds uitzoeken hoe de muren en balken in elkaar passen.

De studie bewijst dat hoewel alle AI-modellen "trager" worden wanneer ze worden gedwongen na te denken zonder labels, alleen de echte "redenerende" modellen hun nauwkeurigheid hoog kunnen houden in deze "buitenaardse" omgeving. Dit suggereert dat AI in de toekomst nieuwe wiskunde moet kunnen ontdekken (waar nog geen namen of labels bestaan), hebben we deze op redenering gerichte modellen nodig, niet alleen diegenen die goed zijn in patroonherkenning.

1. Probleemstelling

Ondanks het succes van Large Language Models (LLM's) in formele wiskundebenchmarks zoals MiniF2F en PutnamBench, blijft een kritieke ambiguïteit bestaan: bezitten deze modellen echte logische redeneercapaciteiten, of voeren ze slechts semantische patroonherkenning uit tegen hun voortrainingsdata?

De Kloof: Huidige benchmarks vertrouwen vaak op bibliotheekretrieval (bijv. Mathlib), waarbij succes afhankelijk is van het herkennen van hoogwaardige lemma's en semantische identificatoren (bijv. add, succ). Dit faalt in het testen van het vermogen van een model om bewijzen te synthetiseren in "vreemde" wiskundige domeinen waar geen externe bibliotheken of vertrouwde semantische aanwijzingen bestaan.
De Noodzaak: Om geautomatiseerde theoremaontdekking te bereiken, moet AI Architecturale Redenering demonstreren: het vermogen om formele bewijzen te synthetiseren uitsluitend met behulp van lokale axioma's, definities en structurele logica, onafhankelijk van semantische betekenis of externe repositories.

2. Methodologie

De auteurs introduceren het Obfuscated Natural Number Game (O-NNG), een zero-knowledge benchmark ontworpen om structurele redenering te isoleren van lexicaal zoeken.

A. Het Obscuratie-algoritme

De kerninnovatie is de systematische verwijdering van semantische aanwijzingen uit het Natural Number Game (NNG) in Lean 4:

Ruisniveau ( $\lambda$ ): Gedefinieerd in het bereik $[0, 1]$ $[0, 1]$ .
- $\lambda = 0$ : Origineel NNG (semantische identificatoren intact).
- $\lambda = 1.0$ : Volledige randomisatie van identificatoren.
Perturbatiemechanisme: Een exponentiële relatie $P = \lambda^{2.5}$ $P = λ^{2.5}$ bepaalt de waarschijnlijkheid van karakter-niveau perturbaties.
- Substitutie: Vervangt karakters door geldige Unicode/ASCII-kandidaten.
- Insertie: Injecteert nieuwe karakters (waarschijnlijkheid $0.4P$ ).
- Verwijdering: Verwijdert karakters (waarschijnlijkheid $0.3P$ ), waarbij wordt gegarandeerd dat identificatoren niet leeg blijven.
Doel: Dit proces transformeert de dataset naar een "gesloten omgeving" waar identificatoren (bijv. axioma's, theorema's, tactieken) willekeurige strings zijn, waardoor het model gedwongen wordt uitsluitend te vertrouwen op de logische structuur van de Peano-axioma's.

B. Experimentele Opstelling

Dataset: 68 formele problemen uit het NNG, georganiseerd in 8 modules (Optelling, Vermenigvuldiging, enz.).
Geëvalueerde Modellen: Vijf state-of-the-art modellen via API:
- Redeneermodellen: DeepSeek-R1, GPT-5, DeepSeek-Prover-V2.
- Algemene Modellen: GPT-4o, Claude-Sonnet-4.5.
Pijplijn:
1. Parsing: NNG extraheren met strikte afhankelijkheidsordening.
2. Obscuratie: Toepassen van karakter-niveau perturbaties gebaseerd op $\lambda$ .
3. Query-Generatie: Prompts construeren die "vreemde" axioma's, doeltheorema's en beschikbare tactieken bevatten.
4. Inferentie: Modellen geven een JSON uit met een natuurlijke taalplanning ("Draft") en Lean 4-code ("Code").
5. Verificatie: Geautomatiseerde validatie met de Lean 4 compiler (v4.27.0) om syntaxis- en logische fouten te controleren.
Metrieken:
- Correct Rate (%): Ratio van succesvol bewezen theorema's.
- Gemiddelde Tijd (s): Inferentielatentie.

3. Belangrijkste Bijdragen

Definitie van Architecturale Redenering: Geformaliseerd als het vermogen om bewijzen te synthetiseren met uitsluitend lokale definities en axioma's binnen een gesloten theorie, waarbij externe bibliotheken en hoogwaardige geautomatiseerde tactieken (zoals linarith) worden uitgesloten.
De O-NNG Benchmark: Een nieuw, zero-knowledge evaluatiekader dat de "Semantisch-Redeneerkloof" kwantificeert door prestatiedegradatie te meten wanneer semantische identificatoren worden verwijderd.
Kwantificering van de "Latency Tax": Gevestigd dat het navigeren door vreemde domeinen een universele computatiekosten (toegenomen inferentietijd) oplegt aan alle modellen, ongeacht de architectuur.

4. Resultaten en Analyse

De studie onthult een scherpe divergentie in modelgedrag wanneer semantische aanwijzingen worden verwijderd:

Universele Latency Tax:
- Alle modellen vertoonden een statistisch significante toename in inferentietijd naarmate $\lambda$ toenam.
- Implicatie: Het verwijderen van semantische identificatoren dwingt modellen tot intensievere interne zoekopdrachten of logische reconstructie, ongeacht hun basisvermogen.
Divergentie in Robuustheid (Nauwkeurigheid):
- Redeneermodellen (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2): Behielden stabiele nauwkeurigheid over alle ruisniveaus ( $\lambda \in [0, 1]$ $λ \in [0, 1]$ ). De daling in prestaties was niet statistisch significant.
  - Conclusie: Deze modellen vertrouwen op structurele logica en kunnen de Peano-axioma's navigeren zonder semantische ankers.
- Algemene Modellen (GPT-4o, Claude-Sonnet-4.5): leden een statistisch significante daling in succespercentages naarmate $\lambda$ $λ$ toenam.
  - Conclusie: Hun prestaties op standaard formele taken vertrouwen sterk op semantische patroonherkenning en vertrouwdheid met naamgevingsconventies in plaats van pure logische synthese.
Statistische Significantie: Een-Weg ANOVA bevestigde dat de prestatiedaling voor algemene modellen en de toename van de latentie voor alle modellen statistisch significant waren ( $p < 0.05$ ).

5. Betekenis en Implicaties

Benchmarken van Echte Redenering: O-NNG biedt een rigoureuze metriek om modellen te onderscheiden die wiskunde "kennen" via patroonherkenning van diegenen die kunnen "redeneren" via structurele logica.
Architecturale Richting: De resultaten suggereren dat voor de toekomst van geautomatiseerde theoremaontdekking (AI4Math) op redenering gerichte architecturen (zoals DeepSeek-R1 en GPT-5) superieur zijn aan algemene modellen, aangezien ze robuust zijn tegen het ontbreken van semantische priors.
De "Redeneer Uncanny Valley": De data wijst op een niet-lineair verband waarbij partiële ruis misschien schadelijker is dan totale obscuratie, wat suggereert dat residuële semantische aanwijzingen kunnen fungeren als afleidende heuristieken.
Toekomstige AI-agenten: De bevindingen pleiten voor de ontwikkeling van "Knowledge-Grounded Semantic Agents" die kunnen opereren in domeinen met onvolledige of verduisterde ontologieën, een vereiste voor het ontdekken van nieuwe wiskundige theorema's.

Kortom, het artikel demonstreert dat terwijl huidige LLM's bekende problemen kunnen oplossen via patroonherkenning, alleen specifieke "redenerende" architecturen de Architecturale Redenering bezitten die nodig is om problemen op te lossen in volledig onbekende, geobscurateerde logische omgevingen.