NeurIPS 2026 — Evaluations & Datasets track (not the main track) LLM Evaluation scientific reasoning premise extraction formal verification controllable benchmark neuro-symbolic reasoning

SciR: A Controllable Benchmark for Scientific Reasoning in LLMs¶

Conference: NeurIPS 2026 — Evaluations & Datasets track (not the main track)
arXiv: 2606.13020
Code: https://github.com/idiap/scir
Area: LLM Evaluation
Keywords: scientific reasoning, premise extraction, formal verification, controllable benchmark, neuro-symbolic reasoning
Source version: arXiv v3, 2026-09-25

TL;DR¶

SciR generates verifiable deduction, induction, and causal-discovery problems before rewriting their premises as multi-document scientific discourse, separately varying inference complexity and premise obfuscation to diagnose LLMs; document formalisation remains a substantial bottleneck even with symbolic solvers.

Background & Motivation¶

Scientific reasoning requires more than domain knowledge: a system must extract evidence, align entities, distinguish observations from interventions, and apply valid inference rules. Formal reasoning benchmarks often provide exact answers but present premises as clean rule lists. Scientific question answering and literature verification use more realistic material, yet their answers often rely on human judgments and their reasoning burden cannot be adjusted independently. A wrong answer may therefore reflect either missed evidence or invalid reasoning over correctly extracted evidence, a distinction that a single leaderboard score obscures.

SciR grounds its three tracks in developmental-biology lineage logic, relation-rule induction over DrugBank background facts, and causal-structure recovery on the Sachs protein-signalling network. The scientific component primarily concerns domain vocabulary, problem structure, and document genres, rather than validation against real experimental records. The authors fix a formal object and its answer first, then use an LLM to distribute and rewrite its evidence as lab records, database entries, paper results, and other textual genres, producing clean and obfuscated versions of the same problem.

Core Idea: fix verifiable answers through formal objects, constrain scientific rewriting with a round-trip check, and evaluate on an “inference complexity × premise obfuscation” grid to distinguish weaknesses in evidence extraction from weaknesses in subsequent inference.

Method¶

Overall Architecture¶

SciR is a benchmark-generation and evaluation pipeline, not a new network, and it does not train the evaluated models. Its inputs are a task family and difficulty parameters; its outputs are multi-document problems with formal reference answers and scores for different solving architectures. The stages are formal task generation, scientific text rendering, and two-axis diagnostic evaluation. Reference answers support construction checks and scoring, not additional inputs to the evaluated model.

The diagram distinguishes offline construction from solving. Solid arrows carry tasks and answers; dashed arrows denote round-trip acceptance or scoring references. There is no training-supervision branch.

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["Task family and difficulty"] --> B["Formal task generation"]
    B --> C["Scientific text rendering"]
    B --> G["Formal reference answer"]
    C -.->|Keep after round-trip check| C
    C -->|Clean or obfuscated text| D["Two-axis diagnostic evaluation"]
    G -.->|Scoring reference| D
    D --> E["Extraction, inference, joint scores"]

Key Designs¶

1. Formal task generation: determine answers and inference burden before writing scientific text

The tracks share a latent-structure-first principle but use different correctness criteria. Deduction begins with syllogisms containing 2–3 premises and repeatedly replaces a premise with another syllogism's premises, building a proof tree whose intermediate conclusions must be recovered. Replacements must avoid new implications between variables already related in the tree. Keeping the conclusion produces True, negating it produces False, and removing a premise constructs Unknown. Unknown does not mean that an unstated fact is false: the available premises establish neither the hypothesis nor its negation.

To prevent solving by following only the most salient chain, the generator adds incomplete Unknown distractor trees with the same conclusion and instantiates predicates using vocabulary from 20 hand-curated developmental-biology contexts. Depth counts premise-expansion steps and increases proof burden; width counts distractor trees, increasing alternative paths while also diluting relevant information. The generator therefore offers separately adjustable axes, but this does not make the resulting cognitive demands perfectly orthogonal.

Induction asks for a rule explaining observed relations, rather than whether a particular entity pair has a relation. The generator samples a target rule and distractor rules, selects positives for each, and introduces one negative per distractor that activates the distractor but not the target. Background facts are restricted to predicates used by candidate rules, yet candidates still require consistency checks across dispersed relation facts and negatives. More distractor rules increase elimination burden; more positives per rule enlarge the background fact set.

