Auto-Formalizing Neuro-Symbolic Predictors

1 Introduction

• End users still need to identify and formalize domain knowledge, even in frameworks intended to make NeSy predictors more accessible.The paper proposes using LLMs to translate natural-language knowledge into symbolic constraints.Source: §1 · p. 1
• auto-nesy-bench extends rsbench with prompts, data instances, output annotations, and metrics for formalizing CNF constraints from text.The benchmark targets a gap left by SAT and CP benchmarks, which do not measure the effect of generated constraints on downstream NeSy performance.Source: §1 · p. 2
• The paper evaluates multiple formalisms and reports that performance depends on constraint-description detail, while syntactically valid formulas can have little downstream impact from formalization errors.Outputs include DIMACS, Python-based formalisms, and natural language.Source: §1 · p. 2
• The evaluation examines whether LLMs can formalize constraints and how generated constraints affect NeSy models using a layer or a training loss.It varies LLMs, input and output formats, and evaluates semantic probabilistic layers and semantic loss.Source: §1 · p. 2

2 NeSy Predictors

• NeSy predictors combine a neural network’s predictions with prior knowledge K to assign lower or even zero probability to outputs that violate K.The constraints can encode structural or safety requirements.Source: §2 · p. 2
• The traffic-rule example excludes the combination green=1, clear=1, forward=0 and renormalizes probability over the remaining valid combinations.Combinations satisfying the rule remain possible.Source: §2 · p. 3
• A semantic probabilistic layer combines the network distribution with a constraint distribution represented by a compiled probabilistic circuit.The resulting distribution is a tractable product of experts normalized by Zx.Source: §2 · p. 3
• SPL requires a well-formed CNF constraint and provably assigns zero probability to invalid outputs, whereas semantic loss is an alternative that uses soft constraints.The partition function is the weighted model count induced by K and can be computed exactly with circuits.Source: §2 · p. 3

3 Auto-formalizing Neuro-Symbolic Predictors

• The pipeline has two stages: an LLM formalizes a constraint, then the generated formula is incorporated into a NeSy predictor for learning and inference.The LLM is treated as a black-box function that maps a prompt to an output sequence.Source: §3 · p. 3

3.1 Constraint Formalization

• Unlike acquisition from examples or oracle interaction, this setup uses one natural-language description as the constraint-acquisition input.The LLM acts as the constraint-acquisition mechanism.Source: §3.1 · p. 3
• The target is propositional logic in CNF, with equivalent representations in DIMACS, NAT, PySAT, CPMpy, and SymPy unified through DIMACS.The formats test whether formalization depends on the target syntax and reflect interfaces practitioners use.Source: §3.1 · pp. 3–4
• Prompts specify the target syntax, grounded variables, and a required output block; detected syntax errors can trigger iterative correction prompts.The study also varies prompt detail to assess dependence on user expertise.Source: §3.1 · p. 4
• The LLM receives the complete set of primary variables and their meanings, isolating constraint formalization from symbol identification.Auxiliary variables are allowed when explicitly defined in terms of primary variables.Source: §3.1 · p. 4
• Formula quality is evaluated by comparing generated and ground-truth valid assignments with model counting, rather than checking satisfiability alone.The evaluation derives precision, recall, and F1; recall matters because SPL cannot predict assignments excluded by an incorrect constraint.Source: §3.1 · p. 4

3.2 From Auto-Formalization To NeSy Predictors

• Generated CNFs are compiled into SDDs and used in SPL or semantic loss, where incorrect or incomplete constraints affect predictions differently.SPL constraints determine feasible predictions, while in semantic loss they act as a training bias.Source: §3.2 · p. 5
• The study adds REL, CON, and MC-R to characterize formula relationships, consistency with the ground truth, and relative satisfying-assignment counts.MC-R quantifies how much the generated formula’s satisfying-assignment set differs in size from the ground-truth set.Source: §3.2 · p. 5

4 Auto-NeSy-Bench

