68 papers
Dit artikel introduceert een nieuw geometrisch raamwerk dat redeneren in grote taalmodellen beschrijft als vloeiende trajecten in representatieruimte, waarbij empirische bevindingen aantonen dat deze modellen logische invarianten als hogere-orde geometrie internaliseren, wat de "stochastische papegaai"-hypothese uitdaagt en wijst op een universeel representatief principe.
Dit paper introduceert Strat2Rocq, een methode die bewijsstrategieën uit grote taalmodellen extraheert en formaliseert als lemmata om het succespercentage van het symbolische bewijsinstrument CoqHammer te verhogen, terwijl deze lemmata ook de prestaties van taalmodel-agenten ten goede komen.
Dit paper introduceert SpotIt, een nieuwe evaluatiepipeline die formele verificatie gebruikt om onbetrouwbare testgebaseerde Text-to-SQL-evaluaties te verbeteren door actief databases te zoeken die gegenereerde en grondwaarheid SQL-query's onderscheiden.
Dit artikel presenteert een schaalbare methodologie voor het formeel verifiëren van drijvende-kommaberekeningen via directe RTL-tot-RTL modelchecking, waarbij een verdeel-en-heerst-strategie wordt gecombineerd met door AI gegenereerde eigenschappen en menselijke feedback om de dekking en efficiëntie te maximaliseren.
Dit artikel stelt een Brouweriaans beperkingsprincipe voor verantwoord AI voor dat in hoog-risicodomeinen alleen uitspraken toestaat die onderbouwd zijn met een openbaar controleerbaar en betwistbaar certificaat, waardoor systemen in andere gevallen "Onbepaald" moeten teruggeven om de epistemische agency van de gebruiker te waarborgen.
Dit artikel toont aan dat in de pure polymorfe afhankelijke typetheorie (P2) de afleidbaarheid van inductie- en co-inductieprincipes voor kwotiënt- en co-inductieve typen onmogelijk is, en dat functieverlenging een cruciale voorwaarde is voor het bewijzen van inductie.
Dit paper introduceert Fluid Logic en Continuous Modal Logical Neural Networks (CMLNNs), een raamwerk dat modale redenering overbrengt van discrete Kripke-structuren naar continue variëteiten via neurale stochastische differentiaalvergelijkingen om logisch consistente oplossingen te genereren zonder kennis van de onderliggende dynamica.
SpotIt+ is een open-source tool die Text-to-SQL-systemen evalueert door middel van gebonden equivalentieverificatie en een door LLM's ondersteunde constraint-mining pipeline om realistische database-instanties te genereren die verschillen tussen gegenereerde en grondware SQL-query's blootleggen.