The v3 scoring rule matters: an answer need not equal the generating target and need not cover every positive. The output is an unordered pair with repetition from nine relation types, represented in sorted order, with 45 possible pairs overall. Evaluation accepts all same-family rules that cover at least one positive and no negative. With background facts $F$, positive and negative examples $P,N$, and candidate rule $r$, the central acceptance condition can be expressed as:

\[ \operatorname{valid}(r)=\mathbf{1}\!\left[\exists p\in P:\ F\cup\{r\}\models p\right]\,\mathbf{1}\!\left[\nexists n\in N:\ F\cup\{r\}\models n\right]. \]

This equation restates the paper's verbal criterion; it is not a new training loss. The same-family constraint must also hold. The authors enumerate all 45 pairs to construct an answer pool and verify each using Popper restricted to that pair. Pools agree with solver-accepted rules on all 400 main induction tasks. The pool is a singleton for 131/200 Easy and 105/200 Hard tasks; the remaining pools contain at most four rules, with mean sizes of 1.43 and 1.58. Pool scoring avoids rejecting valid alternatives but makes this a restricted rule-explanation task, not unique mechanism discovery.

The causal track samples a connected Sachs subgraph, adds a fictional protein XYZ and random directed connections, and simulates observational and interventional concentrations using a linear Gaussian structural causal model. Given the existing subnetwork edges and data from different environments, the solver recovers XYZ's connections. A fictional entity reduces opportunities for answering from memorised biology. The data remain synthetic: recovering the correct edges does not validate a real biological mechanism. The appendix generator uses edge weights near 1, clips negative concentrations to zero, and simulates inhibition or activation through zero or high-value interventions.

Causal difficulty depends on subgraph size, the number of XYZ connections, and samples per environment. More samples strengthen statistical evidence in principle while lengthening the input table and increasing extraction burden, another concrete interaction between the axes. The main experiment is not unconstrained open discovery: it selects among candidate edge sets and retains tasks whose reference inputs can be solved by the construction-time solver.

2. Scientific text rendering: preserve recoverable information without equating scientific packaging with real evidence

A clean natural-language problem is split into chunks, each rewritten in one of eight document genres for its track. Deduction uses genres such as single-cell reports, developmental-biology results, and database entries; induction uses domain databases and research abstracts; causal discovery uses lab records, proteomics reports, and supplementary data. Obfuscation is not merely appended irrelevant text: quantifiers, entity relations, intervention conditions, or data rows are embedded within genre-specific prose, with distractors interleaved.

Each rewritten chunk must pass an inverse transformation. The inverse model receives the rewritten text and the other original chunks as context and attempts to recover the original structured chunk. Failure triggers retries; exhausting the budget discards the task. Deduction may use Prover9 to test first-order equivalence, while other cases use the specified structural matching criteria. Construction-time contextual anchors help recover names and cross-chunk references. At solve time, however, the evaluated model receives only the rewritten documents, not the original chunks, making cross-document alignment difficult.

This establishes an operational round-trip acceptance procedure, not an independent proof that the prose is unambiguous. Both renderer and inverse are o3-mini in the main experiment. A “second LLM” denotes a second role invocation, not an independent model. Retaining only chunks this model can invert may favour its familiar phrasing. Including the unrelated deepseek-r1 baseline addresses part of this concern but does not eliminate selection bias or prove fidelity of every scientific semantic implication.

Preservation constraints differ by track. Deduction prohibits formal-symbol hints and keeps entities recoverable; induction preserves protein categories and relation roles while banning rule-suggestive commentary; causal rendering preserves concentrations row by row, shuffles columns, and embeds known edges and interventions in prose. The main experiment uses two chunks for deduction and causal discovery, and three for induction. Rendering here means textual genre transformation, not image rendering, visual input, or a VLM task.

3. Two-axis diagnostic evaluation: replace inference with solvers to expose formalisation bottlenecks

Each track combines Easy/Hard with NL/Obf: the former changes the latent formal object, while the latter compares clean natural language with obfuscated scientific discourse. Deduction uses depths 4/5 and 1/2 distractor trees; induction uses 2/3 distractor rules and two positives per rule; causal discovery uses 5/6-node subgraphs and 1/2 XYZ connections. Answer spaces differ across tracks, so raw percentages should not be interpreted as scores on equally difficult tasks.

Three solving architectures serve different roles. CoT reasons directly from task text. The neuro-symbolic pipeline, NS, uses an LLM to formalise inputs and then invokes Prover9, Popper, or GIES. SymbCoT shares NS's formalisation step but uses a second LLM call to answer from the formal text instead of executing a symbolic solver. Comparing NS with SymbCoT tests whether gains mainly come from the solver rather than symbolic formatting alone, although unfamiliarity with Prolog also affects the latter.

