Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability

Technische Samenvatting: Betrouwbaar Redeneren met Grootte Taalmodellen via Op Voorkeuren Gebaseerde Maximum Satisfiability

Probleemstelling

Grootte Taalmodellen (LLMs) tonen sterke capaciteiten in het begrijpen van natuurlijke taal en het genereren van code, maar vertonen aanzienlijke onbetrouwbaarheid wanneer ze worden ingezet voor complexe optimalisatieproblemen die meerdere beperkingen en door de gebruiker gedefinieerde voorkeuren omvatten. In domeinen zoals robotica en logistiek, waar correctheid en bewijsbare optimaliteit cruciaal zijn, slagen LLMs er vaak niet in om harde beperkingen te voldoen of objectiefuncties te minimaliseren wanneer ze uitsluitend vertrouwen op intern redeneren (bijvoorbeeld Chain-of-Thought) of directe antwoordgeneratie. Deze falen vloeien voort uit de combinatorische aard van optimalisatie en het onvermogen van de LLM om exact redeneren uit te voeren, wat leidt tot onhaalbare of suboptimale oplossingen die moeilijk te verifiëren zijn. Bovendien vereisen bestaande formele methoden zoals Maximum Satisfiability (MaxSAT) dat gebruikers voorkeuren uitdrukken in gespecialiseerde, starre talen (bijvoorbeeld PDDL), wat een drempel vormt voor niet-experts.

Methodologie

Het artikel stelt een hybride neuro-symbolische aanpak voor die redeneren uit de LLM externaliseert naar een formele solver. Het kernparadigma, aangeduid als "vibe coding", omvat het laten vertalen van probleembeschrijvingen in natuurlijke taal door de LLM naar uitvoerbare Python-code, die vervolgens wordt opgelost door een exacte MaxSAT-solver.

De voorgestelde pijplijn bestaat uit de volgende fasen:

1. Intermediaire Planning: Voordat code wordt gegenereerd, wordt de LLM gevraagd om een gestructureerde, symbolische beschrijving te produceren van de beslissingsvariabelen, harde beperkingen en zachte voorkeuren. Deze stap beoogt de modelleerprecisie te verbeteren door een systematische ontleding van het probleem af te dwingen.
2. Codegeneratie: De LLM genereert Python-code met behulp van de PySAT-API om het probleem te coderen als een gewogen partiële MaxSAT-instantie. Harde beperkingen worden gecodeerd als harde clausules, terwijl gebruikersvoorkeuren worden gecodeerd als gewogen zachte clausules.
3. MaxSAT-oplossing: De gegenereerde code wordt uitgevoerd om een MaxSAT-solver te activeren (specifiek RC2 uit PySAT). De solver garandeert dat de teruggegeven toewijzing haalbaar is (voldoet aan alle harde clausules) en optimaal is (minimaliseert het totale gewicht van niet-voldane zachte clausules) met betrekking tot de gecodeerde probleemstelling.
4. Verificatie: Om het systeem te evalueren zonder te vertrouwen op het interne redeneren van de LLM, construeren de auteurs een "canonieke" MaxSAT-codering voor elke probleeminstantie. Deze canonieke codering dient uitsluitend als grondwaarheid voor verificatie. De oplossing geproduceerd door de door de LLM gegenereerde code wordt vergeleken met deze canonieke codering om te controleren op:
   • Haalbaarheid: Voldoet de oplossing aan alle harde beperkingen?
   • Optimaliteit: Bereikt de oplossing dezelfde objectivewaarde als de canonieke optimale oplossing?
   • Opmerking: Deze verificatie staat alternatieve coderingen en meerdere optimale oplossingen toe, mits deze correct zijn onder de referentiese-mantiek.
5. Feedbacklus: Als de code niet wordt uitgevoerd of een fout produceert, wordt het foutbericht teruggegeven aan de LLM voor verfijning. Cruciaal worden de canonieke verificatieresultaten (haalbaarheids-/optimaliteitscontroles) niet gebruikt als feedback aan het model tijdens het generatieproces om datalekken of overfitting op de referentie te voorkomen.

Belangrijkste Bijdragen

