Forskere har præsenteret en ny compilerstyret proof search-metode, der forbedrer AI's evne til at bevise matematiske sætninger i Lean 4-projekter med 12,8 procentpoint i gennemsnitlig pass rate inden for et budget på 32 forsøg, samtidig med at antallet af LLM-kald reduceres med 21,9 procent. Metoden, beskrevet i et arXiv-paper, adresserer en central udfordring: beviser i virkelige projekter afhænger ofte af projektspecifik kontekst, hvilket gør det svært for AI-modeller at finde korrekte beviser første gang.
Kernen i metoden er en balance mellem udforskning og udnyttelse. Den udforsker forskellige startpunkter gennem dual-model generering og stagnation-triggeret resampling, mens den udnytter lovende proof states gennem current-best refinement styret af compiler-grundet parvis sammenligning. Dette betyder, at systemet lærer af fejl og forbedrer delvist korrekte beviser uden at forringe dem.
For beslutningstagere er implikationen klar: AI-assisteret softwareudvikling kan blive mere effektiv og pålidelig, især i komplekse projekter med domænespecifik logik. Metoden demonstrerer, at compiler-feedback kan bruges som en guide til at reducere spildte LLM-kald, hvilket har direkte omkostningsimplikationer for virksomheder, der investerer i AI-drevne udviklingsværktøjer. Selvom resultaterne er specifikke for Lean 4, peger de på en bredere tendens: integration af compiler- og værktøjsfeedback i AI-workflows kan forbedre både kvalitet og effektivitet.