NS retries only on syntax or parsing errors, with at most two retries and three formalisation attempts in total; it never receives correct-answer feedback. CoT has no retries. SymbCoT* performs one formalisation-and-answer pass, involving two calls rather than iterative correction. Induction is scored against the answer pool. Causal GIES outputs are mapped to options, allowing a subset match when the discovered graph strictly contains an option's edge set. Consequently, main-experiment causal NS accuracy is not open-answer exact whole-graph recovery accuracy.

The diagnostic probes are NL·CoT for inference, Obf·NS for extraction and formalisation, and Obf·CoT for their joint demands. These are operational proxies: clean text still requires parsing, and formalisation itself requires reasoning, so they do not independently measure two isolated cognitive abilities. Cross-track summaries use chance-normalised accuracy, clipping below-chance results to zero:

\[ A_{\mathrm{norm}}=\max\!\left(0,\frac{A_{\mathrm{raw}}-c}{1-c}\right). \]

Both $A_{\mathrm{raw}}$ and $c$ use the 0–1 scale. Chance is 1/3 for deduction, 3.2%/3.5% for Easy/Hard induction, and 10%/5% for causal discovery. Induction chance is the expected fraction of random relation pairs accepted by the answer pool, not simply 1/45. The paper's main table reports raw accuracy; figures and diagnostic summaries report chance-normalised scores. These must remain distinct.

Key Experimental Results¶

Main Results¶

Six base models are evaluated through OpenRouter on 200 tasks per cell, with temperature 0 passed to the API; reasoning models can still sample internally. The table excerpts the Hard tier of Table 1. Values are raw accuracy percentages, with each cell showing NL → Obf, not chance-normalised scores.

Model	Architecture	Deduction Hard	Induction Hard	Causal Hard
gpt-4o	CoT	54.0 → 33.5	28.0 → 25.5	46.0 → 33.0
gpt-4o	NS	97.0 → 43.0	73.5 → 40.5	98.0 → 78.5
o3-mini	CoT	52.5 → 23.5	45.5 → 39.5	85.5 → 70.5
o3-mini	NS	99.0 → 67.0	74.0 → 51.0	92.0 → 97.0
deepseek-r1	CoT	93.0 → 56.5	91.5 → 26.0	88.5 → 85.5
deepseek-r1	NS	98.0 → 73.5	84.5 → 69.0	69.0 → 75.0
llama-3.3-70b	CoT	42.5 → 30.0	17.5 → 18.5	33.0 → 23.0
llama-3.3-70b	NS	88.5 → 48.0	67.5 → 39.0	97.0 → 80.5
qwen3-30b	CoT	80.0 → 39.0	44.0 → 16.0	44.5 → 49.5
qwen3-30b	NS	77.5 → 58.5	41.5 → 38.5	91.5 → 70.5
olmo-3.1-32b	CoT	49.5 → 30.0	36.0 → 23.5	4.0 → 11.0
olmo-3.1-32b	NS	82.0 → 38.5	19.5 → 17.5	44.0 → 24.0

gpt-4o's deduction NS accuracy falls from 97.0% to 43.0%, showing that a correct solver cannot automatically repair incorrect inputs. deepseek-r1's induction CoT falls from 91.5% to 26.0%, showing that evidence presentation can undermine strong reasoning. Several causal cells improve after obfuscation, however. The claim that obfuscation hurts every model is an aggregate trend, not a decrease in every individual cell.

Ablation Study¶

This analysis varies presentation and solving architecture, not trained modules. The table uses Table 2 and reports average Hard-tier input characters and items extracted by gpt-4o NS. Items are first-order clauses, induction background facts, and causal data rows respectively.

Track	Input characters NL → Obf	Gold items	Extracted items NL → Obf	Observable issue
Deduction	3.2k → 9.4k	32.8	33.9 → 39.2	Above-gold counts may include spurious premises
Induction	8.2k → 23k	142.9	122.3 → 48.5	Many facts are not formalised after obfuscation
Causal	4.1k → 17k	64.0	64.0 → 50.7	Narrative presentation loses data rows

Item counts are not extraction precision or recall: duplicates, incorrect entities, and incorrect relations can also contribute to them. They support missing evidence and spurious premises as real failure modes but cannot establish complete extraction correctness. SymbCoT* induction also shows that formalisation is not a universal improvement: gpt-4o obtains only 10.5% on Easy·NL, versus 46.0% with direct CoT.

