FormalScience: AI-system hjälper forskare översätta fysik till formell kod
Forskare har utvecklat FormalScience, ett AI-system som hjälper domänexperter att översätta informella vetenskapliga resonemang till formellt verifierbar kod. Systemet testades på 200 universitetsnivå fysiksuppgifter och uppnådde perfekt formell giltighet, men forskarna identifierade betydande utmaningar med semantisk drift – när AI:n ändrar innebörden medan den försöker formalisera resonemanget.
Djupdykning
Forskare har skapat FormalScience, ett system som låter domänexperter utan djup programmeringskunskap formalisera vetenskapliga resonemang till matematiskt verifierbar kod med hjälp av språket Lean4. Systemet kombinerar AI-agenter med mänsklig input för att översätta informella fysikproblem till formella bevis som datorer kan kontrollera - något som tidigare varit extremt svårt eftersom AI-modeller ofta missar nyanserna i vetenskaplig notation och specialiserad matematik. Det intressanta här är inte bara den tekniska prestationen, utan vad den avslöjar om gapet mellan hur människor och maskiner förstår vetenskap. När systemet inte kan bevara full semantisk mening uppstår fenomen som "notational collapse" - där komplexa fysikaliska begrepp förenklas bort - vilket visar att formell verifiering och mänsklig förståelse inte alltid överlappar perfekt. FormalPhysics-datasetet med 200 universitetsnivå-problem i kvantmekanik och elektromagnetism blir första riktmärket för hur väl AI kan hantera verklig vetenskaplig formalisering. Det är som att bygga en bro mellan den röriga kreativiteten i vetenskaplig upptäckt och datorernas krav på exakt precision.