← Back to summary
Evergreen: Efficient Claim Verification for Semantic Aggregates
Converted from PDF with markitdown. Layout may be rough.
Evergreen: Efficient Claim Verification for Semantic Aggregates
AlexanderW.Lee BenjaminHan ShayakSen
BrownUniversityandSnowflakeInc. SnowflakeInc. SnowflakeInc.
alexander_w_lee@brown.edu benjamin.han@snowflake.com shayak.sen@snowflake.com
SamYeom UğurÇetintemel AnupamDatta
SnowflakeInc. BrownUniversityandSnowflakeInc. SnowflakeInc.
sam.yeom@snowflake.com ugur_cetintemel@brown.edu anupam.datta@snowflake.com
ABSTRACT
1.00
Withrecentsemanticqueryprocessingengines,semanticaggrega- 0.95
tionhasbecomeaprimitiveoperator,enablingthereductionofa
0.90 relationintoanaturallanguageaggregateusinganLLM.However,
theresultingsemanticaggregatemaycontainclaimsthatarenot 0.85
groundedintheunderlyingrelation.Verifyingsuchclaimsischal- 0.80
lenging:theyofteninvolvequantifiers,groupings,andcomparisons 0.75
overrelationsthatfarexceedLLMcontextwindowsandrequire
0.70
anexpensivecombinationofsemanticandsymbolicprocessing.
WepresentEvergreen,asystemthatrecastsclaimverification 10−1 100 101
asasemanticqueryprocessingtaskwithtailoredoptimizationsand Cost ($)
provenancecapture.Evergreencompileseachclaimintoadeclar-
ative semantic verification query that can execute on the same
queryengineusedtoproducetheaggregate.Toreducecost,Ever-
greenavoidsunnecessaryLLMcallsthroughverification-aware
optimizations,includingearlystopping,relevancesorting,andes-
timationwithconfidencesequences,aswellasgeneral-purpose
optimizationsforsemanticqueries,suchasoperatorfusion,similar-
ityfiltering,andpromptcaching.Eachverdictisaccompaniedby
citationsthatidentifyaminimalsetoftuplesjustifyingtheresult,
withsemanticsbasedonsemiringprovenanceforfirst-orderlogic.
Onabenchmarkofproduction-inspiredworkloadsoverrestau-
rantreviewandcustomersupportdatasets,Evergreen’soptimized
configurationsoccupytheentirecost–qualityParetofrontier.With
astrongLLM,EvergreenpreservesverificationqualityatanF1of
0.94whilereducingcostby3.1×relativetounoptimizedverifica-
tion;withasubstantiallyweakerLLM,itsurpassesthestrongest
externalbaseline’sF1(0.87vs.0.83)at7.0×lowercost.
PVLDBReferenceFormat:
AlexanderW.Lee,BenjaminHan,ShayakSen,SamYeom,UğurÇetintemel,
andAnupamDatta.Evergreen:EfficientClaimVerificationforSemantic
Aggregates.PVLDB,20(1):16-30,2026.
doi:10.14778/3845598.3845600
PVLDBArtifactAvailability:
Thesourcecode,data,and/orotherartifactshavebeenmadeavailableat
https://github.com/brown-db/evergreen.
ThisworkislicensedundertheCreativeCommonsBY-NC-ND4.0International
License.Visithttps://creativecommons.org/licenses/by-nc-nd/4.0/toviewacopyof
thislicense.Foranyusebeyondthosecoveredbythislicense,obtainpermissionby
emailinginfo@vldb.org.Copyrightisheldbytheowner/author(s).Publicationrights
licensedtotheVLDBEndowment.
ProceedingsoftheVLDBEndowment,Vol.20,No.1ISSN2150-8097.
doi:10.14778/3845598.3845600
erocS
1F
Opus 4.6 Opus 4.6
Sonnet 4.6
Haiku 4.5 Haiku 4.5 Sonnet 4.6 Qwen3-VL
Qwen3-Next Sonnet 4.6 base_rm
Opus 4.6Opus 4.6
rag_agent
Sonnet 4.6
Haiku 4.5 Sonnet 4.6 rlm
Haiku 4.5 evg_unopt Haiku 4.5 Opus 4.6
evg_opt
Figure 1: F1 vs. mean cost per claim (log scale), averaged
over three trials. We compare base_rm (LLM-as-a-judge),
rag_agent (retrieval-augmented agent), rlm (recursive lan-
guage model), evg_unopt (unoptimized Evergreen), and
evg_opt (optimized Evergreen) across Claude and Qwen
models.ThedashedlineconnectsthePareto-optimalconfig-
urations.evg_optexclusivelyoccupiestheParetofrontier.
1 INTRODUCTION
Semanticqueryprocessingengineshaverecentlyemergedinboth
academia[4,16,18,23,47,49,51,60,65,68,75,78]andindustry[24,
32,48,82].Thesesystemsfeaturesemanticoperatorsthataugment
databaseoperatorswithLLMs.Inseveralsystems[4,48,60,68],
semanticaggregationisaprimitiveoperator,reducingarelation
oftupleswithanLLM-basedaggregationfunctionspecifiedbya
prompt.Forexample,thepromptmightsummarizecustomerre-
viewsorcomparereviewsacrossrestaurants.Whentherelation
fitsintheLLM’scontextwindow,theaggregationrunsinasin-
gleLLMcall;otherwise,itprocessestherelationinchunksand
mergesintermediateresults.Yet,theresultingsemanticaggregate
maycontainclaimsthatarenotgroundedintherelation.TheLLM
mighthallucinatethat“themajorityofreviewsarepositive”when
infactonlyaminorityare,orthat“noreviewersmentionvegan
options”whenonedoes.Thecentralquestionweinvestigateis:
howcanwereliablyandefficientlydeterminewhetherthe
claimsembeddedinasemanticaggregateareactuallysup-
portedbytheunderlyingrelation?Assemanticaggregation
gainsadoptioninproductionsystemssuchasSnowflake’sCortex
AISQL[48],answeringthisquestionbecomesessential.
Verifyingclaimsinsemanticaggregatesischallengingforseveral
reasons.First,theunderlyingrelationsareoftenlarge,easilyex-
ceedingLLMcontextwindows;arelationofafewthousandreviews
16
canspanhundredsofthousandsoftokens.Second,fromourob- WeevaluateEvergreenonabenchmarkof32diverseclaims
servationsofproductionworkloadsatSnowflake,claimsthatarise overthreeYelprestaurantreviewdatasets[84]andthreeTwitter
fromsuchaggregationsofteninvolvequantifiers,groupings,and customersupportdatasets[10]basedonproduction-inspiredwork-
comparisonsacrossgroups(e.g.,“alllocationshavemultiplecom- loads.Figure1showsthatacrossarangeofLLMs,Evergreen’s
plaints”,“thetop-rankedlocationis[A]”).Verifyingtheseclaims optimizedconfigurationsformtheentirecost–qualityParetofron-
requiressemanticreasoningabouteachtuplefollowedbysymbolic tier.Comparedtoanunoptimizedversionof Evergreenwitha
reasoningovertheresultingvalues,ataskLLMsstruggletoaccom- strongLLM,itsoptimizationspreserveverificationqualityatanF1
plishreliably.Third,semanticallyevaluatingeachtuplerequiresan of0.94whilereducingcostby3.1×.Thestrongestexternalbase-
expensiveLLMinvocation,makingbrute-forceverificationprohibi- line[87]reachesanF1of0.83,whichEvergreensurpassesat0.87
tivelycostly.Finally,abooleanverdictaloneisofteninsufficient: with7.0×lowercostusingasubstantiallyweakerLLM.Thisrobust-
usersexpectcitationstotheunderlyingdatathatexplainit. nessreflectsEvergreen’sdeclarative,neuro-symbolicdesign:an
Existingapproachestoclaimverificationfallshortforsemantic LLMspecifiesonlythehigh-levelverificationquery,whilesymbolic
aggregates.NaiveLLM-as-a-judgemethods[54,72,91]assessa queryprocessinghandlesoptimizationandexecution,restricting
claimagainstaprovidedsourcebutassumethateverythingfits LLMstofine-grainedsemantictaskswheretheyarereliable.
inthemodel’scontextwindow,anassumptionviolatedbylarge Insummary,we(1)identifyseveralclaimtypesthatariseinse-
relations. Retrieval-augmented LLM approaches [41, 77, 80, 83] manticaggregatesandmapthemtowell-definedlogicalstructures
scaletolargercorporabyretrievingrelevantevidence,butthey (Section2);(2)showhowsuchclaimscanbeexpressedasdeclarative
targetclaimsverifiedbyconnectingdependentsourcesratherthan semanticverificationqueries(Section3);(3)introduceoptimizations
quantifiedclaimsoverindependenttuples,andtheirnaturallan- tailoredtoverificationandintegratethemwithgeneral-purpose
guagereasoningaboutquantifiersandgroupingsiscostlierand optimizationsforsemanticqueries(Section4);(4)buildonsemir-
lessreliablethandedicatedsymbolicoperations.Program-based ingprovenanceforfirst-orderlogic[31]toformalizecitationsas
LLMmethods[34,58,87]cangenerateimperativeprogramsthat dataprovenance,derivingaminimalexplanationforeachverdict
combinesymbolicandsemanticprocessing;however,theypush (Section5);and(5)evaluateEvergreenonabenchmarkreflect-
theresponsibilityofoptimizationandcitationcaptureontothe ingreal-worldsemanticaggregationworkloadstodemonstrateits
LLM,resultinginpotentiallysuboptimalorerror-proneimplemen- dominanceinverificationqualityandcost(Section6).
tations.Inthedatabasecommunity,query-basedverificationsys-
tems[15,35,37,40,73,74]translateclaimsintodeclarativequeries
2 CLAIMSOVERRELATIONS
overstructureddata,butcannothandleclaimsthatrequireseman-
ticevaluation.Meanwhile,semanticqueryprocessingenginesare Semanticaggregatesimplicitlyencodeacollectionofclaims,i.e.,
capableofexpressingsuchverificationlogic.Yet,existingsystems naturallanguageassertionsabouttheunderlyingrelation.Tover-
lackverification-awareoptimizationsandexplanations.Mostrele- ifytheseclaims,Evergreenfirstmakesthemexplicitviaaclaim
vanttousisanearlyframeworkcalledBinder[18],whichnaively decompositionprocessthatinvokesanLLMtobreakdowneach
processesalltupleswithanLLMandwasonlyevaluatedonaclaim sentenceinthesemanticaggregateintoalistofclaims[80].Since
verificationbenchmarklimitedtosmallstructuredtables[17]. theresultingclaimsmaycontainvaguereferences(e.g.,pronouns,
WepresentEvergreen,asystemthatreliablyandefficientlyver- unknownentities),theprocessinvokesanLLMagainforeachclaim
ifiesclaimsfromsemanticaggregatesbytreatingclaimverification toresolvethereferencesusingtheoriginalresponseascontext.
asasemanticqueryprocessingproblemwithprincipledoptimiza- Fromouranalysisofclaimsgeneratedbyproductionsemantic
tionsandprovenancecapture.Inparticular,Evergreencompiles aggregationworkloadsatSnowflake,weidentifyseveralcommon
eachclaimintoadeclarativesemanticverificationquerycomposed claimtypesthatmaptofamiliarlogicalstructures.Wefirstformalize
ofstandardrelationaloperatorsandsemanticoperators,shifting ourclaimlanguageandthendescribeeachclaimtype.
theburdenofoptimizationandcitationcaptureawayfromtheLLM LetRbearelation,whichservesasthefixed,finitedomainof
andontothequeryengine.Crucially,Evergreencanreusethe ourlogic.Rmaybeafilteredsubsetofthebaserelationrelevantto
samequeryenginethatproducedthesemanticaggregate,requiring theclaim’sscope(e.g.,reviewsforaspecificrestaurantorreviews
noseparateverificationinfrastructure.Itsefficiencystemsfrom fromvegetariancustomers).Thatis,tuplesnotinRarenotrelevant
twocomplementaryclassesofoptimizations.First,Evergreenin- totheclaim.Let𝜑beaquantifier-freeformulawithafreevariable
troducesverification-awareoptimizations—includingearlystopping, rangingovertuples𝑡 ∈R(i.e.,aunaryquery),mappingeachtuple
relevancesorting,andestimationwithanytime-validconfidence totrueifitsatisfiestheformula(i.e.,𝜑(𝑡) =⊤)orfalseifitdoes
sequences[22,79]—thatexploitthestructureofverificationqueries not(i.e.,𝜑(𝑡)=⊥).𝜑maybebuiltfromsymbolicpredicates(e.g.,
tominimizetheamountofevidencethatmustbeexamined.These whetherthetuple’sageattributeisgreaterthan21)andsemantic
techniquesarespecifictoverificationqueriesandconstituteour predicates(e.g.,whetherthetuple’stextattributementionsvegan
primarytechnicalcontributions.Second,Evergreenincorporates options)usingconjunction,disjunction,andnegation.
general-purposeoptimizationsforsemanticqueries,suchasoperator Existentialclaimsusetheexistentialquantifiertoassertthat
fusion,similarityfiltering,andpromptcaching.Finally,Evergreen atleastonetuplesatisfies𝜑,i.e.,∃𝑡 ∈R :𝜑(𝑡).Forexample,“Some
accompanieseachverdictwithcitations—aminimalexplanation reviewersenjoytherestaurant’schickensalad”isexistential.
of why a claim holds or why not—formalized by applying and Universalclaimsusetheuniversalquantifiertoassertthatall
extendingsemiringprovenanceforfirst-orderlogic[31]. tuplessatisfy𝜑,i.e.,∀𝑡 ∈ R :𝜑(𝑡).Forexample,“Thereviewsdo
notmentionanyveganoptions”isuniversal.
17
Cardinal claims use cardinal quantifiers to assert the num- filter(predicate)selectstuplesthatsatisfythebooleanex-
𝜑, ∃ 𝑡 ∈ R 𝜑(𝑡), pressionpredicate.Inverificationqueries,filtersaregenerally
| ber of | tuples that | satisfy | such | as ≥𝑘 | | : where | | | | | |
| ------ | ----------- | ------- | ---- | ----- | --- | ------- | --- | --- | --- | --- | --- |
𝑘 {0,1,...,|R|}.
∈ For example, “At least a handful of vegetar- usedtorestrictR totuplesrelevanttotheclaim.Inadditionto
iancustomersenjoyedtherestaurant’sburgers”isacardinalclaim. symbolicexpressionsforstructuredfiltering,Evergreenfeatures
Variantsofcardinalquantifiersinclude∃>𝑘,∃ ≤𝑘,∃<𝑘,∃ =𝑘,and∃ ≠𝑘. promptexpressionsforsemanticfiltering:prompt(prompt_str,
BecauseRisfixedandfinite,cardinalquantifiersgeneralizeexis- return_type=bool).ThepromptexpressionusesanLLMtoeval-
tentialanduniversalquantifierswith∃ and∃ uateasemanticpredicatespecifiedbyapromptstringprompt_str
≥1 =|R|,respectively.
Proportionalclaimsuseproportionalquantifierstoassertthe
thatcanreferencetupleattributesbyname.
| proportionoftuplesthatsatisfy𝜑,suchas∃ | | | | | 𝑡 | :𝜑(𝑡),where | | | | | |
| -------------------------------------- | ---------- | -------- | --------------- | --- | ------------ | ----------- | --------------------- | --- | --------------- | ---------------- | ---------- |
| | | | | | ≥𝜌 ∈R | | df.filter(prompt("The | | {text} mentions | the restaurant's | service")) |
| 𝜌 ∈ | [0,1]. For | example, | “The restaurant | | has received | majority | | | | | |
positivereviews”isaproportionalclaim.Variantsofproportional map(expr)computesanewattributeforeachtuplebyevaluating
e x p r 𝜑
q u a n tifi e rs in c l ud e ∃ ,∃ , ∃ 𝜌, ∃ , a n d ∃ 𝜌. Pr o po rt i onalquan- t o m a te r i al iz e a t t ri b u t es r e q u i r e d by th e cl a i m ’ s f o r m u la
| | | > 𝜌 | ≤ 𝜌 < | =𝜌 | ≠ | | | | | | |
| ---------- | ------------- | ----------- | ---------------- | ---------- | --------- | -------- | ------------ | ---------- | ---------------------- | ------------------------- | --------------------------- |
| | | | | | 𝜌 | | th a t a r e | no t y e t | p re s e n t i n t h e | r e la t i o n .A sw i th | fi l t er s , e x p r m a y |
| ti fi e rs | re d uc e t o | c ar d in a | lq u a n t ifi e | rs b y s c | al in g b | y |R | . | | | | | |
Ordinalclaimsassertthatagroupoftuplesachievesaparticular beasymbolicorpromptexpression,thoughpromptexpressions
herecanalsoreturnnon-booleantypes.
| rankwithrespecttoaper-groupaggregate.Let𝐺 | | | | | | ,...,𝐺 𝑚 ⊆ R | | | | | |
| ----------------------------------------- | --- | --- | --- | --- | --- | ------------ | --- | --- | --- | --- | --- |
1
| be groups | of tuples | induced | by | partitioning | the | tuples in R by | df.map( | | | | |
| --------- | --------- | ------- | --- | ------------ | --- | -------------- | ------- | --- | --- | --- | --- |
oneormoreattributevalues,andlet𝑓(𝐺 ,𝜑)denoteaper-group prompt("Identify the {text}'s sentiment", Sentiment).alias("sent")
| | | | | | 𝑗 | | ) | | | | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
aggregate(i.e.,thecountorproportionoftuplesin𝐺
𝑗 satisfying
𝜑).Giventheset𝑉(𝜑):={𝑓(𝐺 ,𝜑),...,𝑓(𝐺 ,𝜑)}ofdistinctper- aggregate(agg_exprs, group_by=())aggregatesovertuples
| | | | 1 | | 𝑚 | | | | | | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
groupaggregates,therankofgroup𝐺 𝑖 is byevaluatingthesequenceofaggregationfunctionexpressions
agg_exprs,optionallygroupedbyasequenceofgroupingexpres-
| | rank(𝐺 | ,𝜑):=|{𝑣 | ∈𝑉(𝜑):𝑣 | > | 𝑓(𝐺 ,𝜑)}|+1. | | | | | | |
| --- | ------ | -------- | ------- | --- | ------------ | --- | --- | --- | --- | --- | --- |
𝑖 𝑖 sions group_by. Aggregation functions are closely related to a
Anordinalclaimassertsrank(𝐺 ,𝜑)=𝑟 forsometargetgroup𝐺 claim’squantifiers,andanaggregationfunction’sexpressionexpr
| | | | 𝑖 | | | 𝑖 | | | | | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
andrank𝑟.Forexample,“Thetop-rankedMcDonald’slocationin correspondstotheclaim’sformula𝜑.bool_or(expr)corresponds
totheexistentialquantifier,whilebool_and(expr)corresponds
termsofservicehastheBusinessID[A]”isanordinalclaim.
Nestedclaimscomposethepriorclaimtypesatmultipledepths totheuniversalquantifier.count_if(expr)evaluatestothenum-
ofgrouping.LetQ:={∃,∀,∃𝜃𝑘 ,∃𝜃𝜌}denotethefullsetofquanti- beroftuplessatisfyingexpr,andwhentheresultingaggregateis
fiersintroducedearlierwith𝜃 ∈{≥,>,≤,<,=,≠}.Givenapartition pairedwithacomparisonexpressioninasubsequentoperator,it
ofgroupsG:={𝐺 ,...,𝐺 𝑚}asbefore,anestedclaimofdepthtwo correspondstoacardinalquantifier.Similarly,proportion(expr)
1
specifiesanouterquantifier𝑄 Qovergroups𝐺 evaluatestotheproportionoftuplessatisfyingexprandcorre-
| | | | out | ∈ | | ∈ Gandan | | | | | |
| ---------------- | --- | ------------- | --- | --- | --- | -------- | -------------------------------------------------------- | --- | --- | --- | --- |
| innerquantifier𝑄 | | ∈Qovertuples𝑡 | | ∈𝐺: | | | | | | | |
| | | in | | | | | spondstoaproportionalquantifierwhenpairedwithacomparison | | | | |
expression.exprcansimplybeareferencecol(name)toaboolean
| | | 𝑄 𝐺 | ∈G:(𝑄 | 𝑡 ∈𝐺 | :𝜑(𝑡)). | | | | | | |
| --- | --- | --- | ----- | ---- | ------- | --- | --- | --- | --- | --- | --- |
out in attributeoranexpressionoverattributesthatevaluatestoaboolean.
Forexample,“AllMcDonald’slocationshavemultiplecomplaints
df.aggregate(
aboutpoorservicequality”is∀𝐺 ∈G:(∃ 𝑡 ∈𝐺 :𝜑(𝑡)),where𝐺 [proportion(col("sent").eq(Sentiment.POSITIVE)).alias("pos_prop")]
≥2
| isagroupoftuplesforalocationand𝜑istheformulaforwhether | | | | | | | ) | | | | |
| ------------------------------------------------------ | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
atuplecomplainsabouttherestaurant’spoorservice.Nestingcan Groupingisusedforordinalandnestedclaimstocomputegroup
extendtoarbitrarydepths,thoughdeepernestingisrareinpractice. aggregatesbeforesubsequentrankingorouteraggregationsteps.
3 CLAIMSASQUERIES with_rank(expr, descending=True)createsadenserankat-
tributecol("rank")foreachtuplebasedontheexpressionexpr,
Basedonthelogicalstructureofclaims,EvergreenusesanLLMto indescendingorderbydefault.Thisoperatorisusedforordinal
compilenaturallanguageclaimsintosemanticverificationqueries claims,determiningeachgroup’srankafterper-groupaggregation.
composedofstandardrelationaloperatorsandsemanticoperators. check(predicate) is the terminal operator of a verification
query.Itevaluatesthebooleanexpressionpredicateonthe(typ-
Akintotraditionaldatabasequerylanguages,theseverification
queriesaredeclarative,enablingtheLLMtofocusonspecifying icallyaggregated)resultandaddsitasanewbooleanattribute
what toverifyratherthanhow toverifyit.Thisshiftslow-level representing the claim’s verdict. The verdict is annotated with
responsibilitiessuchasoptimizationandprovenancecaptureaway provenanceinformationthatexplainswhytheverdictistrueor
fromtheLLMandontothequeryengine,improvingreliabilityand false,whichwedescribemoreinSection5.
End-to-EndExamples.Figure2showstheverificationqueryfor
efficiency.Moreover,verificationrequiresnoseparateinfrastruc-
ture:thesamequeryenginethatproducedthesemanticaggregate thenestedclaimfromSection2.Thequeryfirstusesasemantic
canalsoverifyclaimsextractedfromit. map()toevaluate𝜑oneachtuple,labelingwhetherareviewcom-
QueryInterface.EvergreenprovidesaDataFrameAPIinPython, plainsabouttherestaurant’spoorservice.Thefirstaggregate()
whereaDataFramedfrepresentsarelationR.Queriesarecom- groupstuplesbylocation(business_id)andappliescount_if()
tocountcomplaintspergroupfortheinnercardinalquantifier∃
posed by chaining operators parameterized by expressions and ≥2 .
thenoptimizedandexecutedusingcollect().Wedetailthecore Thesecondaggregate()appliesbool_and()toverifythatevery
operatorsandtheirrelevantexpressions,highlightinghowthey group’scomplaintcountmeetsthethreshold,implementingthe
correspondtothelogicalstructureofclaims.
18
df.map( bool_or(expr)stopsaggregatingafterencounteringawitness
prompt( (i.e.,atuplethatsatisfiesexpr),whilebool_and(expr)stopsafter
"Identify whether the {text} complains about "
"the restaurant's poor service", bool encounteringacounterexample(i.e.,atuplethatdoesnotsatisfy
).alias("service_complaint") expr).Forcount_if(expr)andproportion(expr),thequeryop-
)
.aggregate( timizer extracts the relevant comparison expressions from sub-
[count_if(col("service_complaint")).alias("complaint_count")], sequent operators (e.g., check(col("pos_prop") > 0.5)) and
group_by=[col("business_id")] pushesthemdowntothecorrespondingaggregateoperatorsas
)
.aggregate( earlystoppinghints.Giventhesehints,anaccumulatorstopsas
[bool_and(col("complaint_count") >= 2).alias("all_mul_complaints")] soonasthecomparisonissettled:eitheritsrunningcount𝑐already
) determinestheoutcome,or,whenthetotalnumber𝑛ofinputtu-
.check(col("all_mul_complaints"))
.collect() plesisknown,theresultcannotchangeregardlessofwhetherthe
remainingtuplessatisfyexpr.Foranungrouped aggregate,𝑛 is
determinedbyacardinalityscanoperatorthatcountsthetuples
Figure2:Verificationqueryforthenestedclaim“AllMcDon-
priortoLLMevaluation.Whilescanningisconsideredexpensivein
ald’slocationshavemultiplecomplaintsaboutpoorservice
traditionalqueryprocessing,itiseffectivelyfreewhencompared
quality”(∀𝐺 ∈G:(∃ ≥2 𝑡 ∈𝐺 :𝜑(𝑡))). toLLMevaluation.Foragroupedaggregate,𝑛isaper-groupcount
computedduringthesortingphasedescribednext.
df.filter(prompt("The {text} mentions the restaurant's service")) Forgroupedaggregates,Evergreenavoidsusinghash-based
.map( aggregatessincetheyrequirepullingalltuplesthroughthesemantic
prompt(
"Identify whether the {text} praises the restaurant's service", operators,whichdefeatsthepurposeofearlystopping.Evergreen
bool insteadusesstreamingaggregates,processinggroupssequentially
).alias("praises_service")
oversorted,group-contiguousinput.Whilestreamingaggregates
)
.aggregate( are classically only used when input tuples are already sorted,
[proportion(col("praises_service")).alias("service_praise_prop")], sorting(similartoscans)ischeapinoursetting.Theoptimizer
group_by=[col("business_id")]
insertsasortoperatoraslowinthequeryplanaspossibletoensure
)
.with_rank(col("service_praise_prop")) thattuplesbelongingtothesamegroupareaggregatedtogether
.filter(col("business_id").eq("[A]")) whileavoidingunnecessarysemanticoperatorevaluations.Once
.check(col("rank").eq(1))
.collect() agroup’saggregateisresolved,alloperatorsbelowtheaggregate
skiptheremainingtuplesbelongingtothatgroup.
Itisuncommonfortraditionalqueryenginestopushcomparison
Figure3:Verificationqueryfortheordinalclaim“Thetop-
expressionsintoaggregates.Thisoptimizationis,however,remi-
rankedMcDonald’slocationintermsofservicehastheBusi-
niscentofpriorresearchinad-hocsensornetworksthatpushes
nessID[A]”(rank(𝐺 𝑖 ,𝜑)=1). HAVINGpredicatesintogrouped monotonicaggregatestoreduce
transmissionandstorageofgroupsthatdonotsatisfythepredi-
cate[52].There,asinoursetting,per-tupleprocessingisrelatively
outeruniversalquantifier∀.Finally,check()evaluatestheverdict.
expensive.Yet,unlikethispriorwork,Evergreenpushesthese
Figure3showsasecondexamplewithanordinalclaim.Thequery
comparisonsdowntoconfirmorrefutethemasearlyaspossiblefor
additionallyusesasemanticfilter()torestricttoservice-related
bothungroupedandgroupedaggregates.Wefurtheramplifythe
reviewsandwith_rank()todetermineeachlocation’srank.
benefitsofthisapproachwiththenexttwooptimizations.
4 QUERYOPTIMIZATIONS
RelevanceSorting.Earlystoppingismosteffectivewhenrelevant
tuples—thosethatcontributetotheaggregate’sverdict—appear
Thebottleneckofsemanticverificationqueriesliesintheirsemantic earlyintheinputstream.Sincetuplesareprocessedinarbitrary
operators,whichrequireinvokingexpensiveLLMs.Evergreen orderbydefault,theserelevanttuplesmaynotsurfaceuntillater.
introducesverification-awareoptimizationsandcombinesthem Evergreenencouragesstoppingbypre-sortingtuplesbyrelevance.
withgeneral-purposeoptimizationsforsemanticqueriestoreduce Atoptimizationtime,theoptimizerconstructsadescriptionof
costwhilemaintainingreliability. theaggregatetoscoreeachtuple’srelevance.Itfirsttracestheat-
tributereferencedbytheaggregateexpressionbacktothesemantic
4.1 Verification-AwareOptimizations
mapthatproducedit,collectingthemap’spromptexpressionand
EarlyStopping.Computingfullaggregationsoveralltuplesisnot anyfilterpromptsthatreferencethesametextattribute.These
requiredformanyverificationqueries,sincetheaggregatesinour promptsprovidecontextforwhattheaggregateisaccumulating
settingaremonotoneinthenumberofsatisfyingtuples.Assuch, over(i.e.,thescopeoftheclaim’srelationRandtheclaim’sformula
Evergreenexecutesqueriesusingtheiteratormodel—whereoper- 𝜑).Thedescriptionalsoincludestheaggregateexpressionitself
atorslazilypulltuplesfromtheirchildren—andstopsaggregating and,whenapplicable,itscomparisonexpression;together,they
earlysothatonlynecessarytuplesarepulledthroughthesemantic expresstheclaim’squantifier.TheoptimizerthenpromptsanLLM
operatorsthatappearbeforetheaggregation.Table1summarizes withthisdescriptiontogenerateasemanticsearchquery,asetof
theconditionsunderwhicheachaggregatestopsdeterministically inclusionkeywordslikelytoappearinrelevanttuples,andasetof
andprobabilistically,andwenowdescribehowtheyarerealized. exclusionkeywordsthatshouldnotappearinthem.Atexecution
19
Table1:Deterministicandprobabilisticstoppingconditions
aspossiblewithoutcommittingtoasamplesizethatmaybetoo
toconfirm/refuteaclaim.Afterobserving𝑠of𝑛tupleswith
smalltobeconclusiveortoolargetobecost-effective.
| 𝑐satisfyingexpr,thefinalcountisin[𝑐,𝑐+(𝑛−𝑠)].[𝐿 | | | | | ,𝑈 𝑠]is | | | | | | | | |
| ----------------------------------------------- | --- | --- | --- | --- | ------- | --- | ----------------------------------------------------- | --- | --- | --- | --- | --- | --- |
| | | | | | 𝑠 | | Ingeneral,acomparisonresolvesoncetheentireCIliesonone | | | | | | |
theproportionCIand𝜀theerrortolerance.“—”marksaprob-
sideofthethresholdorwithinatoleranceinterval(Table1).For
abilisticconditionsubsumedbythedeterministicone.∃>𝑘
| | | | | | | proportion(),EvergreencomparestheproportionCI[𝐿 | | | | | | | 𝑠 ,𝑈 𝑠]di- |
| ------------ | --- | ---- | -------- | ------------------ | --- | ----------------------------------------------- | --- | --- | --- | --- | --- | --- | ---------- |
| followsfrom∃ | | .∃<𝑘 | ,∃ ,and∃ | swapconfirm/refute | | | | | | | | | |
≥𝑘+1 ≤𝑘 ≠𝑘 rectlyagainst𝜌;forcount_if(),itfirstscalestheproportionCIby
of∃ ≥𝑘 ,∃>𝑘 ,and∃ =𝑘 ,respectively.Proportionalquantifiers thetotalnumber𝑛ofinputtuplestoobtainthecountCI[𝑛𝐿 ,𝑛𝑈 𝑠]
𝑠
replacecountswithproportionsand𝑘with𝜌. andcomparesagainst𝑘.Equalitycomparisonsadditionallyusea
| | | | | | | configurablerelativeerrortolerance𝜀 | | | | | (0,1).Forbool_and(), | | |
| --- | --- | --- | --- | --- | --- | ----------------------------------- | --- | --- | --- | --- | -------------------- | --- | --- |
∈
Deterministic Probabilistic theaccumulatorcheckswhether𝜇=1usingtheequalitycondition
| | | | | | | with𝜌 | =1,whichreducesto | | | [𝐿 ,𝑈 𝑠] | ⊆ [1−𝜀,1],andtherefore | | |
| --- | ------- | --------- | ------- | --- | ------ | ----- | ----------------- | -------------------------------------------- | --- | -------- | ---------------------- | --- | --- |
| | Confirm | Refute | Confirm | | Refute | | | | | 𝑠 | | | |
| | | | | | | 𝐿 | ≥ 1−𝜀 | since𝑈 ≤ 1byconstruction.Forbool_or(),sincea | | | | | |
| ∃ | 𝑐≥1 | 𝑐+(𝑛−𝑠)<1 | — | | 𝑛𝑈𝑠<1 | 𝑠 | | 𝑠 | | | | | |
∀ 𝑐=𝑛 𝑐<𝑠 𝐿𝑠 ≥1−𝜀 — witnessalreadytriggersdeterministicstopping,thescaledcountCI
| | | | | | | servesmainlytodetectthatnosatisfyingtupleexists,i.e.,𝑛𝑈 | | | | | | | <1. |
| --- | --- | --------- | ------ | --- | ----- | ------------------------------------------------------- | --- | --- | --- | --- | --- | --- | --- |
| ∃≥𝑘 | 𝑐≥𝑘 | 𝑐+(𝑛−𝑠)<𝑘 | 𝑛𝐿𝑠 ≥𝑘 | | 𝑛𝑈𝑠<𝑘 | | | | | | | | 𝑠 |
Whenthetotalnumber𝑛ofinputtuplesisknown,weusesampling
| ∃=𝑘 | 𝑐=𝑘∧ | 𝑐>𝑘∨ | [𝑛𝐿𝑠,𝑛𝑈𝑠]⊆ | | [𝑛𝐿𝑠,𝑛𝑈𝑠]∩ | | | | | | | | |
| --- | ---- | ---- | ---------- | --- | ---------- | --- | --- | --- | --- | --- | --- | --- | --- |
𝑠=𝑛 𝑐+(𝑛−𝑠)<𝑘 [𝑘(1−𝜀),𝑘(1+𝜀)] [𝑘(1−𝜀),𝑘(1+𝜀)]=∅ withoutreplacementtoyieldtighterCIs.EvergreencomputesCSs
viathebettingapproachofWaudby-SmithandRamdas[79].
SinceCSsrequirethatobservationsarriveinexchangeable(i.e.,
uniformlyrandom)order,theoptimizerinsertsashuffleoperator
time,eachtupleisscoredusingthreerankingsignals:cosinesimi-
whenestimationisused.Forungroupedaggregates,theshuffleis
laritybetweenthetuple’stextembeddingandthesearchquery’s
placedabovethetablescan,randomizingalltuples.Forgrouped
embedding,thenumberofinclusionkeywordspresent,andthe
aggregates,theshuffleisinsertedabovethesortoperatorusedfor
numberofexclusionkeywordsabsent.Eachtuple’stextembedding
iscomputedduringingestionandreusedacrossqueries.Signals groupingandhierarchicallyrandomizesateachlevel:groupsare
shuffledascontiguousblocks,andtupleswithinthefinestgroups
arecombinedviaReciprocalRankFusion[19](withthestandard
canalsobeshuffledifestimationisusedatthataggregatelevel,
| constant | 60), | and tuples | are fed to the | aggregate | in descending | | | | | | | | |
| -------- | ---- | ---------- | -------------- | --------- | ------------- | --- | --- | --- | --- | --- | --- | --- | --- |
preservinggroupcontiguityforthestreamingaggregate.
relevanceorder.Therelevancesortoperatorisplacedabovethe
Whenmultipleestimationdecisionsoccurinthesamequery,Ev-
tablescansothatreorderingoccursbeforeanyLLMcall.Thisop-
timizationissimilartoatop-koperationininformationretrieval, ergreencontrolsthefamily-wiseerrorrate:theprobabilityofany
CIfailingtocontainitstrueproportionmustnotexceed𝛼.Theerror
butallowsthequeryenginetopotentiallyprocessalltuplesinthe
budgetisdividedintwostages.First,foraquerywith𝑜aggregate
relationwithoutenforcingasetlimit.Again,computingrelevance
operatorsthatuseestimation,thebudgetissplitequally,allocating
scoresandsortingareinexpensivecomparedtoLLMevaluation.
| | | | | | | asignificancelevelof𝛼/𝑜 | | | toeachoperator.Second,withineach | | | | |
| --- | --- | --- | --- | --- | --- | ----------------------- | --- | --- | -------------------------------- | --- | --- | --- | --- |
EstimationwithConfidenceSequences.Inadditiontodeter-
operator,thebudgetisdividedacrossits𝑎estimatingaccumulators
ministicearlystopping,Evergreenusesstatisticalestimationto
andthe𝑚groupsintheinputstream.Whenthenumberofgroups
resolvecertaincomparisons.Ourapproachissimilartoearlywork 𝑚isknowninadvancefromasortoperator,Evergreenapplies
ononlineaggregation[33],whichusesclassicalconfidenceinter-
aBonferronicorrection,assigningeachaccumulatoraper-group
vals(CIs).However,usingCIsforonlineaggregationsuffersfrom
significancelevelof𝛼/(𝑜·𝑎·𝑚).When𝑚isnotknowninadvance,
the“peekingproblem”[38],wherecontinuouslymonitoringthe
Evergreenallocatesageometricallydecreasingsharetoeachsuc-
CIinflatestheerrorrate.Toavoidthisissue,weinsteadleverage
cessivegroup:eachaccumulator’s𝑖-thgroupreceivesasignificance
| recentworkonconfidencesequences(CSs)[79]. | | | | | | | 𝛼 | 𝑜 𝑎 𝑖 | ∑︁ | ∞ | 𝑖 | | |
| ----------------------------------------- | --- | --- | --- | --- | --- | --- | --- | ----- | --- | --- | --- | --- | --- |
𝑍 l e v e l o f / ( · · 2 ) . B e c a u s e 𝑖 1 / 2 = 1 , t h e t o t a l e r ro r b u d g e t
M o r e f o rm a l l y ,l e t ( 𝑠 ) 𝑠 ≥ 1 b e a s e q u e n c e o f B e r n o u ll i r a n d o m = 1
| | | | | | | n e | v e r e x c e e | d s 𝛼 r e g a r d l | e s s o f th | e n u m | b e r o f g | r o u p s . | |
| ------- | ------------ | ------------------- | ----------------------- | ---------------- | --------------------------------- | --- | ----------------- | ------------------- | ------------ | ------------ | ----------- | ------------ | ------------------- |
| v a r i | a b le s , w | h e r e 𝑍 𝑠 = 1 | i f t h e 𝑠 - t h t u | p le s a t is fi | e s t h e a g g r e g a t i o n | | | | | | | | |
| | | | | | | I n | t e r a c t i o n | B e t w e e n S | o r t i n g | a n d E s t | im a t i o | n . R e le v | a n ce s o r ti n g |
| fu n c | t io n ’ s b | o o l e a n e x p r | e s s i o n e x p r a n | d 𝑍 𝑠 = 0 | o t h e r w i s e . F u r t h e r | | | | | | | | |
| | | | | | | and | estimation | impose | conflicting | requirements | | on | tuple order. |
let𝜇 ∈ [0,1]denotethetrueproportionoftuplessatisfyingexpr
inanaccumulator’sinputstream.Theaccumulatorestimates 𝜇 Relevancesortingarrangestuplestoacceleratedeterministicearly
withananytime-valid(1−𝛼)-confidencesequence:asequenceof stopping, while estimation requires exchangeable order for the
confidenceintervals([𝐿 ,𝑈 CS guarantee. The optimizer thus applies at most one strategy
| | | | 𝑠 𝑠])𝑠≥1 thatsatisfies | | | | | | | | | | |
| --- | --- | --- | ---------------------- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
peraggregateoperator.Thechoiceisguidedbyaheuristicthat
Pr(∀𝑠 ≥1:𝜇 [𝐿 ,𝑈 𝑠])≥1−𝛼, assumesclaimsarelikelytrue,whichweexpecttoholdincreasingly
∈ 𝑠
asLLMsimprove.Underthisassumption,thedecidingquestion
| where[𝐿 | ,𝑈 | [0,1]forall𝑠 | ≥1and𝛼 | (0,1)isaconfigurable | | | | | | | | | |
| ------- | --- | ------------ | ------ | -------------------- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
𝑠 𝑠] ⊆ ∈ iswhetherafewsatisfyingtuplessufficetoconfirmtheclaim:if
significancelevel.Equivalently,1−𝛼istheconfidencelevel.Because so,relevancesortingsurfacesthemearly;otherwise,theoptimizer
theprecedingguaranteeholdssimultaneouslyforallsamplesizes usesestimation.Relevancesortingthereforeappliesto∃,∃ ≥𝑘,and
𝑠,theaccumulatorcancheck[𝐿 ,𝑈 𝑠]aftereachobservedtupleand ∃>𝑘 claimswithsmall𝑘;estimationisunhelpfulhere,sincetight
𝑠
stopassoonastheverdictisclear,withoutrepeatedchecksinflating CIsrequireobservingmoretuples.Theoptimizerusesestimation
theerrorrateabove𝛼.AclassicalCI,bycontrast,isvalidonlyat
forallothercases,wheresurfacingsatisfyingtuplesearlydoes
asingle,predeterminedsamplesize,socontinuouslymonitoring not accelerate confirmation. A true universal claim has 𝜇 = 1,
itisunsound.CSsenableEvergreentostopconfidentlyasearly whichestimationconfirmsfromasamplewithoutprocessingevery
20
tablescan relevancesort (busi s n o e r s t s_id) (bu s s h i u n f e f s l s e _id) map (bu c s o i u n n e t s _ s i _ f id) bool_and check
searchquery: prompt: stopconditions: stopconditions:
“...poorservice...”, “Identifywhetherthe 𝑐 ≥ 2or 𝐿𝑠 ≥ 1−𝜀or
incl:“terrible”,... {text}complains...” 𝑐+(𝑛−𝑠) <2 𝑐 =𝑛or𝑐 <𝑠
Figure4:OptimizedqueryplanfortheverificationqueryinFigure2.
tuple.For∃ ≥𝑘 and∃>𝑘 claimswithlarge𝑘,sortingdoesnotpay forcount_if(),and(3)tighterCIsviasamplingwithoutreplace-
offbecausetoomanysatisfyingtuplesareneeded.∃ ≤𝑘,∃<𝑘,and ment.Insuchcases,theoptimizerfallsbacktootheroptimizations
∃ =𝑘 claimsrequireboundingthetotalnumberofsatisfyingtuples, thatdonotrequireknowing𝑛.Forinstance,theinabilitytoscale
whichentailsprocessingnearlyalltuplesregardlessoforder.A theCIpreventsestimationfor∃ ≥𝑘 and∃>𝑘 cardinalclaims,sothe
true∃ ≠𝑘 claim’scountmaylieaboveorbelow𝑘;relevancesorting optimizerappliesrelevancesortingregardlessofthethreshold𝑘.
acceleratesonlytheformerbysurfacing𝑘 +1satisfyingtuples, Eventhoughthestoppingconditionsthatrequire𝑛areunavailable,
whereasestimationcanstopearlyineithercase.Forproportional operatorfusionstillreducesthetotalnumberofLLMcalls.
claims, the optimizer cannot determine whether the equivalent FusingmultiplepromptsintoasingleLLMcallmayreduceout-
countthreshold𝑛𝜌 issmall,since𝑛isunknownatoptimization putquality.Yet,basedonourobservations,verificationqueries
time. In queries with nested aggregates, the two strategies can usuallyrequireonlyafewnarrowlyscopedsemanticoperators.
coexistatdifferentlevels:theinneraggregateusesrelevancesorting GiventhecurrentcapabilitiesofLLMs,fusionthusreducesthe
withineachgroup,whiletheouteraggregateusesestimationwith numberofLLMcallswithminimalqualitydegradation.
groupordershuffled.Wenotethatthisbiastowardtrueclaims SimilarityFiltering.SemanticfiltersinvokeanLLMonevery
canbackfire.Forexample,ifanexistentialclaimisfalse,relevance inputtuple,eventhoughmanymaynotsatisfythepredicate.Ever-
sortingcallsanLLMontheentirerelation,whileestimationwould greenavoidsthesecallsbyinsertingasimilaritypre-filterbelow
havebeenmoreefficient.Adaptivelyselectingbetweenrelevance eachsemanticfilter.Atoptimizationtime,theoptimizerreusesthe
sortingandestimationatruntimeisapromisingfuturedirection. sameLLM-drivenapproachasinrelevancesorting,generatinga
End-to-EndExample.WeillustratehowEvergreenoptimizes searchqueryfromthefilter’spromptandembeddingit.Atexe-
thequeryinFigure2,yieldingtheplaninFigure4.BeforeanyLLM cutiontime,thepre-filterdiscardsatupleifthemaximumcosine
call,theplanreorderstuples:arelevancesortsurfacesreviewslikely similaritybetweenthequeryembeddingandthetuple’ssentence-
tocomplainaboutpoorservicequality,andasortonbusiness_id levelembeddingsfallsbelowaconfigurablethreshold.Sentence-
makeseachlocation’sreviewscontiguoussocount_if()’sstream- levelembeddingsavoidthesignaldilutionofasingledocument
ingaggregatecanprocessonegroupatatime.Ashufflethenran- embedding,retainingatuplewhenevenoneofitssentencesis
domizesgrouporder—preservingwithin-grouprelevance—sothe relevant.Aconservativelylowthresholdkeepsrecallhighwhile
outerbool_and()’sCSobservesgroupsinexchangeableorder.The stilleliminatingtuplesclearlyunrelatedtothepredicate.
semanticmap()labelsonlythereviewspulledthrough.Thetwo PromptCaching.LLMresponsesarecachedondisk,keyedby
aggregatesapplydifferentstoppingconditionsfromTable1:the modelnameandpromptstring.Whenthesamepromptissentto
innercount_if()canonlystopdeterministically,whiletheouter amodel,thecachedresponseisreusedtoavoidredundantLLM
bool_and()canstopbothdeterministicallyandprobabilistically. evaluation.Thisbenefitsworkloadswheremultipleclaimsshare
semanticoperatorsoverthesameunderlyingdata.
End-to-EndExample.ThequeryinFigure3exercisesthegeneral-
4.2 General-PurposeOptimizations
purposeoptimizations.Asimilaritypre-filterdiscardsreviewsunre-
OperatorFusion.Averificationquerycancontainmultiplese-
latedtoservicebeforeLLMevaluation,andthesemanticfilter()
andmap()arefusedintoasingleLLMcallperreview.Unlikethe
manticoperators,e.g.,asemanticfilterfollowedbyasemanticmap,
queryinFigure2,rankingrequiresthefullproportion()ofeach
eachrequiringaseparateLLMcallpertuple.Evergreenreduces
location,sotheaggregatedoesnotstopearly;thesavingsinstead
thiscostbyfusingconsecutiveoperators,combiningtheirprompts
comefromissuingfewerLLMcallspertuple.Finally,whenrelated
into a single LLM call. If any filter evaluates to false, the fused
ordinalclaimsareverified(e.g.,whichlocationranksfirstvs.second
operatordiscardsthetuple;otherwise,itemitsthemapoutputs.
inservice),promptcachingreusesLLMresponsesacrossclaims.
Whenthefusedoperatorcontainsasemanticfilter,thecardinal-
ityscanoperator—whichprovidesanaggregatewiththenumber𝑛
5 CITATIONSASPROVENANCE
ofinputtuples—isnolongerused.Thisisbecauseneitherplacement
ofthecardinalityscanworks:placingitbelowthefusedoperator Returningabooleanverdictisofteninsufficientforusers;eachver-
yieldsapre-filtercountthatoverstatesthenumberoftuplesthe dictshouldbepairedwithacollectionofcitationssothatuserscan
aggregatewillobserve,whileplacingitaboveexecutesthefused checkitsunderlyingevidence.Bytreatingclaimsasqueries,Ever-
operator’sLLMoneverytuplebeforetheaggregatebegins(since greenformalizescitationsasdataprovenance,givingusersaprecise
itisapipelinebreaker),defeatingthepurposeofearlystopping. explanationoftheverdictbasedonfactsintherelation.Specifically,
Without𝑛,threecapabilitiesdescribedinSection4.1becomeun- wegroundourworkinsemiringprovenanceforfirst-orderlogic[31].
available:(1)deterministicboundsbasedonthemaximumachiev- Wefirstprovideashortoverviewofthisformalizationandthen
ablecountorproportion,(2)scalingtheproportionCItoacountCI describeitsapplicationandextensiontooursetting.
21
| | | | | | | | | Table 2: | Explanation | associated | | with each | claim’s | verdict. |
| --- | --- | --- | --- | --- | --- | --- | --- | -------- | ----------- | ---------- | --- | --------- | ------- | -------- |
5.1 SemiringProvenanceforFirst-OrderLogic
| | | | | | | | | 𝑊 ⊆Risasetoftuplessatisfying𝜑.∃>𝑘 | | | | | followsfrom∃ | ≥𝑘+1 . |
| --- | --- | --- | --- | --- | --- | --- | --- | --------------------------------- | --- | --- | --- | --- | ------------ | ------ |
Seminalworkonprovenancesemiringsforpositiverelationalal-
| | | | | | | | | ∃<𝑘 ,∃ | ,and∃ | swaptrue/falseexplanationsof∃ | | | | ,∃>𝑘 , |
| --- | --- | --- | --- | --- | --- | --- | --- | ------ | ----- | ----------------------------- | --- | --- | --- | ------ |
gebra[30]annotateseachoutputtuplewithapolynomialovera ≤𝑘 ≠𝑘 ≥𝑘
| | | | | | | | | and∃ ,respectively.Proportionalclaimsreducetothecar- | | | | | | |
| -------------------- | --- | ------------------------------------- | --- | --- | --- | --- | --- | ---------------------------------------------------- | --- | --- | --- | --- | --- | --- |
| setofindeterminates𝑋 | | inacommutativesemiring.Eachindetermi- | | | | | | =𝑘 | | | | | | |
dinalrows;ordinalandnestedclaimscomposetheserows.
nate𝑝 ∈𝑋,alsocalledaprovenancetoken,uniquelyannotatesan
𝑡
inputtuple𝑡
∈ R.Thesemiring’saddition(+)andmultiplication
(·)representthealternative(e.g.,union)andjoint(e.g.,join)useof ExplanationforTrue(⊤) ExplanationforFalse(⊥)
inputtuples,respectively.Consequently,eachmonomialinthepoly- ∃ 𝑝𝑡(firstwitness) ∏︁ 𝑡∈R 𝑝𝑡
| | | | | | | | | ∀ | ∏︁ 𝑝𝑡 | | | 𝑝𝑡(firstcounterexample) | | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | ----- | --- | --- | ----------------------- | --- | --- |
nomialisanalternativeexplanationofwhichinputtuplesjointly ∏︁ 𝑡∈R ∏︁ 𝑡∈𝑊𝑝𝑡∏︁
| | | | | | | | | ∃≥𝑘 | 𝑡∈𝑊𝑝𝑡,|𝑊|=𝑘 | | | | 𝑡′∈R\𝑊𝑝𝑡′,|𝑊|<𝑘 | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | -------------------------- | --- | --- | ---------- | --------------- | --- |
| | | | | | | | | ∃=𝑘 | ∏︁ 𝑡∈𝑊𝑝𝑡∏︁ 𝑡′∈R\𝑊𝑝𝑡′,|𝑊|=𝑘 | | | ∏︁ 𝑡∈𝑊𝑝𝑡∏︁ | 𝑡′∈R\𝑊𝑝𝑡′,|𝑊|≠𝑘 | |
contributetotheoutputtuple.GrädelandTannen[31]extendthis
frameworktofullfirst-orderlogicwithnegationbypairingeach
| indeterminate𝑝 | 𝑡 ∈𝑋 | (apositivetoken)withadualindeterminate | | | | | | | | | | | | |
| -------------- | ---- | -------------------------------------- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
𝑝 ∈ 𝑋 (anegativetoken).Inthissemiringofdual-indeterminate
| 𝑡 | | | | | | | | Whentheverdictisinsteadsettledbeforeacompletemonomial | | | | | | |
| --- | --- | --- | --- | --- | --- | --- | --- | ----------------------------------------------------- | --- | --- | --- | --- | --- | --- |
polynomials,additioncorrespondstodisjunctionandexistential isobserved(e.g.,estimationoverasample𝑆 ⊂Rordeterministic
quantification,whilemultiplicationcorrespondstoconjunctionand
universalquantification.Inoursetting,apositivetoken𝑝 earlystoppingfromamaximumachievablecountbound),there-
| | | | | | | | 𝑡 records | | | | | | | |
| --- | --- | --- | --- | --- | --- | --- | --------- | --- | --- | --- | --- | --- | --- | --- |
turnedtokensformasubsetofsuchaminimalmonomial.Table2
thepositivefactthattuple𝑡satisfies𝜑(i.e.,𝜑(𝑡)=⊤),whileanega-
summarizestheexplanationEvergreenreturnsforeachclaimtype
| tivetoken𝑝 | recordsthenegativefactthat𝑡 | | | | doesnotsatisfy𝜑(i.e., | | | | | | | | | |
| ------------------------- | --------------------------- | --- | ------------------------------- | --- | --------------------- | --- | --- | -------------------------------------------------- | --- | --- | --- | --- | --- | --- |
| | 𝑡 | | | | | | | andverdictincompletemonomialform,whichwenowderive. | | | | | | |
| 𝜑(𝑡)=⊥).Forexample,given𝜑 | | | :=“enjoystherestaurant’schicken | | | | | | | | | | | |
ExistentialandUniversalClaims.Foratrueexistentialclaim
| 𝑝 | | | 𝑡 | | | | | | | | | | | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
sa la d ”, 𝑡 r e c o r d s t h a t t u p l e e n jo y s th e r e s ta u r a n t ’ s c h i c k en s a la d , ∃ 𝑡 ∈ R 𝜑 ( 𝑡) ∑︁ 𝜋 ( 𝜑 ( 𝑡 ) )
𝑝 𝑡 ′ : , a p p l y i n g r u l e ( i ii ) y i e l d s 𝑡 ∈ R . E a c h tu -
w h il e 𝑡 ′ r e c o r d s t h a t a n o t h e r tu p l e do e s n o t e n j o y it . 𝑡 𝜋 𝜑 𝑡 𝑝 𝜑 𝑡
| | | | | | | | | p l e c on | t r ib u t es | ( ( ) ) | = 𝑡 t o t | h e p o ly | n o m i a l | i f ( ) = ⊤ |
| ------- | -------------- | --------------- | -------------- | ------- | --------- | -------------- | ------------ | ------------ | --------------- | ---------- | --------------- | ------------- | ----------- | -------------------- |
| M o r e | fo r m a ll y, | a n i n t e r p | r e ta t i o n | 𝜋 m a p | s e a c h | l i te r a l t | o a p o ly - | | | | | | | |
| | | | | | | | | an d 𝜋 ( 𝜑 ( | 𝑡 ) ) = 0 o t h | e rw i s e | . S i n c e E v | e r g r e e n | s t o p s | e a r l y a n d an y |
nomialandextendsinductivelytoallfirst-orderformulaswiththe
monomialsufficesasawitness,thereturnedprovenanceisthecor-
| fo ll o wi ng | r u le s ( a d | a pt e df ro | m D e fin | i ti on 2 | of [ 3 1 ]) : | ( i )𝜋 ⟦ 𝜓 | ∨ 𝜒⟧ := | | | | | | | |
| ------------- | -------------- | ------------ | --------- | --------- | ------------- | ---------- | ------- | ------------------------ | --- | --- | ----------------- | --- | --------- | --- |
| | | | | | | | | respondingpositivetoken𝑝 | | | forthefirsttuple𝑡 | | where𝜑(𝑡) | =⊤. |
| 𝜋 ⟦ 𝜓 ⟧ + | 𝜋 ⟦ 𝜒 ⟧ | 𝜋 ⟦ 𝜓 ∧ | 𝜒 ⟧ 𝜋 | ⟦ 𝜓 ⟧ ·𝜋 | ⟦ 𝜒 ⟧ | 𝜋 ⟦ ∃𝑡 | ∈ R | | | | 𝑡 | | | |
, ( ii ) : = , ( ii i ) : Forexample,giventheexistentialclaim“Somereviewersenjoythe
| 𝜓(𝑡)⟧:=∑︁ | 𝜋⟦𝜓(𝑡)⟧,(iv)𝜋⟦∀𝑡 | | | :𝜓(𝑡)⟧:=∏︁ | | | 𝜋⟦𝜓(𝑡)⟧, | | | | | | | |
| --------- | ---------------- | --- | --- | ---------- | --- | --- | -------- | --- | --- | --- | --- | --- | --- | --- |
𝑡∈R ∈ R 𝑡∈R restaurant’schickensalad”,if𝑡 isthefirsttuplethatsatisfies𝜑
:=
and(v)𝜋⟦¬𝜓⟧:=𝜋⟦nnf(¬𝜓)⟧,where𝜓 and𝜒 areformulasand “enjoystherestaurant’schickensalad”,thentheprovenanceis𝑝
𝑡.
| nnf(·) denotes | the | transformation | | to negation | normal | | form. In | | | | | | | |
| -------------------------- | --- | -------------- | ------------------- | ----------- | --------- | ---------- | -------- | ------------------- | ----------------- | ------ | ----------------- | ----------- | --------- | ------------- |
| | | | | | | | | For a | false existential | claim, | we | first apply | rule | (v) to inter- |
| oursetting,wetreateach𝜑(𝑡) | | | anditsnegation¬𝜑(𝑡) | | | asliterals | | | | | | | | |
| | | | | | | | | pret its negation∀𝑡 | | ∈ R | : ¬𝜑(𝑡). Applying | | rule (iv) | then gives |
| | 𝜑 | | | 𝜋 | ⟦𝜑 ( 𝑡 )⟧ | = 𝜋 ( 𝜑 | (𝑡 ) ) | | | | | | | |
re g a rd l e s s of ’s i n t e r n a l s t ru c t ure , so a n d ∏︁ 𝜋(¬𝜑(𝑡)) =∏︁ 𝑝 𝑡.Inthiscase,Evergreenreturnsthis
| 𝜋 𝜑 𝑡 | 𝜋 𝜑 | 𝑡 | | | | | | 𝑡∈R | | 𝑡∈R | | | | |
| ------- | ------ | ------------- | ---------- | ---------- | ---------- | --------- | ------------ | --- | --- | --- | --- | --- | --- | --- |
| ⟦ ¬ ( ) | ⟧ = (¬ | ( ) ) , w h i | c h fo r m | th e ba se | ca s e sfo | rt h e in | d u c ti v e | | | | | | | |
singlemonomialcontainingallnegativetokens,whichindicates
interpretation.Sincewewanttotrackbothpositiveandnegative thatnotupleinRsatisfies𝜑(e.g.,notupleenjoysthechickensalad).
| f a c ts , w e | s e t 𝜋 ( 𝜑 ( | 𝑡) ) = 𝑝 𝑡 | w he n 𝜑 | (𝑡 ) = | ⊤ a nd 𝜋 | (𝜑 ( 𝑡 )) | = 0 o th - | | | | | | | |
| --------------- | -------------- | ---------- | -------- | ------ | -------- | --------- | ---------- | ------------ | --------------- | ----------- | ------------- | ------------------------- | --- | --- |
| | | | | | | | | W h e n e st | i m a ti on i s | e n a b led | a n d 𝑛𝑈 𝑠 | < 1 ,Evergreenreturnsonly | | |
| e r w is e ; du | a l ly , 𝜋 ( ¬ | 𝜑 (𝑡 )) = | 𝑝 w h en | 𝜑 ( 𝑡) | = ⊥ an | d 𝜋 ( ¬ 𝜑 | (𝑡) ) = 0 | | | | | | | |
| | | | 𝑡 | | | | | ∏︁ 𝑝 f | o r th e pr o | c e s s ed | sa m p le 𝑆 ⊂ | R . | | |
𝑡∈ 𝑆 𝑡
otherwise.Thatis,0isinterpretedasafalseassertion. The universal cases are the dual of the existential cases. For
GrädelandTannen’smaincontribution[31]issupportfornega- ∀𝑡 ∈ R 𝜑(𝑡),
| | | | | | | | | a true universal | claim | | : | applying | rule | (iv) yields |
| --- | --- | --- | --- | --- | --- | --- | --- | ---------------- | ----- | --- | --- | -------- | ---- | ----------- |
tion.Whiletheinterpretation𝜋 producesapolynomialexplaining ∏︁ 𝜋(𝜑(𝑡)) =∏︁ 𝑝
| | | | | | | | | 𝑡∈R | | 𝑡∈R 𝑡.Hence,Evergreenreturnsthismono- | | | | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | ------------------------------------- | --- | --- | --- | --- |
atruesentence,ityields0forafalseone,givingnoexplanation.In
mialofallpositivetokens,whichindicatesthateachtupleinR
thiscase,𝜋caninsteadbeappliedtothesentence’snegation,which
| | | | | | | | | satisfies𝜑.Whenestimationisenabledand𝐿 | | | | | ≥1−𝜀,Evergreen | |
| --- | --- | --- | --- | --- | --- | --- | --- | -------------------------------------- | --- | --- | --- | --- | -------------- | --- |
istrue,revealingwhytheoriginalisfalse.Thisframeworkthuspro- 𝑠
| | | | | | | | | returnsonly∏︁ | 𝑝 | fortheprocessedsample. | | | | |
| --- | --- | --- | --- | --- | --- | --- | --- | ------------- | --- | ---------------------- | --- | --- | --- | --- |
𝑡∈𝑆 𝑡
videsexplanationsforbothcases,i.e.,why-provenanceandwhy-not
Forafalseuniversalclaim,weapplyrule(v)tointerpretitsnega-
provenance,soEvergreencanjustifyeachverdict,whethertrueor tion∃𝑡 :¬𝜑(𝑡).Applyingrule(iii)thengives∑︁ 𝜋(¬𝜑(𝑡)).
| | | | | | | | | ∈R | | | | | | 𝑡∈R |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
false.Wegiveexamplesofthisapproachinthenextsubsection.
| | | | | | | | | Eachtuple𝑡contributes𝜋(¬𝜑(𝑡))=𝑝 | | | | if𝜑(𝑡)=⊥and𝜋(¬𝜑(𝑡))= | | |
| --- | --- | --- | --- | --- | --- | --- | --- | ------------------------------- | --- | --- | --- | -------------------- | --- | --- |
𝑡
0otherwise.SinceEvergreenstopsearlyandanymonomialsuf-
5.2 ProvenanceSemanticsforClaims ficesasacounterexample,thereturnedprovenanceisthecorre-
| | | | | | | | | spondingnegativetoken𝑝 | | | forthefirsttuple𝑡 | | where𝜑(𝑡)=⊥. | |
| ------------------------------------------------------- | --- | --- | --- | --- | --- | --- | --- | ---------------------- | --- | --- | ----------------- | --- | ------------ | --- |
| Evergreenderivesitsprovenancefromthepriorinterpretation | | | | | | | | | | | 𝑡 | | | |
CardinalandProportionalClaims.GrädelandTannen[31]do
rules.However,ratherthancomputingthefullprovenancepolyno-
notexplicitlyprovideprovenanceexpressionsforcardinalquanti-
mial(i.e.,allalternativeexplanations),Evergreenreturnsasingle
fiers,sowederivethembasedontheirinterpretationrules.
monomial(i.e.,oneexplanation)eitherbecausethepolynomialis
| | | | | | | | | First,∃ | 𝑡 ∈R :𝜓(𝑡)isequivalentto𝑘nestedexistentialquan- | | | | | |
| --------------------------------------------------------- | --- | --- | --- | --- | --- | --- | --- | ------- | ----------------------------------------------- | --- | --- | --- | --- | --- |
| itselfamonomialorbecauseofoptimizationslikeearlystopping. | | | | | | | | | ≥𝑘 | | | | | |
tifiersoverstrictlyorderedtuples,eachsatisfying𝜓.Interpreting
Bythesemanticsoftheclaimtypes,everycompletemonomialEv-
ergreenobservesisminimal(i.e.,irredundant):nopropersubsetis inthesemiringreplaceseachexistentialquantifierwithasumand
eachconjunctionwithaproduct,yielding
alsoamonomialofthefullpolynomial.Thisisimmediatefortrue
existentialclaims(asingletokenpermonomial)andtrueuniversal ∑︂ ∏︂
| | | | | | | | | | 𝜋⟦∃ ≥𝑘 𝑡 | ∈R :𝜓(𝑡)⟧= | | | 𝜋⟦𝜓(𝑡)⟧. | |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | -------- | ---------- | --- | --- | -------- | --- |
claims(asinglemonomialoveralltuples),andfollowsfortheother
𝑊⊆R𝑡∈𝑊
claimtypesfromtheirpolynomialsderivedlaterinthissection.
|𝑊|=𝑘
22
Setting𝜓 = 𝜑,if𝜑(𝑡) = ⊤forall𝑡 ∈ 𝑊,then∏︁ 𝜋(𝜑(𝑡)) = OrdinalClaims.Anordinalclaimassertsthatatargetgroup𝐺
𝑡∈𝑊 𝑖
∏︁ 𝑝 ≠0;otherwise,theproductis0.Thepolynomialisthus achievesrank𝑟 among𝑚groups,wheretherankisbasedonaper-
𝑡∈𝑊 𝑡
thesumofmonomials,oneforeachsize-𝑘combinationofpositive groupaggregate𝑓.Thisisdeterminedbyaconjunctionof𝑚−1
tokens.Thepolynomialfor∃>𝑘 simplyreplaces𝑘with𝑘+1. pairwisecardinalcomparisonsbetween𝐺 𝑖 andeveryothergroup
Incontrast,∃ =𝑘 𝑡 ∈R :𝜓(𝑡)isequivalenttothesame𝑘nestedex- 𝐺 𝑗 (𝑖 ≠ 𝑗);inthesemiring,thisconjunctionbecomesaproduct
istentialquantifiers,butadditionallyrequiresthateveryremaining ofper-comparisonpolynomials.Eachcomparisonproducestwo
tupledoesnotsatisfy𝜓.Interpretinginthesemiringaugmentsthe
monomials(onepergroup)followingtheprovenancesemantics
| ≥𝑘polynomialwithaproductovertheremainingtuples𝑡′ | | | | | | ∈R\𝑊, | | | | | | |
| ------------------------------------------------ | --- | --- | --- | --- | --- | ----- | ------------------------------------------------------ | --- | --- | --- | --- | --- |
| ∃ | | | | | | | forcardinalorproportionalclaimsdependingontheaggregate | | | | | |
eachcontributing𝜋⟦¬𝜓(𝑡′)⟧,yielding 𝑓.When 𝑓(𝐺 ,𝜑) > 𝑓(𝐺 ,𝜑),𝐺
| | | | | | | | | | 𝑖 | 𝑗 | 𝑖’stokensfollowtherulesfora | |
| --- | --- | --- | --- | --- | --- | --- | ------------- | --- | ------------- | ------------------------------- | ------------------------------ | --- |
| | | | | | | | true∃>𝑓(𝐺𝑗,𝜑) | | claim,while𝐺 | 𝑗’stokensfollowtherulesforatrue | | |
| | | | | | | | ∃<𝑓(𝐺𝑖,𝜑) | | claim.When𝑓(𝐺 | ,𝜑) | < 𝑓(𝐺 ,𝜑),therolesarereversed. | |
𝑖 𝑗
| | | | | | | | When𝑓(𝐺 | | ,𝜑)=𝑓(𝐺 ,𝜑),bothgroups’tokensfollowtherulesfor | | | |
| ----------- | ------- | --- | ------- | --- | ---------- | --- | ------- | -------- | ---------------------------------------------- | --- | --- | --- |
| | | ∑︂ | ∏︂ | ∏︂ | | | | | 𝑖 𝑗 | | | |
| 𝜋⟦∃ =𝑘 𝑡 ∈R | :𝜓(𝑡)⟧= | ⎛ | 𝜋⟦𝜓(𝑡)⟧ | | 𝜋⟦¬𝜓(𝑡′)⟧⎞ | . | | | | | | |
| | | ⎜ | | | | ⎟ | atrue∃ | =𝑓(𝐺𝑖,𝜑) | claimandcontributealltokens. | | | |
𝑊⊆R 𝑡∈𝑊 𝑡′∈R\𝑊 NestedClaims.Anestedclaimcomposesanouterquantifierover
| | | |𝑊|=𝑘⎝ | | | | ⎠ | | | | | | |
| --- | --- | ------ | --- | --- | --- | --- | ------ | ---- | -------------- | --- | ----------- | ------------------ |
| | | | | | | | groups | with | an inner claim | per | group. Such | claims are already |
supportedbytheinductiveinterpretationrules.Evergreenfirst
Setting𝜓 = 𝜑,if𝜑(𝑡) = ⊤forall𝑡 ∈ 𝑊 and𝜑(𝑡′) = ⊥forall evaluateseachgroup’sinnerclaim,producingper-groupprove-
| 𝑡′ ∈R\𝑊,thenwehavethat∏︁ | | | 𝜋(𝜑(𝑡))∏︁ | | 𝜋(¬𝜑(𝑡′))= | | | | | | | |
| ------------------------ | --- | --- | --------- | --- | ---------- | --- | --- | --- | --- | --- | --- | --- |
𝑡∈𝑊 𝑡′∈R\𝑊 nancetokensfollowingthesemanticsoftheinnerclaimtype.The
| ∏︁ 𝑝 ∏︁ | 𝑝 | | | | | | | | | | | |
| ------- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
𝑡∈𝑊 𝑡 𝑡′∈R\𝑊 𝑡′ ≠0;otherwise,theproductis0.Sinceeach outerquantifierthencombinestheseper-grouptokensfollowingits
tupleeithersatisfies𝜑ordoesnot,atmostonesubset𝑊 yieldsa provenancesemantics.Forexample,iftheclaim∀𝐺 ∈G:(∃ 𝑡 ∈
≥2
nonzeroproduct,preciselywhen|𝑊|=𝑘,i.e.,thesentenceholds. 𝐺 : 𝜑(𝑡)) istrue,theprovenanceistheproductoftwopositive
Thepolynomialisthenasinglemonomial∏︁ 𝑝 ∏︁ 𝑝 𝑡′:a tokenspergroup.Otherwise,theprovenanceisthefirstfailing
| | | | | 𝑡∈𝑊 | 𝑡 𝑡′∈R\𝑊 | | | | | | | |
| --- | --- | --- | --- | --- | -------- | --- | --- | --- | --- | --- | --- | --- |
positivetokenforeachofthe𝑘tuplessatisfying𝜑andanegative group’stokens,showingthatfewerthantwoofitstuplessatisfy𝜑.
tokenfortheremaining|R|−𝑘.Theprovenancepolynomialsfor
| ∃<𝑘,∃ ≤𝑘,and∃ | ≠𝑘 arethesameas∃ | | =𝑘 | butsumoversubsets𝑊 | | | | | | | | |
| ------------- | ---------------- | ------------------ | --- | ------------------ | --------------- | --- | --- | ---------------------- | --- | --- | --- | --- |
| | | | | | | | 6 | EXPERIMENTALEVALUATION | | | | |
| of size < | 𝑘, ≤ 𝑘, and | ≠ 𝑘, respectively. | | As with | ∃ =𝑘, requiring | | | | | | | |
everytupleoutside𝑊 nottosatisfy𝜑 forces𝑊 tobeexactlythe OurexperimentalevaluationaimstoshowthatEvergreenachieves
setofsatisfyingtuples;everyothersubsetcontributes0.Hence, higherverificationqualityatlowercostthanexistingapproaches.
thepolynomialsfortheothercardinalquantifiersalsoreduceto Beyond this end-to-end comparison, we analyze the quality of
| atmostthesinglemonomial∏︁ | | | ∏︁ | | | | | | | | | |
| ------------------------- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
𝑡∈𝑊 𝑝 𝑡 𝑡′∈R\𝑊 𝑝 𝑡′ where𝑊 isthe Evergreen’sprovenanceandsemanticoperators,andablatethe
satisfyingset.Thesizeconstrainton𝑊 (< 𝑘,≤ 𝑘,or≠ 𝑘)only effectofeachoptimizationonqualityandcost.
determines whether this monomial is included in the sum, i.e., BenchmarkDatasetsandClaims.Tothebestofourknowledge,
whetherthepolynomialisnonzeroandthusthesentenceholds. nobenchmarktargetsclaimverificationoversemanticaggregates,
Giventhesepolynomials,wenowdescribetheprovenanceEv- so we curate one to evaluate Evergreen. From our analysis of
ergreenreturnsforeachcardinalclaimtype.Foratruecardinal productionsemanticaggregationqueriesonSnowflakeAISQL[48],
:𝜑(𝑡),atleastonemonomial∏︁
claim∃ ≥𝑘 𝑡 ∈R 𝑝 𝑡 of|𝑊|=𝑘 weobservethatqueriesareoftenexecutedoverrelationsofcus-
𝑡∈𝑊
positivetokensexists.Sinceearlystoppinghaltsafterfinding𝑘sat- tomerreviewsandsupporttickets.Assuch,wefirstselectthree
isfyingtuples,Evergreenreturnsonlythesefirst𝑘positivetokens. subsetsoftherestaurantreviewsintheYelpOpenDataset[84],
whichweidentifyasjohns(1,609tuples;230ktokens),mcdonalds
Forexample,iftheclaim“Atleastahandfulofvegetariancustomers
(1,813tuples;244ktokens),andvillage(1,603tuples;291ktokens).
enjoyedtherestaurant’sburgers”istrue,Evergreenreturnsthe
first𝑘positivetokenswithtuplessatisfying𝜑 :=“vegetariancus- mcdonaldscontainsreviewsfrom62McDonald’slocationsinMis-
tomerwhoenjoyedtherestaurant’sburgers”.Similartotheprior souri, while johns and village are reviews of separate restau-
claimtypes,whenestimationisenabledand𝑛𝐿 ≥𝑘,Evergreen rants.WethenincludethreesubsetsoftheCustomerSupporton
𝑠
| returnsonlythepositivetokensintheprocessedsample𝑆 | | | | | | ⊂R. | | | | | play | |
| ------------------------------------------------- | --- | --- | --- | --- | --- | --- | ------- | ------- | ----------- | --- | ----------- | ---------------- |
| | | | | | | | Twitter | dataset | [10], which | we | call (1,197 | tuples; 394k to- |
𝑡 :𝜑(𝑡),itsnegation∃<𝑘 𝑡 kens),airlines(3,167tuples;1,213ktokens),anduber(2,687tu-
| Forafalsecardinalclaim∃ | | | ≥𝑘 ∈ R | | | ∈ | | | | | | |
| ------------------------------- | --- | --- | ------ | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| :𝜑(𝑡)istrue,soitsprovenanceis∏︁ | | | | ∏︁ | | | | | | | | |
R 𝑡∈𝑊 𝑝 𝑡 𝑡′∈R\𝑊 𝑝 where ples;1,005ktokens).airlinescontainsdialogsbetweencustomers
𝑡′
|𝑊| < 𝑘,whichdemonstratesthatfewerthan𝑘 tuplessatisfy𝜑. andsupportagentsacrosssixairlines,whileplayandubercon-
Whenonlyasubsetoftuplesisprocessed—eitherbecausethecount taindialogsforPlayStationandUber,respectively.Wefollowprior
provablycannotreach𝑘
giventheremainingtuples,orbecause work[25]topreprocessthedialogs,keepingonlythosethatcontain
𝑛𝑈 <𝑘—thetokenscoveronlytheprocessedtuples.
| 𝑠 | | | | | | | 6–20utterancesbetweenasinglecustomerandagent. | | | | | |
| --- | --- | --- | --- | --- | --- | --- | --------------------------------------------- | --- | --- | --- | --- | --- |
For∃ =𝑘and∃ ≠𝑘,whenthecountequals𝑘,Evergreenprocesses Weposethreetypesofaggregationqueriesoverthesixdatasets
alltuplesandoutputsalltokenstodemonstratetheexactcount; viaAISQL’sAI_AGG()function[48]withLlama3.370B[29].We
whenthecountdiffersfrom𝑘,itmaystopearlyandoutputthe issueseparatesummarizationqueriestojohns,village,play,and
uber(e.g.,“SummarizewhatcustomersaresayingaboutJohn’s
processedtokens,demonstratingthatthecountliesaboveorbelow
𝑘.Sinceproportionalclaimsreducetocardinalclaims,Evergreen RoastPork”).Formcdonaldsandairlines,weissuecomparative
scalestheproportionthreshold𝜌bythenumberofprocessedtuples queries(e.g.,“ComparethereviewsforthedifferentMcDonald’s
andthenappliestheprovenancesemanticsofcardinalclaims. locations;highlightthecommonalitiesanddifferencesbetween
23
Table3:Representativesampleofbenchmarkclaims.
ID Dataset SemanticAgg.Type ClaimType Claim Grounded
C2 ∃ Somereviewersenjoytherestaurant’schickensalad. ⊤
C3 johns Summarize ∃≥0.1 CommoncriticismsofJohn’sRoastPorkincludecash-onlypolicy. ⊥
C4 ∀ Thereviewsdonotmentionanyveganoptions. ⊤
C8 Compare ∀∃≥2 AllMcDonald’slocationshavemultiplecomplaintsaboutpoorservicequality. ⊤
mcdonalds
C9 rank()=1 Thetop-rankedMcDonald’slocationintermsofservicehastheBusinessID[A]. ⊤
C10 Rank rank()=2 TheMcDonald’slocationranked#2intermsofservicehastheBusinessID[B]. ⊤
C16 village Summarize ∀ Thereareover200varietiesofwhiskeyavailableatVillageWhiskey. ⊥
C19 play Summarize ∃=0.1 10%ofcustomersareexperiencingproblemswithpaymentsorbilling. ⊥
C21 airlines Compare ∃=4∃>0.15 Thereare4airlinecompanieswhereover15%ofcustomercomplaintsareregardingflightdelays. ⊤
C26 Rank rank()=2 SouthwestAirhasthesecondmostcustomersupportdialogswithcomplaintsaboutflightbookingissues. ⊤
C29 ∃=776 776customerscomplainedaboutpoordriverbehavior. ⊤
C C 3 3 0 1 uber Summarize ∃ ∃ < < 7 0 2 .1 5 L L e e s s s s t t h h a a n n 7 1 2 0 5 % c o u f s c t u om sto e m rs e c r o s m re p p la o i r n te e d d r a e b c o e u iv t i p n o g o i r n d c r o i n v s e i r st b e e n h t a o v r io in r. accurateinformationfromsupportagents. ⊥ ⊥
C32 ∃<0.25 Lessthan25%ofcustomersreportedreceivinginconsistentorinaccurateinformationfromsupportagents. ⊤
therestaurantlocations”)andrankingqueries(e.g.,“Analyzethe Snowflakearctic-embed-l-v2.0[53].WecompareEvergreenwith
customersupportdialogsforthedifferentairlinecompaniesand fourimplementations:base_rm,rag_agent,rlm,andevg_unopt.
describetheworst3airlinecompaniesregardingflightbooking base_rmpromptsanLLMtoreasonaboutwhetheraclaimis
issues”).WeusetheapproachdescribedinSection2todecompose supportedbythegiveninputrelationandrepresentsexistingLLM-
eachaggregateresponseintoalistofclaims. as-a-judgebaselines[54,72,91].Weinstantiatebase_rmwiththree
Tocurateadiverseandbalancedbenchmark,westartfromthese LLMs:ClaudeOpus4.6[7],Sonnet4.6[9],andHaiku4.5[5].It
automaticallydecomposedclaims.Weusesomedirectly,adaptoth- serializeseachtupleasJSONandgreedilyfillsthepromptupto
ers(e.g.,recastingareportedproportionasacount,ornegatinga Claude’s200k-tokencontextwindow.Whenclaimsinvolvevague
claimtoobtainafalsevariant),andaddmanuallywrittenclaims. quantifiers (e.g., “common”), we provide hints specifying exact
Intotal,weobtain32claimsthatspanallclaimtypesdescribedin thresholds(e.g.,“atleast10%”)forafairercomparisonwiththe
Section2,withanevensplitbetweengroundedandungrounded reference ground truth. These hints are also used by the other
claims.Table3showsarepresentativesample.Ingeneral,complete implementations.Wesettemperatureto0andallowupto10retries,
humanannotationofclaim-levelgroundtruthisinfeasibleinour sincebase_rmoccasionallyexhaustsits8,192-tokenoutputlimit.
settingbecauseverifyingquantifiedclaims(e.g.,“allreviewsare rag_agentisanLLMagentthatusesaretrievaltoolandrep-
positive”)mayrequirereviewingeverytupleintherelation—over resentsanimplementationofiterativeretrieval-basedclaimver-
1,000perdataset.Instead,thegroundtruthvalidityofeachclaimis ification approaches [41, 83]. The interface to the retrieval tool
determinedwithareferenceimplementationof Evergreenthat issimilartorelevancesortingbutrestrictedtotop-kqueries.In
executesmanuallywrittenverificationqueries.Eachinvocationof additiontoasemanticsearchquery,inclusionkeywords,andexclu-
asemanticoperatortakesthemajorityvotefromanensembleof sionkeywords,theagentmustspecifyalimitonthemostrelevant
threestrongLLMsspanningdistinctfamilies(ClaudeOpus4.8[8], tuplestoretrievefromthedatabase.Theagentcanalsoinclude
GPT-5.5[57],andGemini3.5Flash[28]).Moreover,thereference structuredfiltersintheretrievalquery(e.g.,business_id = [A]),
implementationdisablesalloptimizations,sincesomecandegrade whichareexecutedaspre-filtersbeforeretrievingtherequested
qualityandearlystoppingpreventscapturingtuple-levellabelsfor numberoftuples.Aftertuplesareretrieved,theLLMcanchoose
provenanceandsemanticoperatorqualityevaluations.Toevaluate thenumberoftuplestoviewinitiallyfromtheset{10,20,...,50}.
agreementofthereferencelabelsagainstanindependenthuman Ateachiterationoftheagenticloop,theLLMeither(1)issuesa
reference,wefirstdrawastratifiedrandomsampleofper-operator retrievalqueryandviewstheinitialresults,(2)viewsthenextpage
decisions(i.e.,theensemble’stuple-levelfilterandmapoutputs)cov- ofpreviouslyretrievedtuples,or(3)outputswhethertheclaimis
eringall26distinctsemanticoperatorsinourbenchmark.Wethen groundedandterminates.Weinstantiaterag_agentwiththesame
samplefourdecisionsperoperator,balancedacrosslabelvalues, threeClaudemodelsasbase_rmandsettemperatureto1.
foratotalof104decisions.Thefirstauthor,blindtotheensemble rlmisaRecursiveLanguageModel(RLM)[87]thatcanitera-
labels,annotateseachsampleddecision,andwemeasureagreement tivelywriteandexecutearbitraryPythoncodeinaREPL,where
betweenthehumanandensembleusingexactmatchandCohen’s𝜅. thegeneratedcodecanalsoinvokesub-LLMcalls.Weadditionally
Thehumanandensembleagreeon98.1%ofdecisions(95%Wilson providerlmwiththesameretrievaltoolgiventorag_agent.As
CI[0.93,0.99];𝜅 =0.96).Asanadditionalcheck,forclaimswhose such,thisimplementationisageneralizationofpriorimperative,
verdictcanbedeterminedviaahandfuloftuples(e.g.,∃or∃ ≥𝑘 program-basedverificationapproaches[34,58].Weinstantiaterlm
withsmall𝑘),wemanuallyconfirmedtheensemble’sverdict:these usingtherecentimplementationinDSPy[42]andkeeptheroot
checksagreedwiththeensembleineverycase. LLMfixedtoOpuswhilevaryingthesub-LLMtothesamethree
Implementations. We use Snowflake Cortex AI [70] for LLM Claudemodelsusedforbase_rmandrag_agent.TherootLLM
inferenceandembeddinggeneration.Allembeddingsarecreatedby usesatemperatureof1whilethesub-LLMusesatemperatureof0.
24
evg_unoptinstantiatesEvergreenwithnooptimizationsen- areviewpraisingtherestaurant’schickensaladforexistentialclaim
abledandrepresentsanaivesemanticqueryprocessingenginelike C2,thetargetentitiesforordinalclaimsC10andC26,andallbutone
Binder[18].ItuseseachofthethreeClaudemodelsfromearlier airlinefornestedclaimC21).base_rmalsostruggleswithprecise
andevaluatessemanticoperatorsoneverytuple.AllEvergreen quantities,defaultingtoungroundedoncardinalclaimC29and
implementationsuseatemperatureof0.Moreover,implementa- proportionalclaimC32.rag_agentavoidsthefirstproblemsince
tionsprocesstuplesinbatchesof32,tradinguptoabatch’sworth retrievalsurfacestherelevantwitnesses,butbecauseitestimates
ofunnecessaryLLMcallsforsignificantlylowerlatency. quantitiesinnaturallanguagefromretrievedsamples,itstillfails
evg_optinstantiatesEvergreenwithalloptimizationsenabled. onclaimsrequiringpreciseaggregates(e.g.,C10,C19,C26,and
Weevaluatefiveconfigurations,eachusingadifferentLLMforits C29).Whilerlmimprovesoverrag_agent,itsometimesprocesses
semanticoperators.WeincludethethreeClaudemodelsusedinthe onlyasampleoftherelationwithitssub-LLM,soitfacessimilar
otherimplementationsandtwoadditionalQwenmodels(Qwen3- samplingimprecision(e.g.,cardinalclaimC30andproportional
VL-235B-A22B[11]andQwen3-Next-80B-A3B[62])toevaluate claimC31).Evenwhenrlmprocesseseverytuple,noisyper-tuple
howqualityandcostchangewithevenweakermodels.Opusis labelsandsmallper-groupdenominatorsfliptherankingforordinal
alwaysusedfortheoptimizer’sLLMtogeneratehigh-qualitysearch claimC9.Incontrast,Evergreen’sonlysourceoferrorissemantic
queries.Tomaintainhighrecall,wesetthethresholdforsimilarity operatormislabeling,asitssymbolicaggregationisotherwiseexact
filtersto0.15.ForestimationwithCSs,weset𝛼 =𝜀 =0.05. orstatisticallysound.Errorsoccurmorefrequentlywithweaker
ForEvergreenimplementations,claimsarecompiledtoqueries models;forexample,onC30,onlyOpusreturnsthecorrectverdict.
byprovidinganLLMwiththeclaim,theaggregationprompt,the However,claimsinvolvingcloserankings(C10)orexactcounts
datasetschema,hintsforvaguequantifiers,andEvergreen’sAPI (C29)remainchallengingevenforthestrongestmodel.
documentation(withexamplequeriesfromaseparatemoviereview ProvenanceandSemanticOperatorQuality.Tounderstand
domain).Averagedoverthe32claimsandthreetrialseach,itcosts howEvergreen’sprovenanceandsemanticoperatorsdegradewith
$0.051±0.001andtakes9.8±1.2s(mean±SD)tocompileaclaim weakermodels,weexecutethereferencequerieswithevg_unopt
usingOpus4.6,withnegligiblevariationacrossclaimtypes.We andevg_optacrossLLMsandmeasureprovenanceprecisionand
reviewedeverygeneratedqueryandfoundeachequivalenttoits per-operatorquality(Table5).Semanticfilterandmapqualityare
manuallywrittenreferencequery.Weattributethisreliablecompi- micro-averagedoverdistinctsemanticoperators,whileprovenance
lationtoEvergreen’sdeclarative,constrainedqueryinterface. precisionispooledacrossallqueries.Provenanceprecisionisthe
VerificationResults.Figure1highlightsthecost–qualitytrade- proportionofreturnedtokensthatarecorrectaccordingtothe
offs for each implementation, and Table 4 reports their quality, referenceimplementation.Wereportprecisionratherthanrecall
cost,andlatencyinmoredetail.Precision,recall,andF1scoretreat becauseEvergreenintentionallyreturnsnon-exhaustiveprove-
ungroundedclaimsasthepositiveclass,measuringanimplementa- nancetokens;wethereforerequireprovenancetobecorrect,not
tion’sabilitytodetecthallucinations.Sinceourbenchmarkhasan complete.Wemeasurefilterqualitybyprecision,recall,andF1,
evensplitbetweengroundedandungroundedclaims,wealsoreport treatingtuplesselectedbythereference’sfilterasthepositiveclass.
accuracy.Costiscomputedfrominputandoutputtokencounts Mapaccuracyistheproportionofmapoutputsthatmatchtheref-
atpublishedper-million-tokenUSDratesforeachLLM.Weuse erence.evg_optwithOpuscloselytracksevg_unopt:itmatches
Anthropic’sinput/outputrates[6]of$5/$25forOpus4.6,$3/$15for provenanceprecisionat0.94andhascomparablefilterprecision
Sonnet4.6,and$1/$5forHaiku4.5,andAlibabaCloud’srates[2] (0.99vs.0.98).Similarityfilteringmodestlyreducesfilterrecallto
of$0.287/$1.147forQwen3-VLand$0.144/$0.574forQwen3-Next. 0.90from0.97,loweringfilterF1to0.94from0.98,whilemapaccu-
SincelatencyissubjecttoCortex’sserver-sideconfigurationand racydipsslightlyto0.94from0.96.Qualitythendegradesgracefully
variability,wetreatitasasecondarymetric. asthemodelweakens:filterF1andmapaccuracyremainatleast
evg_optconfigurationsformtheentireParetofrontier:allother 0.90and0.88,respectively,acrossallmodels,whileprovenance
implementationsaredominatedbysomeevg_optpointwithhigher precisionisthemostsensitive,droppingto0.82from0.94.
or equal F1 at lower cost. Compared to evg_unopt with Opus, AblationStudy.Weevaluatethecontributionofeachoptimization
evg_optpreservesverificationqualityatanF1of0.94whilereduc- byperformingaleave-one-outablationstudywithHaiku,disabling
ingcostby3.1×($5.05vs.$15.88),demonstratingtheeffectiveness oneoptimizationwhilekeepingtheothersenabled.Figure6are-
of Evergreen’soptimizations.rlmwithSonnetperformsthebest portstheresultingcostmultipliersrelativetothefullyoptimized
amongthenon-EvergreenimplementationswithanF1of0.83; configuration;wesummarizeeachoptimizationbythegeometric
however, evg_opt with Qwen3-VL dominates at 0.87 with 7.0× meanoftheseratiosoveritsapplicableclaims.Notethatdisabling
lowercost($0.183vs.$1.29).Theseresultshighlighttheadvantages earlystoppingeffectivelydisablesrelevancesortingandestimation.
of Evergreen’sdeclarative,neuro-symbolicdesign.Byenabling Earlystoppingleadstothelargestcostsavingsof9.5×,illustrat-
theLLMcompilertosimplyspecifythehigh-levelverificationquery, ingthebenefitsofverification-awareoptimizations.Estimationand
EvergreenabstractsawayoptimizationdetailsandrestrictsLLMs operatorfusioneachgivecomparablesavingsof2.9×to3.0×.Rele-
tofine-grainedsemantictasks.Thisyieldshigherverificationqual- vancesortingprovidesmoremoderatesavingsof1.8×.Similarity
ityatlowercostwithweakermodelsthanapproachesthatrely filteringproducesalmostnocostsavingsinourevaluationbecause
on strong LLMs for both semantic and symbolic processing or thesimilaritythresholdissetlowtomaintainhighrecall,filtering
program-basedapproachesthatpushoptimizationontotheLLM. outfewtuplesbeforethesemanticfilterisexecuted.Promptcaching
Figure5revealseachimplementation’sfailuremodes.base_rm isomittedfromFigure6a:fouroftheeightapplicableclaimsare
failswhengroundingwitnessesfallbeyonditscontextwindow(e.g., servedentirelyfromcacheatnocostwhenenabled,sotheircost
25
Table4:Verificationquality,averagecost,andaveragelatencyacrossclaims.Wereportthemean[min,max]overthreetrials.
Implementation LLM Precision Recall F1Score Accuracy Cost($) Latency(s)
| ClaudeOpus4.6 | 0.71[0.70,0.73] 0.94[0.88,1.00] | 0.81[0.78,0.84] 0.78[0.75,0.81] | 0.945[0.942,0.947] | 47[39,58] |
| ------------- | ------------------------------- | ------------------------------- | ------------------ | --------- |
base_rm
| ClaudeSonnet4.6 | 0.69[0.67,0.71] 0.90[0.88,0.94] | 0.78[0.76,0.81] 0.75[0.72,0.78] | 0.570[0.568,0.573] | 92[76,105] |
| --------------- | ------------------------------- | ------------------------------- | ------------------ | ------------ |
| ClaudeHaiku4.5 | 0.61[0.60,0.62] 0.96[0.94,1.00] | 0.74[0.73,0.76] 0.67[0.66,0.69] | 0.188[0.188,0.188] | 17[17,17] |
| ClaudeOpus4.6 | 0.70[0.63,0.75] 0.75[0.75,0.75] | 0.72[0.69,0.75] 0.71[0.66,0.75] | 2.61[2.46,2.74] | 220[216,225] |
rag_agent ClaudeSonnet4.6 0.73[0.67,0.76] 0.79[0.75,0.81] 0.76[0.71,0.79] 0.75[0.69,0.78] 2.84[2.57,3.00] 324[294,355]
| ClaudeHaiku4.5 | 0.61[0.60,0.62] 0.88[0.75,1.00] | 0.72[0.67,0.76] 0.66[0.62,0.69] | 0.272[0.258,0.287] | 38[33,41] |
| -------------- | ------------------------------- | ------------------------------- | ------------------ | ------------ |
| ClaudeOpus4.6 | 0.83[0.80,0.87] 0.79[0.75,0.81] | 0.81[0.77,0.84] 0.81[0.78,0.84] | 1.89[1.77,2.02] | 260[257,261] |
rlm ClaudeSonnet4.6 0.89[0.86,0.92] 0.79[0.75,0.88] 0.83[0.80,0.88] 0.84[0.81,0.88] 1.29[1.21,1.32] 199[190,212]
| ClaudeHaiku4.5 | 0.80[0.73,0.86] 0.73[0.69,0.75] | 0.76[0.71,0.80] 0.77[0.72,0.81] | 0.649[0.616,0.680] | 177[163,193] |
| -------------- | ------------------------------- | ------------------------------- | ------------------ | ------------ |
| ClaudeOpus4.6 | 0.89[0.89,0.89] 1.00[1.00,1.00] | 0.94[0.94,0.94] 0.94[0.94,0.94] | 15.88[15.88,15.88] | 331[319,353] |
evg_unopt ClaudeSonnet4.6 0.83[0.83,0.83] 0.94[0.94,0.94] 0.88[0.88,0.88] 0.88[0.88,0.88] 9.54[9.54,9.54] 304[290,326]
| ClaudeHaiku4.5 | 0.83[0.83,0.83] 0.94[0.94,0.94] | 0.88[0.88,0.88] 0.88[0.88,0.88] | 3.23[3.23,3.23] | 354[316,400] |
| --------------- | ------------------------------- | ------------------------------- | --------------- | ------------ |
| ClaudeOpus4.6 | 0.89[0.89,0.89] 1.00[1.00,1.00] | 0.94[0.94,0.94] 0.94[0.94,0.94] | 5.05[4.86,5.36] | 261[193,317] |
| ClaudeSonnet4.6 | 0.88[0.88,0.88] 0.94[0.94,0.94] | 0.91[0.91,0.91] 0.91[0.91,0.91] | 3.25[3.17,3.37] | 192[169,227] |
evg_opt
| ClaudeHaiku4.5 | 0.83[0.83,0.83] 0.94[0.94,0.94] | 0.88[0.88,0.88] 0.88[0.88,0.88] | 1.01[1.00,1.01] | 133[103,179] |
| -------------- | ------------------------------- | ------------------------------- | ------------------ | ------------ |
| Qwen3-VL | 0.83[0.82,0.83] 0.92[0.88,0.94] | 0.87[0.85,0.88] 0.86[0.84,0.88] | 0.183[0.174,0.188] | 228[216,234] |
| Qwen3-Next | 0.82[0.81,0.82] 0.83[0.81,0.88] | 0.82[0.81,0.85] 0.82[0.81,0.84] | 0.113[0.111,0.116] | 114[111,115] |
base_rm Claude Opus 4.6 3 0 1 3 3 3 3 3 3 0 3 2 3 3 3 3 3 3 3 3 0 3 3 3 3 0 3 3 0 3 3 0
base_rm Claude Sonnet 4.6 3 0 3 3 3 3 3 3 3 0 3 1 3 3 3 3 3 2 3 3 0 3 3 3 3 0 3 3 0 0 3 0
base_rm Claude Haiku 4.5 3 0 3 0 3 3 3 0 0 0 3 3 3 3 3 1 3 3 3 3 0 3 0 3 3 0 3 3 0 3 3 0
rag_agent Claude Opus 4.6 3 2 3 3 3 3 3 3 3 0 3 0 3 3 3 3 0 0 0 1 1 3 3 3 3 1 2 2 0 3 2 3
rag_agent Claude Sonnet 4.6 3 3 3 3 3 3 3 3 3 0 3 1 3 3 3 3 3 2 0 3 0 3 3 3 2 1 0 2 0 3 2 2
noitatnemelpmI rag_agent Claude Haiku 4.5 3 3 3 0 3 3 1 0 0 1 2 3 3 3 1 3 2 3 1 2 2 1 3 3 1 1 3 3 0 3 3 0
rlm Claude Opus 4.6 3 3 3 3 3 3 3 3 1 1 2 2 3 3 3 3 0 0 1 3 3 3 3 3 3 3 3 3 2 2 1 3
rlm Claude Sonnet 4.6 3 3 3 3 3 2 3 3 1 2 3 3 3 3 3 3 2 2 1 2 3 3 3 3 3 3 3 3 3 0 0 3
rlm Claude Haiku 4.5 3 3 3 3 3 2 3 3 0 2 2 3 3 3 3 3 1 1 0 2 3 3 3 3 3 3 3 3 1 0 0 3
evg_unopt Claude Opus 4.6 3 3 3 3 3 3 3 3 3 0 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 0 3 3 3
evg_unopt Claude Sonnet 4.6 3 3 3 0 3 3 3 3 3 0 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 0 0 3 3
evg_unopt Claude Haiku 4.5 3 3 3 0 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 0 0 3 0
evg_opt Claude Opus 4.6 3 3 3 3 3 3 3 3 3 0 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 0 3 3 3
evg_opt Claude Sonnet 4.6 3 3 3 3 3 3 3 3 3 0 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 0 0 3 3
evg_opt Claude Haiku 4.5 3 3 3 3 3 3 3 3 3 0 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 3 0 0 3 0
evg_opt Qwen3-VL 3 3 3 3 3 3 3 3 3 0 3 3 3 2 3 3 3 3 3 3 0 3 3 3 3 3 3 3 0 0 3 3
evg_opt Qwen3-Next 3 3 3 3 3 3 3 3 3 0 3 3 3 0 3 3 3 3 3 3 0 3 3 3 3 3 3 3 0 0 1 3
C1 C2 C3 C4 C5 C6 C7 C8 C9C10C11C12C13C14C15C16C17C18C19C20C21C22C23C24C25C26C27C28C29C30C31C32
Claim
Figure5:Per-claimverificationcorrectness.Eachcellshowsthenumberofcorrecttrialsoutofthree.
Table5:Evergreen’sprovenanceprecisionandsemanticoperatorquality.Wereportthemean[min,max]overthreetrials.
Implementation LLM ProvenancePrecision FilterPrecision FilterRecall FilterF1Score MapAccuracy
| ClaudeOpus4.6 | 0.94[0.94,0.94] | 0.98[0.98,0.98] 0.97[0.97,0.98] | 0.98[0.98,0.98] 0.96[0.96,0.96] | |
| ------------- | --------------- | ------------------------------- | ------------------------------- | --- |
evg_unopt ClaudeSonnet4.6 0.91[0.91,0.91] 0.98[0.98,0.98] 0.97[0.97,0.97] 0.97[0.97,0.97] 0.95[0.95,0.95]
| ClaudeHaiku4.5 | 0.83[0.83,0.83] | 0.93[0.92,0.93] 0.99[0.99,0.99] | 0.96[0.95,0.96] 0.93[0.93,0.93] | |
| --------------- | --------------- | ------------------------------- | ------------------------------- | --- |
| ClaudeOpus4.6 | 0.94[0.94,0.95] | 0.99[0.98,0.99] 0.90[0.89,0.91] | 0.94[0.93,0.95] 0.94[0.94,0.95] | |
| ClaudeSonnet4.6 | 0.89[0.88,0.89] | 0.97[0.97,0.98] 0.89[0.88,0.90] | 0.93[0.93,0.94] 0.92[0.92,0.92] | |
evg_opt ClaudeHaiku4.5 0.82[0.81,0.82] 0.95[0.94,0.97] 0.89[0.89,0.90] 0.92[0.92,0.93] 0.89[0.88,0.89]
| Qwen3-VL | 0.89[0.89,0.89] | 0.98[0.98,0.98] 0.87[0.84,0.89] | 0.92[0.91,0.94] 0.92[0.91,0.93] | |
| ---------- | --------------- | ------------------------------- | ------------------------------- | --- |
| Qwen3-Next | 0.86[0.86,0.86] | 0.98[0.98,0.98] 0.83[0.83,0.84] | 0.90[0.90,0.91] 0.88[0.87,0.88] | |
multipliersareundefined.Measuredinsteadbytotalcostacrossthe {text}mentionsthenumberofwhiskeyvarietiesavailable”)main-
eightclaims,promptcachingreducescostby2.0×. tainhighrecall,whileclaimswithsemanticallybroaderpredicates
Weexaminethesimilarityfilter’ssensitivitytothethreshold. (e.g.,C21:“Thecustomersupport{dialog}containsacustomercom-
Thebenchmark’ssemanticfiltersreducetofourdistinctpredicates, plaint”)experiencearapiddropinrecall.Thus,0.15isaconservative
thoseofC3,C9,C16,andC21;therestreuseoneoftheseonthe default.Integratingmoreadvancedtechniques(e.g.,learningthe
samedatasetandyieldidenticalcurves.Figures6band6creport threshold[60,68]orlateinteraction[43,66])isanaturalnextstep.
recall(thefractionofreference-selectedtuplesabovethethreshold) Fourofthesixoptimizations—relevancesorting,operatorfu-
andfilterrate(thefractionoftuplesremoved)acrossthresholds. sion,similarityfiltering,andpromptcaching—maintainverification
Atthedefaultof0.15,recallexceeds0.99onallfourfilterswitha quality,whiledisablingearlystoppingorestimationeachlowers
filterrateofatmost0.02.Athigherthresholds,claimswithseman- precisionbyroughly0.06.BothdropstracetoC4,agroundeduni-
ticallyspecificfilterpredicates(e.g.,C16:“Therestaurantreview versalclaim.Withearlystoppingorestimationenabled,Evergreen
26
101
100
ES RS ECS OF SF
Implementation
reilpitluM
tsoC
1.0
0.8 9.5 0.6
2.9 3.0 0.4 1.8 1.0 0.2
0.0
0.1 0.2 0.3 0.4 0.5
Similarity Threshold
(a)Optimizationcostmultipliers.
llaceR
1.0
C3 0.8 C9 0.6
C16 0.4 C21 0.2
0.0
0.1 0.2 0.3 0.4 0.5
Similarity Threshold
(b)Similarityfilterrecall.
etaR
retliF
(c)Similarityfilterrate.
Figure6:Optimizationanalysis.(a)Costmultipliers(logscale)wheneachoptimizationisdisabled,relativetoevg_optwith
Haiku4.5(ES:EarlyStopping,RS:RelevanceSorting,ECS:EstimationwithConfidenceSequences,OF:OperatorFusion,SF:
SimilarityFiltering).Eachpointisoneclaim’smultiplier(meanofthreetrials);thehorizontallineisthegeometricmean
andthedashedlineat1×marksparitywithevg_opt.(b)Recalland(c)filterrateofthesimilarityfilteracrossthresholds;the
dashedlinemarksthe0.15default.Pointsaremeansoverthreetrials,andshadedregionsshowtherange.
onlyprocessesasubsetoftuplesandcorrectlyfindsnocounterex- Dataprovenanceoriginatedfromthedatabasecommunity[26],
ample.Withouttheseoptimizations,processingalltuplesincreases withfoundationalmodelsincludingdatalineage[20],why-and
theLLM’slikelihoodofflaggingafalsecounterexample,flipping where-provenance [12], and why-not provenance [13]. Seminal
theverdict.Thiseffectisnotgeneral,however,sinceestimationcan workbyGreenetal.[30]unifiesseveralofthesemodelsunder
alsomissavalidcounterexamplebysampling.Overall,ouropti- provenancesemirings,alsoknownashow-provenance.Subsequent
mizationsyieldsubstantialcostsavingswhilemaintainingquality. workextendssemiringsemanticstoothersettings,suchasaggrega-
tion[3]andfullfirst-orderlogicwithnegation[31].Severaldatabase
7 RELATEDWORK
systemssupportprovenancecaptureandquerying[27,46,55,56,
Section1presentedworkrelevanttoclaimverification.Here,we 61,67];however,nonesupportsemanticqueriesorprovenancefor
discussotherrelatedworkinmoredetail. first-orderlogic.InNLP,Zhangetal.[88,89]formalizeprovenance
SemanticqueryprocessingenginessuchasSnowflake’sCor- forclaimsasalabeledgraphoverdependentwebsources,tracing
texAISQL[48],DocETL[68,81],LOTUS[60],andPalimpzest[49, howaclaimoriginatedandevolved.Unlikethissetting,Evergreen
64],amongmanyothers[4,16,18,21,23,24,32,47,51,65,75,78,82], verifies quantified claims over independent tuples in a relation,
haveemergedinrecentyears.Attheircoreisasetofsemantic motivatingitschoiceofprovenancesemantics.
operators—includingsemanticaggregation—whichaugmenttradi-
tionaldatabaseoperatorswithLLMs.Toreducethecostofinvoking 8 CONCLUSIONS
theseoperators,novelqueryoptimizers[64,81]andefficientexecu-
WepresentEvergreen,asystemthatreliablyandefficientlyveri-
tionstrategies[50,69,71,76,85,86,90]havebeenproposed,with
fiesclaimsextractedfromsemanticaggregatesbycompilingthem
recentworkintroducingtheSemBenchbenchmarkforevaluating
intodeclarativesemanticverificationqueriescomposedofstan-
thesesystems[44].Yet,thecommunitylacksasystematicapproach
dardrelationalandsemanticoperators.Thisformulationadmits
to verify the correctness of semantic aggregates. Lee et al. [45]
asuiteofcomplementaryoptimizationsthatsubstantiallyreduce
describeavisionforsemanticintegrityconstraintsasadeclara-
costwhilepreservingverificationquality.Furthermore,eachver-
tiveabstractionforenforcingthecorrectnessofLLMoutputsin
dictisaccompaniedbyaminimalexplanationbasedonsemiring
semanticqueries.Evergreenisasteptowardsthisvision.
provenanceforfirst-orderlogic.Lookingahead,anaturalextension
Approximatequeryprocessing(AQP)tradesaccuracyfor
istoexploitsharedcomputationacrossthemanyclaimsthatarise
speedviasampling[1,14,33,59,92].Onlineaggregation[33]in-
fromasemanticaggregate,akintomulti-queryoptimizationin
troducedprogressiverefinementofaggregateestimates,allowing
databases.Assemanticaggregationbecomesastandardfeatureof
userstostopearlyonceestimatesappeartightenough;however,
productiondatasystems,Evergreendemonstratesthatthedeclar-
continuouslymonitoringclassicalCIsinvalidatestheirerrorguar-
ativequeryabstractionsalreadypresentinthesesystemscanbe
antees[38].Evergreen’suseofCSs[22,79]enablesvalidmon-
efficientlyleveragedtomaketheiroutputsreliableandexplainable.
itoringwithoutapredeterminedsamplesize.Morerecentwork
explores approximating aggregation queries that involve evalu-
ACKNOWLEDGMENTS
atingmultimodalsemanticoperatorsforfilters(e.g.,ABae[39],
ThalamusDB[36])andthestatisticsofinterest(e.g.,InQuest[63]). We thank the Snowflake AISQL team for their support and the
Incontrasttothesesettings,whichestimateboundsonthetrue anonymousreviewersfortheirconstructivefeedback.Thismaterial
aggregatevalues,verificationqueriesonlyneedtoresolveboolean isbaseduponworksupportedbytheNationalScienceFoundation
comparisonsinvolvingtheaggregates.Thisstructureenablesearlier GraduateResearchFellowshipProgramunderGrantNo.2439559.
termination:whiletraditionalAQPrelaxesapreciseaggregateto Anyopinions,findings,andconclusionsorrecommendationsex-
anintervalestimate,Evergreencollapsestheintervaltoaboolean pressedinthismaterialarethoseoftheauthorsanddonotneces-
verdict,needingonlyenoughprecisiontoresolvethecomparison. sarilyreflecttheviewsoftheNationalScienceFoundation.
27
REFERENCES
forComputingMachinery,NewYork,NY,USA,758–759. https://doi.org/10.
1145/1571941.1572114
[1] SameerAgarwal,BarzanMozafari,AurojitPanda,HenryMilner,SamuelMadden,
andIonStoica.2013.BlinkDB:querieswithboundederrorsandboundedresponse [20] YingweiCui,JenniferWidom,andJanetL.Wiener.2000.Tracingthelineageof
viewdatainawarehousingenvironment.ACMTrans.DatabaseSyst.25,2(June
timesonverylargedata.InProceedingsofthe8thACMEuropeanConference
| | | | | 2000),179–227. | https://doi.org/10.1145/357775.357777 | |
| --- | --- | --- | --- | -------------- | ------------------------------------- | --- |
onComputerSystems(Prague,CzechRepublic)(EuroSys’13).Associationfor
ComputingMachinery,NewYork,NY,USA,29–42. https://doi.org/10.1145/ [21] HanjunDai,BethanyYixinWang,XingchenWan,BoDai,SherryYang,Azade
Nova,PengchengYin,PhitchayaMangpoPhothilimthana,CharlesSutton,and
2465351.2465355
[2] AlibabaCloud.2026. AlibabaCloudModelStudio:Modelinferencepricing. DaleSchuurmans.2024.UQE:AQueryEngineforUnstructuredDatabases.In
TheThirty-eighthAnnualConferenceonNeuralInformationProcessingSystems.
| https://www.alibabacloud.com/help/en/model-studio/model-pricing. | | | Accessed: | | | |
| ---------------------------------------------------------------- | --- | --- | --------- | --- | --- | --- |
https://openreview.net/forum?id=t7SGOv5W5z
2026-06-23.
[3] YaelAmsterdamer,DanielDeutch,andValTannen.2011. Provenanceforag- [22] D. A. Darling and Herbert Robbins. 1967. CONFIDENCE SEQUENCES
| | | | | FORMEAN,VARIANCE,ANDMEDIAN. | | ProceedingsoftheNationalAcad- |
| --- | --- | --- | --- | --------------------------- | --- | ----------------------------- |
gregatequeries.InProceedingsoftheThirtiethACMSIGMOD-SIGACT-SIGART
SymposiumonPrinciplesofDatabaseSystems(Athens,Greece)(PODS’11).As- emy of Sciences 58, 1 (1967), 66–68. https://doi.org/10.1073/pnas.58.1.66
arXiv:https://www.pnas.org/doi/pdf/10.1073/pnas.58.1.66
| sociationforComputingMachinery,NewYork,NY,USA,153–164. | | | https: | | | |
| ------------------------------------------------------ | --- | --- | ------ | --- | --- | --- |
[23] UélisonJeanLopesdosSantos,AlessandroFerri,SzilardNistor,RiccardoTom-
//doi.org/10.1145/1989284.1989302
[4] EricAnderson,JonathanFritz,AustinLee,BohouLi,MarkLindblad,Henry masini,CarstenBinnig,andManishaLuthra.2025.TowardsaMultimodalStream
| | | | | ProcessingSystem. | arXiv:2510.14631[cs.DB] | https://arxiv.org/abs/2510.14631 |
| --- | --- | --- | --- | ----------------- | ----------------------- | -------------------------------- |
Lindeman,AlexMeyer,ParthParmar,TanviRanade,MehulA.Shah,etal.2025.
TheDesignofanLLM-poweredUnstructuredAnalyticsSystem.InCIDR. [24] TillDöhmen.2024. INTRODUCINGTHEPROMPT()FUNCTION:USETHE
POWEROFLLMSWITHSQL!https://motherduck.com/blog/sql-llm-prompt-
[5] Anthropic.2025.SystemCard:ClaudeHaiku4.5.https://www-cdn.anthropic.
com/7aad69bf12627d42234e01ee7c36305dc2f6a970.pdf. Accessed:2026-03-31. function-gpt-models/. Accessed:2026-03-31.
[6] Anthropic.2026.ClaudeAPIDocs:Pricing.https://platform.claude.com/docs/ [25] GuyFeigenblat,ChulakaGunasekara,BenjaminSznajder,SachindraJoshi,David
Konopnicki,andRanitAharonov.2021.TWEETSUMM-ADialogSummarization
| en/about-claude/pricing. | Accessed:2026-03-31. | | | | | |
| ------------------------ | -------------------- | --- | --- | --- | --- | --- |
[7] Anthropic.2026.SystemCard:ClaudeOpus4.6.https://www-cdn.anthropic. DatasetforCustomerService.InFindingsoftheAssociationforComputational
Linguistics:EMNLP2021,Marie-FrancineMoens,XuanjingHuang,LuciaSpecia,
| com/0dd865075ad3132672ee0ab40b05a53f14cf5288.pdf. | | Accessed:2026-03-31. | | | | |
| ------------------------------------------------- | --- | -------------------- | --- | --- | --- | --- |
[8] Anthropic.2026.SystemCard:ClaudeOpus4.8.https://www-cdn.anthropic. andScottWen-tauYih(Eds.).AssociationforComputationalLinguistics,Punta
com/0b4915911bb0d19eca5b5ee635c80fef830a37ea.pdf. Accessed:2026-06-23. Cana,DominicanRepublic,245–260. https://doi.org/10.18653/v1/2021.findings-
emnlp.24
[9] Anthropic.2026.SystemCard:ClaudeSonnet4.6.https://www-cdn.anthropic.
com/78073f739564e986ff3e28522761a7a0b4484f84.pdf. Accessed:2026-03-31. [26] BorisGlavic.2021.DataProvenance.Found.TrendsDatabases9,3-4(April2021),
209–441. https://doi.org/10.1561/1900000068
| [10] StuartAxelbrooke.2017.CustomerSupportonTwitter. | | https://doi.org/10.34740/ | | | | |
| ---------------------------------------------------- | --- | ------------------------- | --- | --- | --- | --- |
KAGGLE/DSV/8841 [27] BorisGlavicandGustavoAlonso.2009.Perm:ProcessingProvenanceandData
ontheSameDataModelthroughQueryRewriting.InProceedingsofthe2009
[11] ShuaiBai,YuxuanCai,RuizheChen,KeqinChen,XionghuiChen,ZesenCheng,
IEEEInternationalConferenceonDataEngineering(ICDE’09).IEEEComputer
LianghaoDeng,WeiDing,ChangGao,ChunjiangGe,WenbinGe,ZhifangGuo,
QidongHuang,JieHuang,FeiHuang,BinyuanHui,ShutongJiang,ZhaohaiLi, Society,USA,174–185. https://doi.org/10.1109/ICDE.2009.15
| | | | | [28] Google.2026. | Gemini3.5FlashModelCard. | https://storage.googleapis.com/ |
| --- | --- | --- | --- | ----------------- | ------------------------ | ------------------------------- |
MingshengLi,MeiLi,KaixinLi,ZichengLin,JunyangLin,XuejingLiu,Jiawei
Liu,ChenglongLiu,YangLiu,DayihengLiu,ShixuanLiu,DunjieLu,Ruilin deepmind-media/Model-Cards/Gemini-3-5-Flash-Model-Card.pdf. Accessed:
2026-06-23.
Luo,ChenxuLv,RuiMen,LingchenMeng,XuanchengRen,XingzhangRen,
[29] AaronGrattafiori,AbhimanyuDubey,AbhinavJauhri,etal.2024.TheLlama3
SiboSong,YuchongSun,JunTang,JianhongTu,JianqiangWan,PengWang,
PengfeiWang,QiuyueWang,YuxuanWang,TianbaoXie,YihengXu,Haiyang HerdofModels. arXiv:2407.21783[cs.AI] https://arxiv.org/abs/2407.21783
[30] ToddJ.Green,GrigorisKarvounarakis,andValTannen.2007. Provenance
Xu,JinXu,ZhiboYang,MingkunYang,JianxinYang,AnYang,BowenYu,Fei
Zhang,HangZhang,XiZhang,BoZheng,HumenZhong,JingrenZhou,Fan semirings.InProceedingsoftheTwenty-SixthACMSIGMOD-SIGACT-SIGART
SymposiumonPrinciplesofDatabaseSystems(Beijing,China)(PODS’07).Associ-
Zhou,JingZhou,YuanzhiZhu,andKeZhu.2025.Qwen3-VLTechnicalReport.
ationforComputingMachinery,NewYork,NY,USA,31–40. https://doi.org/10.
| arXiv:2511.21631[cs.CV] | https://arxiv.org/abs/2511.21631 | | | | | |
| ----------------------- | -------------------------------- | --- | --- | --- | --- | --- |
[12] PeterBuneman,SanjeevKhanna,andTanWang-Chiew.2001.WhyandWhere: 1145/1265530.1265535
[31] ErichGrädelandValTannen.2024.ProvenanceAnalysisandSemiringSemantics
ACharacterizationofDataProvenance.InDatabaseTheory—ICDT2001,Jan
VandenBusscheandVictorVianu(Eds.).SpringerBerlinHeidelberg,Berlin, forFirst-OrderLogic. arXiv:2412.07986[cs.LO] https://arxiv.org/abs/2412.07986
| | | | | [32] JianHeandVaibhavSethi.2025. | AnnouncingBigQuery-managedAIfunc- | |
| --- | --- | --- | --- | -------------------------------- | --------------------------------- | --- |
Heidelberg,316–330.
tionsforbetterSQL.https://cloud.google.com/blog/products/data-analytics/sql-
| [13] AdrianeChapmanandH.V.Jagadish.2009. | | Whynot?.InProceedingsofthe | | | | |
| ---------------------------------------- | --- | -------------------------- | --- | --- | --- | --- |
2009ACMSIGMODInternationalConferenceonManagementofData(Providence, reimagined-for-the-ai-era-with-bigquery-ai-functions. Accessed:2026-03-31.
[33] JosephM.Hellerstein,PeterJ.Haas,andHelenJ.Wang.1997.Onlineaggregation.
RhodeIsland,USA)(SIGMOD’09).AssociationforComputingMachinery,New
York,NY,USA,523–534. https://doi.org/10.1145/1559845.1559901 SIGMODRec.26,2(June1997),171–182. https://doi.org/10.1145/253262.253291
| | | | | [34] Qisheng Hu, | Quanyu Long, and Wenya | Wang. 2025. BOOST: Bootstrap- |
| -------------------------------------------------------- | --- | --- | ----------- | ---------------- | ---------------------- | ----------------------------- |
| [14] SurajitChaudhuri,BolinDing,andSrikanthKandula.2017. | | | Approximate | | | |
pingStrategy-DrivenReasoningProgramsforProgram-GuidedFact-Checking.
QueryProcessing:NoSilverBullet.InProceedingsofthe2017ACMInterna-
tionalConferenceonManagementofData(Chicago,Illinois,USA)(SIGMOD arXiv:2504.02467[cs.AI] https://arxiv.org/abs/2504.02467
[35] TharushiJayasekaraandImmanuelTrummer.2025.CEDAR:ASystemforCost-
’17).AssociationforComputingMachinery,NewYork,NY,USA,511–519.
https://doi.org/10.1145/3035918.3056097 EfficientData-DrivenClaimVerification.Proc.VLDBEndow.18,11(July2025),
4492–4504. https://doi.org/10.14778/3749646.3749708
[15] AtoosaChegini,KeivanRezaei,HamidEghbalzadeh,andSoheilFeizi.2025.
RePanda:Pandas-poweredTabularVerificationandReasoning.InProceedingsof [36] SaehanJoandImmanuelTrummer.2024. ThalamusDB:ApproximateQuery
the63rdAnnualMeetingoftheAssociationforComputationalLinguistics(Volume ProcessingonMulti-ModalData.Proc.ACMManag.Data2,3,Article186(May
| | | | | 2024),26pages. | https://doi.org/10.1145/3654989 | |
| --- | --- | --- | --- | -------------- | ------------------------------- | --- |
1:LongPapers),WanxiangChe,JoyceNabende,EkaterinaShutova,andMoham-
madTaherPilehvar(Eds.).AssociationforComputationalLinguistics,Vienna, [37] SaehanJo,ImmanuelTrummer,WeichengYu,XuezhiWang,CongYu,Daniel
| | | | | Liu,andNiyatiMehta.2019. | VerifyingTextSummariesofRelationalData | |
| -------------------- | ---------------------------------------------- | --- | --- | ------------------------ | -------------------------------------- | --- |
| Austria,32200–32212. | https://doi.org/10.18653/v1/2025.acl-long.1549 | | | | | |
[16] Shu Chen, Deepti Raghavan, and Uğur Çetintemel. 2025. Continuous Sets.InProceedingsofthe2019InternationalConferenceonManagementofData
(Amsterdam,Netherlands)(SIGMOD’19).AssociationforComputingMachinery,
| Prompts: LLM-Augmented | Pipeline Processing | over Unstructured | Streams. | | | |
| ----------------------- | -------------------------------- | ----------------- | -------- | ----------------------- | --------------------------------------- | --- |
| | | | | NewYork,NY,USA,299–316. | https://doi.org/10.1145/3299869.3300074 | |
| arXiv:2512.03389[cs.DB] | https://arxiv.org/abs/2512.03389 | | | | | |
[17] WenhuChen,HongminWang,JianshuChen,YunkaiZhang,HongWang, [38] RameshJohari,PeteKoomen,LeonidPekelis,andDavidWalsh.2017.Peeking
atA/BTests:Whyitmatters,andwhattodoaboutit.InProceedingsofthe23rd
| ShiyangLi,XiyouZhou,andWilliamYangWang.2020. | | TabFact:ALarge- | | | | |
| -------------------------------------------- | --- | --------------- | --- | --- | --- | --- |
scaleDatasetforTable-basedFactVerification.InInternationalConferenceon ACMSIGKDDInternationalConferenceonKnowledgeDiscoveryandDataMining
(Halifax,NS,Canada)(KDD’17).AssociationforComputingMachinery,New
| LearningRepresentations. | https://openreview.net/forum?id=rkeJRhNYDH | | | | | |
| ------------------------ | ------------------------------------------ | --- | --- | ---------------------- | --------------------------------------- | --- |
| | | | | York,NY,USA,1517–1525. | https://doi.org/10.1145/3097983.3097992 | |
[18] ZhoujunCheng,TianbaoXie,PengShi,ChengzuLi,RahulNadkarni,YushiHu,
CaimingXiong,DragomirRadev,MariOstendorf,LukeZettlemoyer,NoahA. [39] DanielKang,JohnGuibas,PeterBailis,TatsunoriHashimoto,YiSun,andMatei
Zaharia.2021.Acceleratingapproximateaggregationquerieswithexpensive
| Smith,andTaoYu.2023. | BindingLanguageModelsinSymbolicLanguages. | | | | | |
| -------------------- | ----------------------------------------- | --- | --- | --- | --- | --- |
InTheEleventhInternationalConferenceonLearningRepresentations. https: predicates.Proc.VLDBEndow.14,11(July2021),2341–2354. https://doi.org/10.
14778/3476249.3476285
//openreview.net/forum?id=lH1PV42cbF
[40] GeorgiosKaragiannis,MohammedSaeed,PaoloPapotti,andImmanuelTrummer.
[19] GordonV.Cormack,CharlesLAClarke,andStefanBuettcher.2009.Reciprocal
rankfusionoutperformscondorcetandindividualranklearningmethods.In 2020.Scrutinizer:amixed-initiativeapproachtolarge-scale,data-drivenclaim
verification.Proc.VLDBEndow.13,12(July2020),2508–2521. https://doi.org/10.
Proceedingsofthe32ndInternationalACMSIGIRConferenceonResearchand
| DevelopmentinInformationRetrieval(Boston,MA,USA)(SIGIR’09).Association | | | | 14778/3407790.3407841 | | |
| ---------------------------------------------------------------------- | --- | --- | --- | --------------------- | --- | --- |
28
[41] OmarKhattab,ChristopherPotts,andMateiZaharia.2021. Baleen:Robust [58] LiangmingPan,XiaobaoWu,XinyuanLu,AnhTuanLuu,WilliamYangWang,
Multi-HopReasoningatScaleviaCondensedRetrieval.InAdvancesinNeu- Min-YenKan,andPreslavNakov.2023. Fact-CheckingComplexClaimswith
ralInformationProcessingSystems,M.Ranzato,A.Beygelzimer,Y.Dauphin, Program-GuidedReasoning.InProceedingsofthe61stAnnualMeetingofthe
P.S. Liang, and J. Wortman Vaughan (Eds.), Vol. 34. Curran Associates, AssociationforComputationalLinguistics(Volume1:LongPapers),AnnaRogers,
Inc.,27670–27682. https://proceedings.neurips.cc/paper_files/paper/2021/file/ JordanBoyd-Graber,andNaoakiOkazaki(Eds.).AssociationforComputational
e8b1cbd05f6e6a358a81dee52493dd06-Paper.pdf Linguistics,Toronto,Canada,6981–7004. https://doi.org/10.18653/v1/2023.acl-
[42] OmarKhattab,ArnavSinghvi,ParidhiMaheshwari,ZhiyuanZhang,Keshav long.386
Santhanam,SriVardhamananA,SaifulHaq,AshutoshSharma,ThomasT. [59] YongjooPark,BarzanMozafari,JosephSorenson,andJunhaoWang.2018.Ver-
Joshi,HannaMoazam,HeatherMiller,MateiZaharia,andChristopherPotts. dictDB:UniversalizingApproximateQueryProcessing.InProceedingsofthe2018
2024.DSPy:CompilingDeclarativeLanguageModelCallsintoState-of-the-Art InternationalConferenceonManagementofData(Houston,TX,USA)(SIGMOD
Pipelines.InTheTwelfthInternationalConferenceonLearningRepresentations. ’18).AssociationforComputingMachinery,NewYork,NY,USA,1461–1476.
https://openreview.net/forum?id=sY5N0zY5Od https://doi.org/10.1145/3183713.3196905
[43] OmarKhattabandMateiZaharia.2020.ColBERT:EfficientandEffectivePas- [60] LianaPatel,SiddharthJha,MelissaPan,HarshitGupta,ParthAsawa,Carlos
sageSearchviaContextualizedLateInteractionoverBERT.InProceedingsofthe Guestrin,andMateiZaharia.2025.SemanticOperatorsandTheirOptimization:
43rdInternationalACMSIGIRConferenceonResearchandDevelopmentinInfor- EnablingLLM-BasedDataProcessingwithAccuracyGuaranteesinLOTUS.Proc.
mationRetrieval(VirtualEvent,China)(SIGIR’20).AssociationforComputing VLDBEndow.18,11(July2025),4171–4184. https://doi.org/10.14778/3749646.
Machinery,NewYork,NY,USA,39–48. https://doi.org/10.1145/3397271.3401075 3749685
[44] JialeLao,AndreasZimmerer,OlgaOvcharenko,TianjiCong,MatthewRusso, [61] FotisPsallidasandEugeneWu.2018.Smoke:fine-grainedlineageatinteractive
GerardoVitagliano,MichaelCochez,FatmaÖzcan,GautamGupta,Thibaud speed.Proc.VLDBEndow.11,6(Feb.2018),719–732. https://doi.org/10.14778/
Hottelier,H.V.Jagadish,KrisKissel,SebastianSchelter,AndreasKipf,andIm- 3199517.3199522
manuelTrummer.2026. SemBench:ABenchmarkforSemanticQueryPro- [62] QwenTeam.2025. Qwen3-Next:TowardsUltimateTraining&InferenceEffi-
cessingEngines. Proc.VLDBEndow.19,8(July2026),1754–1767. https: ciency.https://qwen.ai/blog?id=qwen3-next. Accessed:2026-06-23.
//doi.org/10.14778/3811243.3811249 [63] MatthewRusso,TatsunoriHashimoto,DanielKang,YiSun,andMateiZaharia.
[45] AlexanderW.Lee,JustinChan,MichaelFu,NicolasKim,AkshayMehta,Deepti 2023.AcceleratingAggregationQueriesonUnstructuredStreamsofData.Proc.
Raghavan,andUğurÇetintemel.2025.SemanticIntegrityConstraints:Declara- VLDBEndow.16,11(July2023),2897–2910. https://doi.org/10.14778/3611479.
tiveGuardrailsforAI-AugmentedDataProcessingSystems.Proc.VLDBEndow. 3611496
18,11(July2025),4073–4080. https://doi.org/10.14778/3749646.3749677 [64] MatthewRusso,ChunweiLiu,SivaprasadSudhir,GerardoVitagliano,Michael
[46] SeokkiLee,BertramLudäscher,andBorisGlavic.2019.PUG:aframeworkand Cafarella,TimKraska,andSamuelMadden.2026. Abacus:ACost-BasedOp-
practicalimplementationforwhyandwhy-notprovenance.TheVLDBJournal timizerforSemanticOperatorSystems. Proc.VLDBEndow.19,5(May2026),
28,1(Feb.2019),47–71. https://doi.org/10.1007/s00778-018-0518-5 1060–1073. https://doi.org/10.14778/3796195.3796215
[47] ZequnLi,YuanhaoZhong,ChengliangChai,ZhaozeSun,YuhaoDeng,YeYuan, [65] Gabriele Sanmartino, Matthias Urban, Paolo Papotti, and Carsten Binnig.
GuorenWang,andLeiCao.2025.DocDB:ADatabaseforUnstructuredDocument 2026. The Stretto Execution Engine for LLM-Augmented Data Systems.
Analysis.Proc.VLDBEndow.18,12(Aug.2025),5387–5390. https://doi.org/10. arXiv:2602.04430[cs.DB] https://arxiv.org/abs/2602.04430
14778/3750601.3750678 [66] KeshavSanthanam,OmarKhattab,JonSaad-Falcon,ChristopherPotts,andMatei
[48] PawełLiskowski,BenjaminHan,ParitoshAggarwal,BoweiChen,BoxinJiang, Zaharia.2022.ColBERTv2:EffectiveandEfficientRetrievalviaLightweightLate
NitishJindal,ZihanLi,AaronLin,KyleSchmaus,JayTayade,WeichengZhao, Interaction.InProceedingsofthe2022ConferenceoftheNorthAmericanChapter
AnupamDatta,NathanWiegand,andDimitrisTsirogiannis.2026. Cortex oftheAssociationforComputationalLinguistics:HumanLanguageTechnologies,
AISQL:AProductionSQLEngineforUnstructuredData.InCompanionof MarineCarpuat,Marie-CatherinedeMarneffe,andIvanVladimirMezaRuiz
theInternationalConferenceonManagementofData(India)(SIGMODCom- (Eds.).AssociationforComputationalLinguistics,Seattle,UnitedStates,3715–
panion’26).AssociationforComputingMachinery,NewYork,NY,USA,400–412. 3734. https://doi.org/10.18653/v1/2022.naacl-main.272
https://doi.org/10.1145/3788853.3803093 [67] Aryak Sen, Silviu Maniu, and Pierre Senellart. 2025. ProvSQL: A Gen-
[49] ChunweiLiu,MatthewRusso,MichaelCafarella,LeiCao,PeterBailleChen, eralSystemforKeepingTrackoftheProvenanceandProbabilityofData.
ZuiChen,MichaelFranklin,TimKraska,SamuelMadden,RanaShahout,and arXiv:2504.12058[cs.DB] https://arxiv.org/abs/2504.12058
GerardoVitagliano.2025.Palimpzest:OptimizingAI-PoweredAnalyticswith [68] ShreyaShankar,TristanChambers,TarakShah,AdityaG.Parameswaran,and
DeclarativeQueryProcessing.InCIDR. EugeneWu.2025.DocETL:AgenticQueryRewritingandEvaluationforComplex
[50] ShuLiu,AsimBiswal,AmogKamsetty,AudreyCheng,LuisGasparSchroeder, DocumentProcessing.Proc.VLDBEndow.18,9(May2025),3035–3048. https:
LianaPatel,ShiyiCao,XiangxiMo,IonStoica,JosephE.Gonzalez,andMatei //doi.org/10.14778/3746405.3746426
Zaharia.2025.OptimizingLLMQueriesinRelationalDataAnalyticsWorkloads. [69] ShreyaShankar,SepantaZeighami,andAdityaParameswaran.2026. Task
InEighthConferenceonMachineLearningandSystems. https://openreview.net/ CascadesforEfficientUnstructuredDataProcessing.Proc.ACMManag.Data4,
forum?id=R7bK9yycHp 1,Article88(April2026),26pages. https://doi.org/10.1145/3786702
[51] DuoLu,SimingFeng,JonathanZhou,FrancoSolleza,MalteSchwarzkopf,and [70] Snowflake.n.d..SnowflakeCortexAI.https://www.snowflake.com/en/product/
UğurÇetintemel.2025.VectraFlow:IntegratingVectorsintoStreamProcessing. features/cortex/. Accessed:2026-03-31.
InCIDR. [71] ZhaozeSun,ChengliangChai,QiyanDeng,KaisenJin,XinyuGuo,HanHan,
[52] SamuelMadden,MichaelJ.Franklin,JosephM.Hellerstein,andWeiHong.2003. YeYuan,GuorenWang,andLeiCao.2025. QUEST:QueryOptimizationin
TAG:aTinyAGgregationserviceforad-hocsensornetworks.SIGOPSOper.Syst. UnstructuredDocumentAnalysis.Proc.VLDBEndow.18,11(July2025),4560–
Rev.36,SI(Dec.2003),131–146. https://doi.org/10.1145/844128.844142 4573. https://doi.org/10.14778/3749646.3749713
[53] Luke Merrick, Danmei Xu, Gaurav Nuti, and Daniel Campos. 2024. [72] LiyanTang,PhilippeLaban,andGregDurrett.2024.MiniCheck:EfficientFact-
Arctic-Embed: Scalable, Efficient, and Accurate Text Embedding Models. CheckingofLLMsonGroundingDocuments.InProceedingsofthe2024Con-
arXiv:2405.05374[cs.CL] https://arxiv.org/abs/2405.05374 ferenceonEmpiricalMethodsinNaturalLanguageProcessing,YaserAl-Onaizan,
[54] SewonMin,KalpeshKrishna,XinxiLyu,MikeLewis,Wen-tauYih,PangKoh, MohitBansal,andYun-NungChen(Eds.).AssociationforComputationalLinguis-
MohitIyyer,LukeZettlemoyer,andHannanehHajishirzi.2023.FActScore:Fine- tics,Miami,Florida,USA,8818–8847. https://doi.org/10.18653/v1/2024.emnlp-
grainedAtomicEvaluationofFactualPrecisioninLongFormTextGeneration. main.499
InProceedingsofthe2023ConferenceonEmpiricalMethodsinNaturalLanguage [73] MichaelTheologitis,PreetamPrabhuSrikarDammu,ChiragShah,andDan
Processing,HoudaBouamor,JuanPino,andKalikaBali(Eds.).Associationfor Suciu.2026. ClaimDB:AFactVerificationBenchmarkoverLargeStructured
ComputationalLinguistics,Singapore,12076–12100. https://doi.org/10.18653/ Data. arXiv:2601.14698[cs.CL] https://arxiv.org/abs/2601.14698
v1/2023.emnlp-main.741 [74] MichaelTheologitisandDanSuciu.2026.Thucy:AnLLM-basedMulti-AgentSys-
[55] HaneenMohammed,CharlieSummers,SughoshKaushik,andEugeneWu.2023. temforClaimVerificationacrossRelationalDatabases.arXiv:2512.03278[cs.DB]
SmokedDuckDemonstration:SQLStepper.InCompanionofthe2023International https://arxiv.org/abs/2512.03278
ConferenceonManagementofData(Seattle,WA,USA)(SIGMOD’23).Association [75] MatthiasUrbanandCarstenBinnig.2023. CAESURA:LanguageModelsas
forComputingMachinery,NewYork,NY,USA,183–186. https://doi.org/10. Multi-ModalQueryPlanners.InCIDR.
1145/3555041.3589731 [76] MatthiasUrbanandCarstenBinnig.2024. ELEET:EfficientLearnedQuery
[56] HaneenMohammed,AlexanderYao,CharlieSummers,HongbinZhong,Gromit ExecutionoverTextandTables. Proc.VLDBEndow.17,13(Sept.2024),4867–
Yeuk-YinChan,SubrataMitra,LamprosFlokas,andEugeneWu.2024. FaDE: 4880. https://doi.org/10.14778/3704965.3704989
MoreThanaMillionWhat-IfsPerSecond.Proc.VLDBEndow.18,4(Dec.2024), [77] HaoranWangandKaiShu.2023.ExplainableClaimVerificationviaKnowledge-
943–955. https://doi.org/10.14778/3717755.3717757 GroundedReasoningwithLargeLanguageModels.InFindingsoftheAssociation
[57] OpenAI.2026.GPT-5.5SystemCard.https://deploymentsafety.openai.com/gpt- forComputationalLinguistics:EMNLP2023,HoudaBouamor,JuanPino,and
5-5/gpt-5-5.pdf. Accessed:2026-06-23. KalikaBali(Eds.).AssociationforComputationalLinguistics,Singapore,6288–
6304. https://doi.org/10.18653/v1/2023.findings-emnlp.416
29
[78] JiayiWangandGuoliangLi.2025.AOP:AutomatedandInteractiveLLMPipeline Manag.Data3,6,Article311(Dec.2025),26pages. https://doi.org/10.1145/
OrchestrationforAnsweringComplexQueries.InCIDR. 3769776
[79] Ian Waudby-Smith and Aaditya Ramdas. 2023. Estimating means of [86] Sepanta Zeighami, Shreya Shankar, and Aditya Parameswaran. 2025.
bounded random variables by betting. Journal of the Royal Statistical Featurized-DecompositionJoin:Low-CostSemanticJoinswithGuarantees.
Society Series B: Statistical Methodology 86, 1 (02 2023), 1–27. https:// arXiv:2512.05399[cs.DB] https://arxiv.org/abs/2512.05399
doi.org/10.1093/jrsssb/qkad009arXiv:https://academic.oup.com/jrsssb/article- [87] AlexL.Zhang,TimKraska,andOmarKhattab.2026.RecursiveLanguageModels.
pdf/86/1/1/56961777/qkad009.pdf arXiv:2512.24601[cs.AI] https://arxiv.org/abs/2512.24601
[80] JerryWei,ChengrunYang,XinyingSong,YifengLu,NathanHu,JieHuang, [88] YiZhang,ZacharyIves,andDanRoth.2020.“Whosaidit,andWhy?”Provenance
DustinTran,DaiyiPeng,RuiboLiu,DaHuang,CosmoDu,andQuocV.Le. forNaturalLanguageClaims.InProceedingsofthe58thAnnualMeetingofthe
2024. Long-formfactualityinlargelanguagemodels.InAdvancesinNeural AssociationforComputationalLinguistics,DanJurafsky,JoyceChai,Natalie
InformationProcessingSystems,A.Globerson,L.Mackey,D.Belgrave,A.Fan, Schluter,andJoelTetreault(Eds.).AssociationforComputationalLinguistics,
U.Paquet,J.Tomczak,andC.Zhang(Eds.),Vol.37.CurranAssociates,Inc., Online,4416–4426. https://doi.org/10.18653/v1/2020.acl-main.406
80756–80827. https://doi.org/10.52202/079017-2567 [89] YiZhang,ZacharyIves,andDanRoth.2021.WhatisYourArticleBasedOn?
[81] LindseyLinxiWei,ShreyaShankar,SepantaZeighami,YeounohChung,Fatma InferringFine-grainedProvenance.InProceedingsofthe59thAnnualMeetingof
Ozcan,andAdityaG.Parameswaran.2026.Multi-ObjectiveAgenticRewrites theAssociationforComputationalLinguisticsandthe11thInternationalJointCon-
forUnstructuredDataProcessing. arXiv:2512.02289[cs.DB] https://arxiv.org/ ferenceonNaturalLanguageProcessing(Volume1:LongPapers),ChengqingZong,
abs/2512.02289 FeiXia,WenjieLi,andRobertoNavigli(Eds.).AssociationforComputational
[82] Patrick Wendell, Eric Peter, Nicolas Pelaez, Jianwei Xie, Vinny Vi- Linguistics,Online. https://doi.org/10.18653/v1/2021.acl-long.458
jeyakumaar, Linhong Liu, and Shitao Li. 2023. Introducing AI Func- [90] FuhengZhao,JiayueChen,YimingPan,TahseenRabbani,Sohaib,Divyakant
tions: Integrating Large Language Models with Databricks SQL. Agrawal,AmrElAbbadi,ParitoshAggarwal,AnupamDatta,andDimitris
https://www.databricks.com/blog/2023/04/18/introducing-ai-functions- Tsirogiannis.2025. AccessPathsforEfficientOrderingwithLargeLanguage
integrating-large-language-models-databricks-sql.html. Accessed:2026-03-31. Models. arXiv:2509.00303[cs.DB] https://arxiv.org/abs/2509.00303
[83] ZhuohanXie,RuiXing,YuxiaWang,JiahuiGeng,HasanIqbal,DhruvSahnan, [91] LianminZheng,Wei-LinChiang,YingSheng,SiyuanZhuang,ZhanghaoWu,
IrynaGurevych,andPreslavNakov.2025.FIRE:Fact-checkingwithIterative YonghaoZhuang,ZiLin,ZhuohanLi,DachengLi,EricP.Xing,HaoZhang,
RetrievalandVerification.InFindingsoftheAssociationforComputationalLin- JosephE.Gonzalez,andIonStoica.2023. JudgingLLM-as-a-judgewithMT-
guistics:NAACL2025,LuisChiruzzo,AlanRitter,andLuWang(Eds.).Asso- benchandChatbotArena.InProceedingsofthe37thInternationalConference
ciationforComputationalLinguistics,Albuquerque,NewMexico,2901–2914. onNeuralInformationProcessingSystems(NewOrleans,LA,USA)(NIPS’23).
https://doi.org/10.18653/v1/2025.findings-naacl.158 CurranAssociatesInc.,RedHook,NY,USA,Article2020,29pages.
[84] Yelp.2023.YelpOpenDataset.https://business.yelp.com/data/resources/open- [92] YuxuanZhu,TengjunJin,StefanosBaziotis,ChengsongZhang,CharithMendis,
dataset/. Accessed:2026-03-31. andDanielKang.2025.PilotDB:Database-AgnosticOnlineApproximateQuery
[85] SepantaZeighami,ShreyaShankar,andAdityaParameswaran.2025.CutCosts, ProcessingwithAPrioriErrorGuarantees.Proc.ACMManag.Data3,3,Article
NotAccuracy:LLM-PoweredDataProcessingwithGuarantees. Proc.ACM 198(June2025),28pages. https://doi.org/10.1145/3725335
30