v3 adds a GPT-5.4 frontier-model check with high reasoning effort and 50 tasks per setting. It is separate from the six-model main experiment's 200-task cells.

GPT-5.4 setting	Correct	Experimental boundary
Deduction Hard·Obf	49/50	Direct CoT, scientific textual presentation
Induction Hard·Obf	25/50	Answer-pool scoring
Induction Hard·NL	50/50	Same tasks as the preceding row
Causal Hard·Obf	50/50	Main-experiment multiple-choice format
Causal full Sachs graph·NL	30/50	11 proteins, 19 known edges, 5 XYZ edges, open exact answer

Key Findings¶

The two-axis effects compound: gpt-4o CoT's cross-track chance-normalised means are 42.6 for NL Easy, 33.2 for NL Hard, 30.1 for Obf Easy, and 17.5 for Obf Hard. These means are not directly comparable with the raw percentages above.
Reasoning-model advantages lean more toward inference, but o3-mini also renders and inverts the text, creating selection-bias risk for its extraction scores. NS performance depends on formalisation quality and task interfaces.
Frontier models have not invalidated every task: GPT-5.4 scores 25/50 on rendered induction and 50/50 on the clean version. On the 25 singleton-answer tasks, scores are still 8/25 versus 25/25, so answer ambiguity cannot explain the gap.
The expanded causal check changes both graph size and answer format; 30/50 is not a pure inference-complexity ablation. The main experiment also lacks multi-seed error bars.

Highlights & Insights¶

Paired versions of the same task probe reasoning and scientific-document formalisation rather than comparing unrelated test sets. This supports studying where multi-pass extraction or entity-consistency checks actually help.
Induction answer pools accept valid alternative rules while requiring exclusion of every negative. This better matches evidence-conditioned rule explanation than matching only the generating target.
Releasing a generator is useful when model capabilities keep changing. Difficulty can increase, but answer spaces, chance baselines, and reference-solver solvability must be checked again after changes.

Limitations & Future Work¶

Real scientific documents rarely contain such clean latent formal objects, and each reasoning mode uses only one domain surface. Results do not establish real literature-discovery capability or biological validation of synthetic causal recovery.
There is no equally complex non-scientific-text control, leaving length, cross-document alignment, and scientific-genre effects partly entangled. A useful extension would match facts, length, and chunking across scientific and non-scientific presentations.
Renderer and inverse use the same model, and inversion receives extra original context. Stronger validation could use independent models, item-level entity/relation checking, and human review of rewriting ambiguity.
Main evaluation is a single run with 200 tasks per cell. Temperature 0 does not guarantee internally deterministic reasoning models. The authors report roughly US$1,500 in API costs without measuring run-to-run variance.
A qualification is needed for a source inconsistency: the text says joint scores are always below both single-axis scores, but deepseek-r1's chance-normalised causal Easy joint score is 100.0, exceeding inference at 99.4 and extraction at 88.9. The claim therefore does not hold cell by cell.
Failure analysis says it samples 30 failed traces per track, but the deepseek-r1 causal table lists 29 reasoning and 0 extraction errors, totalling 29. No missing category is invented here. Induction error categorisation also uses success on the clean version as a control, rather than directly identifying extraction errors from traces alone.

vs ProofWriter / FOLIO / SylloBio-NLI: These provide logical answers or biomedical vocabulary. SciR adds multi-genre, multi-document evidence and adjustable presentation difficulty; it is not the first formal-logic evaluation benchmark.
vs SciFact / GPQA / DiscoveryBench: Real scientific material and open discovery are closer to practical work. SciR trades some realism for verifiable answers and parametric control, making the approaches complementary rather than interchangeable.
vs BABILong / GSM-∞: Irrelevant content and length perturbations have precedents. SciR's distinction is their combination with three inference families and domain-tuned scientific genres, not two-axis control without precedent.
vs Logic-LM / LINC / SymbCoT: Solvers and symbolic representations can strengthen inference, but formalising inputs is not free. Evidence-provenance checks between round-trip validation and NS inputs could prevent a correct backend from masking incorrect evidence.

Rating¶

Novelty: 4/5 — A valuable combination of three scientific inference types, multi-document genres, and two-axis generation control.
Experimental Thoroughness: 4/5 — Broad coverage of six models, three architectures, and a frontier check, but no repeated runs or non-scientific control.
Writing Quality: 4/5 — Substantial method and appendix detail, with absolute claims and failure-count boundaries requiring clarification.
Value: 4/5 — Useful for diagnosing scientific-text formalisation, but not sufficient evidence of real scientific-discovery capability.