• The benchmark evaluates both whether LLMs formalize intended domain knowledge and how generated constraints affect NeSy predictors, a pipeline not covered by existing SAT/CP or NeSy benchmarks.Existing constraint-generation benchmarks address standalone SAT or CP, while NeSy benchmarks typically assume background knowledge is already available.Source: §4 · p. 5
• The repurposed satbench retains 1,041 SAT instances after excluding UNSAT cases and applying consistency checks.UNSAT instances would give an SPL zero probability for every configuration, making the downstream predictor uninformative.Source: §4 · p. 5
• The repurposed dcpbench yields 85 instances after filtering out optimization, continuous-variable, oversized-circuit, and non-convertible cases.The resulting set is used to evaluate LLM auto-formalization.Source: §4 · pp. 5–6
• Table 1 compares models across benchmarks using F1, precision, recall, and syntax-error rate, with results reported as mean ± standard deviation.Models are ordered by size; best and second-best results are marked.Source: Table 1 · p. 6
• auto-nesy-bench extends rsbench to 18 NeSy problems and pairs tasks with descriptions at multiple granularity levels and annotated examples.The benchmark is intended to cover constraint extraction through downstream NeSy prediction.Source: §4 · p. 6

5.1 RQ1: Auto-formalization of Logical Constraints

• On auto-nesy-bench, gpt-oss-120b achieved the highest F1 at 0.786, while gemma-3-27b achieved 0.040 and had a 55.6% syntax error rate.No tested LLM reached perfect performance; gpt-oss-120b also achieved F1 of 0.963 on satbench and 0.324 on dcpbench.Source: §5.1 · p. 7
• On auto-nesy-bench, detailed descriptions raised F1 from 0.330 to 0.455, while syntax errors also rose from 25.3% to 28.9%.The passage reports that the F1 gain is unlikely to reflect easier parsing.Source: §5.1 · p. 7, Table 2 · p. 7
• CoT prompting raised F1 from 0.437 to 0.472 on auto-nesy-bench, 0.176 to 0.191 on dcpbench, and 0.805 to 0.893 on satbench.Its effects on recall and syntax errors varied by benchmark.Source: §5.1 · p. 7, Table 2 · p. 7
• CPMpy achieved the highest auto-nesy-bench F1 among output formats at 0.575, whereas NAT led on satbench at 0.920.Code-based formats generally outperformed DIMACS and NAT on auto-nesy-bench and dcpbench, but syntax-error rates did not track performance.Source: §5.1 · p. 7, Table 3 · p. 8

5.2 RQ2: Downstream Impact of LLM-Generated Constraints

• Generated formulas, when available, yield downstream SPL performance comparable to ground-truth formulas, with mean differences below 0.03 in ΔF1 and 0.02 in Δrecall.The comparison uses SPL on auto-nesy-bench; one exception is qwen3-8b on kand-logic-2, whose formula captures only 2% of valid assignments.Source: Table 4 · p. 8, §5.2 · p. 8
• gpt-oss-120b produced valid formulas on all 18 tasks, while olmo3-32b-think and qwen3-8b had failures on 6/18 and 7/18 tasks, respectively.Failures were roughly evenly divided among degenerate, unproduced, and run-failure formulas.Source: §5.2 · p. 9

• Prior language-to-formal-model work evaluates end-task accuracy or formalization quality, but does not target auto-formalization for NeSy predictors.Related directions include constraint programming, logic translation, ontologies, executable programs, and answer set programming.Source: §6 · p. 9
• NeSy knowledge acquisition has included learning symbolic knowledge from data and learning interpretable knowledge-bearing models, while this work studies formalization from natural-language descriptions.The described prior approaches assume a human-specified predicate vocabulary or knowledge learned from data.Source: §6 · p. 9

• The authors report that the best-performing LLMs generate high-quality formulas with downstream performance comparable to manually constructed formulas, while smaller models can struggle substantially.They frame generated formulas as interpretable support for domain experts, not a replacement, because the formulas can be inspected and corrected.Source: §7 · p. 9
• The evaluation is restricted to propositional formulas and SPL and SL, leaving broader predictor architectures and more complex constraint formalisms for future work.The paper notes that substantially more complex constraints remain a general challenge in NeSy AI.Source: §7 · p. 9

A Implementation

• Experiments use Python 3.12.4 and PyTorch 2.11; LLM evaluation runs with vLLM across experiment clusters.Table 5 covers LLM evaluation with the vLLM backend across those clusters.Source: A Implementation · p. 19, Table 5 · p. 19
• SPL and SL experiments use two RTX 4090s, and SPL implementations are taken verbatim from cirkit.Datasets come from original repositories or are generated; dataset details and hyperparameters are referenced in Sections D, G, and H.Source: A Implementation · p. 19
• All tested models are open-weight and downloaded directly from HuggingFace.The passage also states that datasets were sourced from their original repositories or generated.Source: A Implementation · p. 19

