VerisyntaxEvidence-oriented language
Under udviklingVerisyntax er en lokal prototype. Funktioner, syntaks og dokumentation kan ændre sig.

Verisyntax — brugermanual (prototype 0.1)

Kontinuerte Bayes-modeller

Det første kontinuerte modelsnit bruger engelske distributionstermer:

p ~ beta(alpha = 2, beta = 2)
successes ~ binomial(trials = 20, probability = p)

observe successes = 14

ask p
  interval 0.89 hdi

Kør modellen reproducerbart:

<compiler>/verisyntax infer <example-project> \
  --seed 42 --chains 4 --warmup 1000 --samples 2000 --proposal-scale 0.8

Første version understøtter:

  • normal(mean = <number-or-variable>, sd = <positive number>);
  • student_t(df = <positive number>, mean = <number-or-variable>, scale = <positive number>) til robuste heavy-tailed modeller;
  • uniform(min = <number>, max = <number>) med min < max;
  • beta(alpha = <positive number>, beta = <positive number>);
  • binomial(trials = <positive integer>, probability = <number-or-variable>), hvor binomialvariablen skal observeres;
  • numeriske observationer som observe successes = 14;
  • kontinuerte queries med interval <mass> hdi; uden interval-linjen bruges 0,89.

En binomial probability-reference skal være en beta eller en uniform, hvis støtte ligger helt inden for [0,1]. En binomial query er diskret og afvises derfor som kontinuerlig HDI-query. Dependency-cycles, ukendte variable, observationer uden for støtte og ugyldige parametre afvises af C++-typekontrollen.

Runtime bruger deterministic-seed, multi-chain random-walk Metropolis. Før warmup flyttes uobserverede normalparametre med en begrænset, deterministisk tæthedssøgning fra hver sin prior-draw. Under warmup tilpasses proposal-bredden separat for hver uobserveret parameter med en deterministisk Robbins–Monro-opdatering mod 44 % acceptance. Bredderne fryses, før retained sampling starter. Det forhindrer både meget fjerne startpunkter og proposal-trin, som er alt for store til en smal posterior. initialization, warmupAdaptation, warmup-acceptance og retained-acceptance gemmes i JSON-resultatet. De retained samples og posteriorberegningen kommer fortsat fra Metropolis-sampleren, ikke fra søgningen eller en LLM.

JSON-resultatet er markeret exact: false og viser diagnosticsPassed, posterior mean/SD, HDI, effective sample size, split R-hat, warmup- og retained-acceptance, seed og sampleantal. Samme program, seed og indstillinger giver byte-identisk resultat med samme build. Hvis R-hat eller ESS fejler, viser IDE'en Run completed with warnings i stedet for et ukvalificeret Run completed. Det er stadig approksimativ inferens: kontrollér især split R-hat, ESS, acceptance og advarsler før resultatet bruges. Et godt diagnostisk tal er ikke i sig selv bevis for, at modellen er korrekt.

En indbygget regressionstest bruger theta ~ normal(0,1), measurement ~ normal(theta,1) og observe measurement = 1000. Det analytiske facit er theta | measurement=1000 ~ normal(mean=500, variance=0.5). Standardkørslen skal derfor ligge tæt på mean 500 og SD sqrt(0.5) og samtidig bestå R-hat/ESS-kontrollen; testen beskytter mod, at kæderne blot stopper på vej fra prioren til posterioren.

En anden regressionstest bruger prioren theta ~ normal(10,5) og to meget præcise sensorer med SD 0,1, observeret til henholdsvis 15 og 5. Det analytiske facit har mean præcis 10 og varians 1/200.04, altså SD cirka 0,07070. Testen kræver også R-hat under 1,01, ESS på mindst 400 og retained acceptance inden for review-intervallet; den beskytter mod proposal-trin bestemt af den langt bredere prior.

Sikkerhedsgrænserne er 2–16 chains, højst 100.000 warmup-samples og 100–100.000 retained samples pr. chain, højst én million samlede samples og proposal scale 0,01–5. Alle samples, HDI, ESS og split R-hat beregnes af C++-programmet; ingen LLM deltager i den numeriske inferens.

Prediktive binære observationer kan evalueres deterministisk fra en TSV med kolonnerne split, period, probability, outcome. Rækkerne skal være temporalt ordnet train, validation, test; omvendt splitrækkefølge afvises:

<compiler>/verisyntax evaluate-predictions predictions.tsv --bins 10

Resultatet viser Brier score, clipped log loss, calibration bins og expected calibration error samlet og pr. split. Det er modeldiagnostik, ikke kausal evidens.

En færdig kørsel kan gemmes eksplicit i et allerede initialiseret metadata-schema:

<compiler>/verisyntax infer model.vsx --seed 42 --store local
<compiler>/verisyntax inference-runs list model.vsx local --limit 20

Audit-rækken gemmer IR-hash, metode, seed, samplerindstillinger, diagnostics, canonical result og start/sluttid atomisk. --store er aldrig implicit og gælder i første version kun kontinuerte kørsler.