Thema: Mathematik

  • AlphaEvolve: Algorithmen durch evolutionäre Codesuche

    AlphaEvolve sucht nach Programmen, die ein klar messbares Ziel verbessern. Kandidaten werden automatisch ausgeführt und bewertet; erfolgreiche Varianten dienen als Ausgangspunkt für weitere Vorschläge. Ergebnisse sind besonders belastbar, wenn die Bewertungsfunktion die Aufgabe vollständig abbildet.

    Forschungsfrage

    Können Sprachmodelle nicht nur Code schreiben, sondern durch wiederholte, automatisch bewertete Variation neue und effizientere Algorithmen entdecken?

    Ansatz

    • Mehrere Sprachmodelle schlagen Programmvarianten vor
    • Automatische Evaluatoren messen Korrektheit oder Leistung
    • Eine evolutionäre Datenbank wählt vielversprechende Kandidaten
    • Neue Generationen verändern und kombinieren erfolgreiche Programme

    Berichtete Anwendungen

    • Optimierung von Rechenzentrums- und Planungsalgorithmen
    • Beiträge zu Chipdesign und KI-Training
    • Neue Varianten für Matrixmultiplikation
    • Suche nach Lösungen mathematischer Probleme

    Warum das überprüfbarer ist

    Die Ausgabe besteht aus ausführbarem Code. Dieser kann mit Tests, Benchmarks oder mathematischen Prüfungen bewertet werden. Das reduziert, aber beseitigt nicht die Gefahr einer unvollständigen Bewertungsfunktion.

    Grenzen

    • Die Aufgabe benötigt eine verlässliche maschinelle Bewertungsfunktion
    • Optimierung kann unbeabsichtigte Lücken im Messverfahren ausnutzen
    • Entdeckter Code muss von Fachleuten verstanden, getestet und abgesichert werden

    Status

    Aktives Forschungssystem; konkrete Zugänglichkeit und Einsatzbereiche sind begrenzt und können sich ändern.

    Primärquellen

  • FunSearch: Programme als mathematische Entdeckungen

    FunSearch erzeugt Programme, deren Qualität objektiv berechnet werden kann. Auf diese Weise wurden neue Konstruktionen für das Cap-Set-Problem und Heuristiken für Online-Bin-Packing gefunden. Die Methode funktioniert nur bei Problemen, die sinnvoll als Programm und Bewertung formuliert werden können.

    Forschungsfrage

    Kann ein Sprachmodell durch automatische Prüfung zu neuen, menschlich interpretierbaren Lösungen in Mathematik und Informatik beitragen?

    Ansatz

    • Ein Ausgangsprogramm und eine Bewertungsfunktion definieren das Problem
    • Das Sprachmodell verändert ausgewählte Programme
    • Jede Variante wird ausgeführt und bewertet
    • Gute und unterschiedliche Lösungen fließen in neue Generationen ein

    Veröffentlichte Ergebnisse

    • Neue große Cap Sets in bestimmten Dimensionen
    • Verbesserte Heuristiken für das Online-Bin-Packing
    • Ausgabe als kompakte Programme, die von Forschenden analysiert werden können

    Bedeutung

    Die Kombination aus generativer Suche und strenger automatischer Bewertung zeigt einen Weg, wie Sprachmodelle über bloße Textvorschläge hinaus zu überprüfbaren Resultaten beitragen können.

    Grenzen

    • Nicht jedes Forschungsproblem besitzt eine vollständige Bewertungsfunktion
    • Eine hohe Punktzahl kann Nebenbedingungen übersehen
    • Mathematische Interpretation und formale Prüfung bleiben erforderlich

    Primärquellen

  • AlphaGeometry: Geometriebeweise ohne menschliche Demonstrationen

    Das System erzeugt Hilfskonstruktionen und prüft geometrische Folgerungen symbolisch. In einem Testset löste es 25 von 30 ausgewählten Olympiade-Aufgaben innerhalb der vorgegebenen Zeitbedingungen. Der Vergleich betrifft einen begrenzten Bereich formaler Geometrie und keine allgemeine mathematische Intelligenz.

    Forschungsfrage

    Wie können kreative geometrische Konstruktionen mit streng überprüfbaren Beweisschritten verbunden werden?

    Ansatz

    Ein neuronales Modell schlägt zusätzliche Punkte, Linien oder Kreise vor. Eine symbolische Engine leitet daraus formal gültige Aussagen ab und sucht einen vollständigen Beweis.

    Veröffentlichte Ergebnisse

    • 25 von 30 Aufgaben des IMO-AG-30-Testsets gelöst
    • Vorheriger Vergleichsansatz löste 10 Aufgaben
    • Beweise wurden in symbolisch nachvollziehbarer Form erzeugt

    Bedeutung

    • Verbindung generativer Vorschläge mit formaler Verifikation
    • Synthetische Trainingsdaten statt menschlicher Lösungsdemonstrationen
    • Forschung zu maschinellem Theorembeweisen und mathematischen Assistenzsystemen

    Grenzen

    • Spezialisiert auf euklidische Olympiade-Geometrie
    • Testset und Vergleich erlauben keine Aussage über gesamte Mathematik
    • Formale Übersetzung und geeignete Werkzeuge bleiben für andere Gebiete schwierig

    Primärquellen