• Neuro-symbolisch Kader: De auteurs presenteren een methode waarbij LLMs fungeren als natuurlijke taalinterfaces voor gewogen partiële MaxSAT-solvers, die gebruikersintentie vertalen naar formele MaxSAT-formuleringen via codegeneratie.
• Onafhankelijke Verificatie: De studie introduceert een evaluatieprotocol dat door LLM gegenereerde oplossingen verifieert tegen een canonieke codering op zowel haalbaarheid als optimaliteit, waardoor de geldigheid van de oplossing wordt ontkoppeld van de correctheid van het interne redeneren van de LLM.
• Empirische Analyse van Voorkeuren: Het artikel analyseert hoe verschillende door de gebruiker gedefinieerde voorkeursconfiguraties de prestaties van LLM-redenering beïnvloeden bij diverse beperkingsoptimalisatieproblemen.
• Evaluatie van Intermediaire Planning: Het werk onderzoekt de effectiviteit van een intermediaire planningsstap en komt tot de bevinding dat dit de prestaties verbetert voor sterkere modellen, maar mogelijk foutpropagatie introduceert voor zwakkere modellen.

Experimentele Resultaten

De aanpak werd geëvalueerd op drie families van op voorkeuren gebaseerde redeneertaken: Maximum Independent Set (MIS), Planning en Set Cover. De dataset bestond uit 300 instanties (25 per familie × 4 voorkeursvarianten) getest op vier LLM's (GEMINI-3.1-PRO, GPT-5.5, LLAMA3.3 en QWEN3-CODER).

• Basisprestaties: Baselines voor directe antwoorden en Chain-of-Thought (CoT) presteerden slecht, vaak met acceptatiepercentages van 0% op MIS- en Planning-taken. Baselines voor Program-of-Thought (PoT) toonden lichte verbeteringen, maar bleven aanzienlijk lager dan de MaxSAT-gebaseerde aanpak.
• Prestaties van de MaxSAT-pijplijn: De voorgestelde MaxSAT-gebaseerde pijplijn behaalde aanzienlijk hogere acceptatiepercentages. Voor sterke modellen zoals GEMINI-3.1-PRO en GPT-5.5 overschreden de acceptatiepercentages 80% op Set Cover-taken en bereikten ongeveer 56–59% op Planning- en MIS-taken wanneer intermediaire planning werd gebruikt.
• Invloed van Planning: Intermediaire planning verbeterde consequent de prestaties voor de sterkste modellen (bijvoorbeeld verbeterde GEMINI-3.1-PRO van 36% naar 56% op MIS). Voor zwakkere modellen (LLAMA3.3, QWEN3-CODER) verslechterde planning echter soms de prestaties, wat suggereert dat foutpropagatie kan optreden als het model de planning niet getrouw kan vertalen naar uitvoerbare code.
• Voorkeursgevoeligheid: Hoewel gebruikersvoorkeuren over het algemeen de acceptatiepercentages verlaagden ten opzichte van de instelling "geen voorkeur", bleef de MaxSAT-gebaseerde aanpak robuuster dan de baselines over alle voorkeursvarianten heen.

Betekenis en Claims

Het artikel claimt dat de primaire bijdrage geen nieuwe solver-architectuur is, maar een empirische en methodologische demonstratie van het gebruik van LLM's als interfaces voor formele solvers voor voorkeursbewuste optimalisatie. De auteurs stellen het volgende:

1. Externalisatie is Sleutel: LLM's mogen niet worden vertrouwd om optimalisatieredenering intern uit te voeren; in plaats daarvan zijn ze zeer effectief in het vertalen van beperkingen in natuurlijke taal naar uitvoerbare code.
2. Betrouwbaarheid via Solvers: Door de optimalisatie en verificatie toe te vertrouwen aan sound en complete MaxSAT-solvers, bereikt het systeem formele garanties van haalbaarheid en optimaliteit die puur LLM-redeneren niet kan bieden.
3. Robuustheid: De combinatie van semantische interpretatie door de LLM en MaxSAT-oplossing maakt robuuste, verifieerbare besluitvorming mogelijk die gebruikersvoorkeuren accommodert zonder gespecialiseerde domeintalen te vereisen.

De auteurs concluderen dat het scheiden van semantische interpretatie (LLM) van formele optimalisatie (MaxSAT-solver) een veelbelovende richting is voor het bouwen van betrouwbare, gebruikersgerichte besluitvormingssystemen, met name op gebieden waar correctheid van het grootste belang is. Zij merken op dat toekomstig werk interactieve settings zal verkennen waarbij gebruikers voorkeuren iteratief kunnen verfijnen met ondersteuning van deze neuro-symbolische lus.