B.1 Auto-formalization

• Syntax error rate is measured after self-verification, when present, for LLM-generated formulas.The section introduces the metrics used in the experiments.Source: §B.1 · p. 19, B Metrics · p. 19
• For formulas without auxiliary variables, confusion-matrix counts use exact model counting up to 20 variables and ApproxMC above 20.True positives, false positives, false negatives, and true negatives are defined by intersections of the ground-truth and predicted formulas.Source: §B.1 · p. 19
• When encodings contain auxiliary variables, reported quantities use the projection onto primary variables before negation or conjunction.With ApproxMC, each of three calls uses confidence δ/3, so T, P, and TP counts hold jointly with probability at least 1−δ by the union bound.Source: §B.1 · pp. 19–20

B.2 Downstream NeSy predictor

• Downstream evaluation uses standard supervised-learning metrics and hold-out test data, plus consistency of final MAP predictions with the ground-truth formula.Consistency below 1.00 indicates some predicted assignments violate constraints, which can be harmful to the downstream application.Source: §B.2 · p. 20
• The REL metric classifies generated formulas as equal, permissive, strict, or incomparable relative to the ground-truth formula.Permissive formulas admit invalid assignments; strict formulas exclude some valid assignments, removing their support from the predictive distribution; incomparable formulas have both error types.Source: §B.2 · p. 20
• MC-R quantifies how much more or less permissive a generated formula is, including when its qualitative relation to ground truth is not equal.For example, a permissive formula with mc_ratio = 1.75 admits 75% more satisfying assignments than the ground truth.Source: §B.2 · p. 20

C Error Taxonomy

• Errors are divided into general errors that apply to DIMACS regardless of source format and generation errors introduced by the particular DIMACS-generation process.The general category also applies to NAT and executed PySAT, CPMpy, and SymPy output.Source: C Error Taxonomy · p. 20
• General DIMACS errors include malformed or missing headers and tags, clause-format problems, invalid content, out-of-range literals, and overly complex NAT-to-CNF conversion.A single output may trigger more than one error code.Source: C Error Taxonomy · p. 21
• Generation errors vary by format and include execution or timeout errors, mapping and Boolean-variable issues, and NAT parsing or operator errors.For applicable DIMACS layers, a preamble auto-fix recomputes missing variable counts and mismatched clause counts from clause bodies without another LLM query.Source: C Error Taxonomy · p. 21

D Datasets

• auto-nesy-bench combines a balanced mix of problem sizes with input-output annotations for NeSy predictors, unlike SATBench’s many small problems and DCP-Bench’s fewer, larger problems.Table 6 reports variable and clause counts as MIN / MAX / MEAN.Source: Table 6 · p. 21

D.1 SATBench

• SATBench’s natural-language scenarios and reference CNF formulas are repurposed to test constraint recovery; removing UNSAT and malformed instances leaves 1,041 SAT instances.The original 2,100 instances were evenly split between SAT and UNSAT; nine malformed SAT instances were also removed.Source: §D.1 · pp. 21–22

D.2 DCPBench-Open

• DCP-Bench-Open’s 164 CP problems are instantiated and converted to one-hot CNF; filtering unusable cases leaves 85 problems with DIMACS targets for the main experiments.Excluded cases include optimization problems, failed conversions, and conversions exceeding a 90-second timeout; prompts omit problem names and enumerate Boolean variables and value ranges.Source: §D.2 · p. 22

D.3 Auto-NeSy-Bench

• auto-nesy-bench contains 18 established NeSy visual-reasoning tasks, spanning formulas from single-digit to hundred-plus variable counts.Examples include relational Kandinsky-pattern tasks, 4 × 4 VisualSudoku, and a 4 × 4 Warcraft shortest-path task.Source: §D.3 · pp. 23, 25, 26
• Task-validity predicates are compiled into DIMACS CNF and cross-checked against a Python oracle; road-r instead uses its dataset’s existing CNF.The oracle check is exhaustive when the variable count permits (≤220 assignments).Source: §D.3 · pp. 26, 28

D.3.2 Constraint descriptions (detailed vs. non-detailed)

• Detailed and non-detailed task descriptions differ only in constraint-description explicitness; two authors independently wrote and reconciled them while keeping the surrounding prompt and variable list identical.The detailed version lists rules and background facts not to encode, while the concise version can leave rule decomposition or conventions implicit.Source: §D.3 · p. 28

