Technische Samenvatting: PhysProver

Probleemstelling

Hoewel de integratie van Large Language Models (LLM's) met verifieerbare formele talen de automatische stellingbewijzing in de wiskunde (bijv. Lean4) aanzienlijk heeft geavanceerd, blijft het domein van de formele natuurkundige redenering grotendeits onderbelicht. Bestaande state-of-the-art (SOTA) stellingbewijzers, die primair zijn getraind op wiskundige datasets, vertonen een slechte prestatie op natuurkundige taken. Dit gat bestaat omdat de natuurkunde steunt op rigoureuze wiskundige fundamenten en formele afleidingen die specifiek zijn voor fysische theorieën (bijv. kwantumveldentheorie, snaartheorie), welke niet adequaat worden gerepresenteerd in huidige wiskundige stellingbewijzers-datasets. Eerdere werken hebben deze tekortkoming geïdentificeerd, maar hebben geen effectieve methoden voorgesteld om dit te overbruggen.

Methodologie

De auteurs stellen PhysProver voor, de eerste systematische aanpak om het formeel stellingbewijzen specifiek voor het natuurkundige domein te verbeteren. De methodologie bestaat uit drie kerncomponenten:

1. Dataconstructie (PhysLeanData)

Om het tekort aan hoogwaardige formele natuurkundige data aan te pakken, hebben de auteurs PhysLeanData geconstrueerd, een gespecialiseerde dataset bestaande uit ongeveer 5.541 trainingsvoorbeelden. De datageneratie-pipeline omvat:

• Seed Collectie: Het extraheren van bewijsbare lemma's en de bijbehorende bewijzen uit de open-source PhysLean repository, die domeinen zoals klassieke mechanica, elektromagnetisme, kwantummechanica, relativiteitstheorie en kwantumveldentheorie beslaat.
• Synthetische Augmentatie: Het gebruik van Claude-4.5-Sonnet om nieuwe conjecturen te genereren op basis van seed lemma-header paren.
• Verificatie-pipeline: Een tweestaps filterproces:
  1. Syntactische Verificatie: Het gebruik van de Lean-verifieerder om te waarborgen dat gegenereerde conjecturen welgevormd zijn en alle gerefereerde definities bestaan.
  2. Bewijsbaarheid Verificatie: Het inzetten van meerdere sterke bewijzers (DeepSeek-Prover-V2-7B, Kimina-Prover-Distill-8B, Goedel-Prover-V2-8B) om bewijzen te proberen te leveren. Conjecturen worden alleen behouden als ten minste één bewijzer de stelling succesvol verifieert.
• Resultaat: De uiteindelijke dataset bevat ~5.000 trainingsvoorbeelden en ~250 testvoorbeelden, gefilterd tot een maximale lengte van 4.096 tokens.

2. Trainingsframework

De auteurs maken gebruik van DeepSeek-Prover-V2-7B, een sterke open-source wiskundige stellingbewijzer, als het basismodel. In plaats van Supervised Fine-Tuning (SFT), wat volgens de auteurs de prestaties op deze taak zou verslechteren, gebruiken zij Reinforcement Learning with Verifiable Rewards (RLVR) met het Group Relative Policy Optimization (GRPO) algoritme.

• Beloningssignaal: De Lean-verifieerder levert een binaire beloning (1 voor een correct bewijs, 0 anders). Bewijzen die placeholders zoals sorry of admit bevatten, worden bestraft met een beloning van 0 om reward hacking te voorkomen.
• Curriculum Learning: Om het leren te faciliteren, wordt de trainingsdata gesorteerd op de lengte van de grondwaarheid-bewijzen, wat een "easy-to-hard" trainingsprogressie mogelijk maakt.

3. Evaluatiestrategie

Het model wordt geëvalueerd op:

• In-Distribution: De PhysLeanData testset, gecategoriseerd in Klassiek, Deeltjes & Snaren, Relativiteitstheorie en Kwantumveldentheorie.
• Out-of-Distribution (OOD): De MiniF2F-Test benchmark (wiskunde) om de generalisatiecapaciteiten buiten het natuurkundige domein te beoordelen.

Belangrijkste Resultaten

• Prestaties op Natuurkundige Benchmarks: PhysProver bereikt een algemene verbetering van 2,4% ten opzichte van de basis DeepSeek-Prover-V2-7B over alle natuurkundige subdomeinen. Met name presteert het beter in de uitdagende categorie "Particle & String" met een verbetering van 3,0%.
• Vergelijking met Propriëtaire Modellen: De 7B-parameter PhysProver presteert beter dan zowel GPT-5 als Claude-4.5-Sonnet qua algemene nauwkeurigheid op de natuurkundige testset, wat de effectiviteit van kleine, domeinspecifieke expertmodellen aantoont.
• Generalisatie naar Wiskunde: Training op natuurkundige data levert een verbetering van 1,3% op de MiniF2F-Test benchmark (pass@16) op, wat aangeeft dat formele natuurkundige training de algemene formele wiskundige redeneerkracht versterkt.
• Ablatie op SFT: Experimenten tonen aan dat standaard Supervised Fine-Tuning (SFT) op de natuurkundige dataset leidt tot een prestatiedaling van 6,4%. Daarentegen leveren Rejection-Sampling Fine-Tuning (RAFT) en de voorgestelde RLVR-aanpak verbeteringen op, wat suggereert dat het afstemmen van de outputdistributie van het model op de trainingsdata (via RL of RAFT) effectiever is dan directe SFT voor dit domein.

Betekenis en Bijdragen

De paper claimt drie primaire bijdragen:

1. Eerste Domeinspecifieke Bewijzer: Het introduceert de eerste methoden die specifiek zijn ontworpen om formele stellingbewijzers voor natuurkunde te trainen, waarmee een kritiek gat in de literatuur wordt gedicht waar SOTA-modellen falen op natuurkundige taken.
2. Dataset en Pipeline: Het ontwikkelt en publiceert PhysLeanData, een compacte maar uitgebreide dataset, samen met een pipeline voor de synthese van conjecturen afgestemd op fysische stellingen, bedoeld om de onderzoekscommunity te ondersteunen.
3. Prestaties en Generalisatie: Het demonstreert dat een model dat getraind is op een kleine (~5K) natuurkundige dataset, de SOTA wiskundige bewijzers op natuurkundige taken kan overtreffen en tegelijkertijd de prestaties op algemene wiskundige benchmarks kan verbeteren.

De auteurs concluderen dat hun werk een paradigma biedt voor het uitbreiden van formele bewijzers buiten wiskundige domeinen. Ze benadrukken dat hoewel de huidige resultaten veelbelovend zijn, de aanpak de potentie onderstreept van het gebruik van RLVR en hoogwaardige, domeinspecifieke data om de beperkingen van algemene modellen in gespecialiseerde wetenschappelijke velden te overwinnen. De dataset en het model worden aan de community vrijgegeven om verder onderzoek te stimuleren.