D.3.1 Licensing and Redistribution

• The code is planned for BSD-3-Clause release, while redistributed data artifacts use CC BY-NC-SA 4.0; SUSHI3 and CIFAR-10/100 are obtained from their original sources instead.SUSHI3 prohibits redistribution, and CIFAR-10/100 lack an explicit license or redistribution grant.Source: §D.3.1 · pp. 28–29

D.3.2 Constraint descriptions (detailed vs. non-detailed)

• Single-digit multiplication descriptions specify digit and product ranges and their product relation, while chest X-ray severity rules map finding counts to codes and require exactly one code.These examples include detailed and less-detailed formulations of the tasks.Source: §D.3.2 · pp. 29–30
• Classification examples range from the exactly-one-class rule for clothing to object rules using features such as wings, wheels, and animal traits, with unmatched objects left unclassified.The general object-classification examples also contrast exactly-one-class wording with an explicit prohibition on assigning multiple classes.Source: §D.3.2 · pp. 30–31
• Sushi-ranking constraints require a one-to-one assignment between items and ranks, while 4x4 grid validity requires each digit once per row, column, and 2x2 box.The detailed grid description enumerates the four boxes and applies constraints across all 16 cells.Source: §D.3.2 · p. 32
• The 4x4 pathfinding descriptions require one simple path from (0,0) to (3,3), excluding cycles and disconnected loops or paths.The detailed version specifies endpoint and intermediate-cell edge conditions.Source: §D.3.2 · p. 33
• Pattern-recognition descriptions define color and shape patterns by whether three primitives all match, exactly two match, or all differ; a two-primitive variant uses same-versus-different patterns.Both versions require the two images to share a color or shape pattern.Source: §D.3.2 · pp. 33–34
• Driving-action constraints describe when a car may move forward, stop, or turn, conditional on lights, lane availability, following vehicles, and obstacles.The descriptions distinguish conditions for left and right turns, including lane markings and obstructions.Source: §D.3.2 · pp. 34–35
• The driving example contrasts simple proceed/stop rules with detailed conditions involving signals, obstacles, road clearance, and permitted maneuvers.The detailed version also distinguishes domain background facts from rules to encode.Source: §D.3.2 · p. 35
• The detailed object-matching description requires both objects to share shape and color and each to have exactly one of each, while the non-detailed version states only the matching requirement.Source: §D.3.2 · p. 36
• The sentiment example contrasts explicit label and tie rules—including a conflict label for tied positive and negative counts—with a majority-vote description and priority order.Source: §D.3.2 · pp. 36–37
• The autonomous-driving consistency task checks whether a detection’s agent class, location, actions, and traffic-light color tags satisfy a large set of compatibility and exclusivity rules.The non-detailed prompt introduces the dash-cam detection and its tags; the detailed version enumerates class, location, action, and color constraints.Source: §D.3.2 · pp. 37–39
• Constraint descriptions specify valid agent classes, actions, and locations, mutually exclusive traffic-light colours, and restrictions on combinations within a detection.They include rules such as allowing object-pushing only for pedestrians and disallowing invalid action-action or location-location combinations.Source: §D.3.2 · pp. 39–40

D.3.3 Variable lists

• Variable lists map indexed names to descriptions, covering task-specific labels and attributes as well as arithmetic and structured-output domains.The lists include, for example, medical findings and emergency codes, digit and product bits, and sentiment labels.Source: §D.3.3 · pp. 40–43

E Large Language Models

• The benchmark evaluates eight open-weight model families, with parameter counts from 8.2B to 117B, generally loaded unquantized in bfloat16.The gpt-oss-20b and gpt-oss-120b checkpoints use their native low-bit format; instruction-tuned models are selected when possible.Source: E Large Language Models · p. 44

F Prompts

• Prompt templates vary by dataset, output format, and ZS or ZS-CoT mode, and specify variable mappings, format-specific output rules, and self-correction.The shared self-correction protocol provides the original problem, proposed CNF, and error message, then requests [[OK]] or [[FIXED]] with a corrected formula when needed.Source: F Prompts · pp. 44–46

G LLMs Hyperparameters and Model Selection

• LLM evaluations allow five self-verification steps, use provider-recommended decoding settings, and set a uniform 32,768-token generation cap.Reasoning-tuned checkpoints retain their internal thinking traces.Source: G LLMs Hyperparameters and Model… · p. 46

H SPL and SL Model Selection

• The SPL and SL pipeline uses Adam and Bayesian optimization, then retrains selected configurations for 50 epochs across five seeds; SPL circuits are compiled from task CNFs and use an MLP gate head.Optimization searches learning rate, head width, and batch size; final test metrics use the final-epoch model and are reported as mean ± standard deviation.Source: H SPL and SL Model Selection · pp. 46–47
• Equivalent constraints can yield different compiled circuit structures and sumlayer parameter counts because CNF encodings differ, so hyperparameters are searched separately for each formula.Tseitin variables are existentially quantified during compilation, leaving the circuit over the ground-truth primary variables, but vtree and SDD size may still vary.Source: H SPL and SL Model Selection · p. 47
• Best SPL configurations are listed for ground-truth and LLM-predicted formulas, with datasets omitted when the LLM produced no valid formula.The listed configurations specify γ, ν, h, Adam, and backbone.Source: H SPL and SL Model Selection · pp. 47–48
• SL reused the same hyperparameters because of time constraints.The appendix directs readers to Section I.2.3 for the reused settings.Source: H SPL and SL Model Selection · p. 49

H.1 SPL Model Architectures

• SPL experiments pair each task with a backbone, ranging from scratch-trained CNNs and MLPs to frozen BERT and a Slowfast video model.For road-r, Slowfast processes 8-frame clips through slow and fast pathways whose features are concatenated for the SPL head.Source: §H.1 · pp. 49–50

I Additional Results

• The additional-results section reports further results and ablations for both stages of the auto-formalization pipeline.Source: I Additional Results · p. 50

I.1 Auto-Formalization

• The auto-formalization analysis covers input-level, model-level, output-level, and error-analysis components.Source: §I.1 · p. 51

I.1.1 Input-Level Analysis

• On auto-nesy-bench, a tenfold increase in variables is associated with an F1 decrease of 0.1986, while a tenfold increase in clauses corresponds to a decrease of 0.1391.Clause count is more informative among the 18 problems (R2 = 0.452 vs. 0.101), though the small sample warrants caution.Source: §I.1.1 · p. 51
• On dcpbench, slopes are −0.0947 for variables and −0.0845 for clauses; on satbench, they are −0.1921 and −0.1789, respectively.The reported fits explain roughly 28–30% of dcpbench variation; satbench fits also show declining F1 as formula size increases.Source: §I.1.1 · p. 51
• Across all three datasets, larger target formulas are associated with lower mean F1, but the magnitude varies by dataset.Figure 10 plots mean F1 against variable or clause counts on a log scale, with separate fitted lines and confidence intervals for each dataset.Source: §I.1.1 · p. 51
• The results suggest formula size may not fully capture problem complexity.Source: §I.1.1 · p. 51

I.1.2 Model-Level Analysis

• Selected prompting and output-format preferences differ by dataset, though high-level code formats predominate on auto-nesy-bench and dcpbench.Ten of eleven auto-nesy-bench models select ZS-CoT; all three satbench models select ZS-CoT with NAT.Source: §I.1.2 · p. 51
• On satbench, gemma4-31b achieves the highest F1 (0.992) with ZS-CoT and NAT; substantially lower best-configuration performance on dcpbench indicates reliable auto-formalization remains challenging for more difficult instances.Source: §I.1.2 · p. 53
• Best-configuration mean F1 rises from 0.455 to 0.692 on auto-nesy-bench, 0.183 to 0.297 on dcpbench, and 0.849 to 0.942 on satbench.The comparison selects each model’s best of ten prompt-and-format configurations; Table 16 reports the corresponding metrics.Source: §I.1.2 · p. 51, Table 16 · p. 53
• Larger models tend to perform better on auto-nesy-bench and dcpbench, but not satbench, and none of the fitted associations is statistically significant.The study cautions that the comparisons use only 11, four, and three models, respectively, and do not establish a general scaling law.Source: §I.1.2 · p. 56, Figure 11 · p. 57

I.1.3 Output-Level Analysis

• On auto-nesy-bench, CPMpy has the highest across-model mean F1 at 0.575, followed by SymPy at 0.549.CPMpy and SymPy improve mean F1 by approximately 0.19–0.21 over direct DIMACS generation.Source: §I.1.3 · p. 58
• The best format can vary by model even within auto-nesy-bench, where CPMpy and SymPy are strongest on average.For example, gpt-oss-120b performs best with CPMpy, while SymPy is best for several other competitive models.Source: §I.1.3 · p. 58
• On dcpbench, CPMpy has the highest mean F1 at 0.247, but the best format varies across individual models.The strongest model-level formats include SymPy for deepseek-r1-llama-70b and PySAT for gpt-oss-120b.Source: §I.1.3 · p. 58
• On satbench, NAT achieves the highest across-model mean F1 at 0.920, while gemma4-31b performs best with CPMpy.NAT is strongest for gpt-oss-120b and qwen-coder-next; gemma4-31b reaches 0.989 with CPMpy versus 0.979 with NAT.Source: §I.1.3 · p. 58
• No single output format consistently dominates across models and datasets; the strongest format depends on both.CPMpy and SymPy perform well on auto-nesy-bench and dcpbench, whereas NAT is substantially stronger on satbench.Source: §I.1.3 · p. 58

I.1.4 Syntactic Error Analysis

• On auto-nesy-bench, no_cnf_tags is most common at 17.4 occurrences, followed by execution_error at 15.9; mistral-nemo averages 7.3 errors per type.On satbench, qwen3-coder-next has 1,257 execution errors, while gpt-oss-120b has three errors total.Source: §I.1.4 · pp. 58, 61, Figure 13 · p. 60
• On auto-nesy-bench, CPMpy has the lowest format-level mean at 7.5 errors per type, while direct DIMACS has the highest at 8.4 despite the lowest syntax-error rate.On dcpbench, PySAT has the lowest average error count at 12.1; on satbench, DIMACS has the lowest mean at 2.6.Source: Figure 14 · p. 61, §I.1.4 · pp. 61–62
• Higher-level formats reduce manual encoding errors but can add code-execution, symbolic-conversion, and computational-cost errors.Error types differ by format across auto-nesy-bench, dcpbench, and satbench.Source: §I.1.4 · pp. 61–62, Figure 14 · p. 61

I.2.1 Downstream Results with Detailed Prompts on SPL

• Among detailed-prompt SPL missing results, five of thirteen errors arise from incorrect formulas; other cases involve no usable formula or SDD compilation failure.The incorrect formulas include examples from olmo3-32b-think and qwen3-8b.Source: Table 24 · p. 64, §I.2.1 · p. 64

I.2.2 What Happens When SPL Is Equipped with LLM-Generated Formulas from Less Detailed Prompts?

• Average ∆F1/∆recall with non-detailed prompts is −0.12/−0.10 for gpt-oss-120b, −0.15/−0.14 for olmo3-32b-think, and −0.14/−0.12 for qwen3-8b.The passage attributes the gap from detailed prompts mainly to non-equivalent formulas.Source: §I.2.2 · pp. 64–65, Table 25 · p. 66
• With non-detailed prompts, 10 of 14 missing SPL results stem from degenerate formulas, including formulas that omit task variables or are unsatisfiable.The qwen3-8b formula for mn-mul omits 45 of 102 variables.Source: §I.2.2 · p. 67, Table 29 · p. 68

I.2.3 What if the Constraints are Soft? Semantic Loss Downstream Results with Detailed Prompts

• SL adds a differentiable penalty for low probability mass on constraint-satisfying assignments to the task loss, rather than enforcing constraints in the prediction mechanism.The experiments combine the task loss and semantic loss with λ set to 1.Source: §I.2.3 · p. 68
• With detailed prompts and equivalent formulas, SL leaves mean ∆F1 between −0.00 and +0.02 while improving consistency on tasks with room for improvement.On sushi, consistency rises from 0.06 to 0.88–0.97.Source: Table 30 · p. 69, §I.2.3 · p. 69

I.2.4 Soft Constraints with Semantic Loss equipped with LLM-Generated Formulas from Less Detailed Prompts

• With non-detailed prompts, only 9/16 gpt-oss-120b, 7/12 olmo3-32b-think, and 6/13 qwen3-8b formulas are exactly correct for SL; strict and incomparable formulas often reduce consistency.Reported consistency drops include −0.29 to −0.53 on kand-logic-2 for all three models.Source: Table 36 · p. 72, §I.2.4 · p. 72
• With non-detailed prompts, SL's average consistency gain falls to +0.03 for gpt-oss-120b and qwen3-8b, and −0.02 for olmo3-32b-think; mean ∆F1 ranges from −0.04 to −0.01.SL remains more robust than SPL because it uses formulas as soft training signals rather than enforcing them on every prediction.Source: §I.2.4 · p. 73