pith. sign in

arxiv: 2604.07496 · v1 · submitted 2026-04-08 · 💻 cs.LO

SMT with Uninterpreted Functions and Monotonicity Constraints in Systems Biology

Ond\v{r}ej Huvar , Martin Jon\'a\v{s} , Samuel Pastva This is my paper

Pith reviewed 2026-05-10 17:15 UTC · model grok-4.3

classification 💻 cs.LO
keywords SMTuninterpreted functionsmonotonicity constraintssystems biologymodel inferencequantifier instantiation
0
0 comments X

The pith

SMT with uninterpreted functions under monotonicity constraints outperforms specialized tools for inferring biological models

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that model inference for biological systems can be encoded as satisfiability problems over uninterpreted functions whose inputs have fixed positive or negative effects on outputs. It compares a naive quantified encoding against eager and lazy instantiation of a finite set of monotonicity lemmas, finding that the instantiation approaches scale better on large arities and complex cases. The key demonstration is that these SMT encodings run faster than the leading domain-specific solvers on a large suite of systems biology benchmarks. This matters because model inference is a bottleneck when reverse-engineering regulatory networks from partial observations.

Core claim

The central claim is that SMT solvers using uninterpreted functions with monotonicity constraints, encoded via eager or lazy instantiation of quantifier-free lemmas, significantly outperform both quantified SMT encodings and the existing ASP-based and BDD-based tools when solving model inference problems drawn from systems biology.

What carries the argument

Uninterpreted functions equipped with monotonicity constraints, where each input is required to have a consistently non-decreasing or non-increasing effect on the function value; these constraints are compiled into a finite collection of quantifier-free lemmas that are either all added upfront or introduced on demand during solving.

If this is right

  • Instantiation-based SMT encodings succeed on instances with high-arity functions where fully quantified formulas fail.
  • The same monotonicity encoding yields faster runtimes than the leading specialized solvers across the tested biology benchmarks.
  • Lazy introduction of lemmas provides a practical middle ground between eager instantiation and full quantification.
  • General-purpose SMT technology becomes competitive for a core task in computational systems biology.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same lemma-instantiation technique could be reused in any domain where components are known to be monotonic but otherwise unknown.
  • Hybrid systems could feed SMT-derived models back into biology simulators for further validation or parameter tuning.
  • If monotonicity lemmas can be learned from data rather than supplied, the method might extend to partially observed or noisy networks.

Load-bearing premise

The biological components being modeled really obey the assumed monotonicity rules and the benchmark collection reflects the size and structure of problems that arise in practice.

What would settle it

A collection of model inference instances from real biological data on which the SMT instantiation methods require more time or memory than the ASP or BDD baselines.

read the original abstract

The theory of uninterpreted functions is a key modeling tool for systems with unknown or abstracted components. Some domains such as systems biology impose further restrictions regarding monotonicity on these components, requiring specific inputs to have a consistently positive or negative effect on the output. In this paper, we tackle the model inference problem for biological systems by applying the theory of uninterpreted functions with monotonicity constraints. We compare the performance of naive quantified encodings of the problem and the performance of the existing approach based on eager quantifier instantiation, which is based on the fact that a finite set of quantifier-free monotonicity lemmas is sufficient to encode the monotonicity of uninterpreted functions. Additionally, we consider a lazy variant of the approach that introduces the monotonicity lemmas on demand. We evaluate the SMT-based approach to model inference using a large collection of systems biology benchmarks. The results demonstrate that the instantiation-based encodings significantly outperform quantified encodings, which typically struggle with large function arities and complex instances. As the key result, we show that our approach based on SMT with uninterpreted functions and monotonicity constraints significantly outperforms state-of-the-art domain-specific tools used in systems biology, such as the ASP-based Bonesis and the BDD-based AEON.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper applies SMT with uninterpreted functions (UF) augmented by monotonicity constraints to the model inference problem in systems biology. It compares naive quantified encodings of the problem against eager quantifier instantiation (using a finite set of quantifier-free monotonicity lemmas) and a lazy on-demand variant. The evaluation on a large collection of systems biology benchmarks shows that instantiation-based encodings outperform quantified ones on large-arity and complex instances, and that the overall SMT+UF+monotonicity approach significantly outperforms the ASP-based tool Bonesis and the BDD-based tool AEON.

Significance. If the benchmarks prove representative and the monotonicity assumptions hold for the modeled components, the work would establish SMT as a competitive, general-purpose engine for biological model inference, extending standard SMT theory (UF + monotonicity lemmas) to a new domain without circularity or ad-hoc axioms. The use of external benchmarks and standard theory is a clear strength.

major comments (1)
  1. [Evaluation] Evaluation section: the headline claim that SMT with UF and monotonicity constraints 'significantly outperforms' Bonesis and AEON rests on an undescribed benchmark suite. No information is supplied on benchmark origins, instance sizes, selection criteria, whether monotonicity was verified for the underlying biological components, sensitivity analysis with monotonicity constraints removed, or statistical tests. This directly undermines the central empirical result.
minor comments (2)
  1. [Approach] The distinction between the eager and lazy instantiation strategies would benefit from a small pseudocode fragment or explicit complexity remark in the approach section.
  2. [Abstract] The abstract should report the number of benchmarks, the primary performance metric (e.g., solved instances within timeout), and the hardware/time limits used.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive feedback and the positive assessment of our work's significance. We address the major comment on the evaluation below and commit to revising the manuscript to incorporate the suggested improvements.

read point-by-point responses

  1. Referee: [Evaluation] Evaluation section: the headline claim that SMT with UF and monotonicity constraints 'significantly outperforms' Bonesis and AEON rests on an undescribed benchmark suite. No information is supplied on benchmark origins, instance sizes, selection criteria, whether monotonicity was verified for the underlying biological components, sensitivity analysis with monotonicity constraints removed, or statistical tests. This directly undermines the central empirical result.

    Authors: We agree that the manuscript would benefit from a more detailed description of the benchmark suite to support the central claims. In the revised version, we will add information on the origins of the benchmarks, their instance sizes, and the selection criteria used. We will also clarify that the monotonicity constraints are based on domain knowledge for the biological components. Furthermore, we will include a sensitivity analysis by reporting results with monotonicity constraints disabled and add statistical tests to the performance comparisons. These additions will be included in the updated manuscript. revision: yes

Circularity Check

0 steps flagged

No circularity: empirical outperformance on external benchmarks uses standard SMT theory without self-referential reduction.

full rationale

The paper's central claim is an empirical result: SMT encodings with uninterpreted functions and monotonicity constraints outperform Bonesis and AEON on a collection of systems biology benchmarks. This rests on runtime measurements treated as independent inputs, not on any derivation that reduces a 'prediction' or theorem to fitted parameters, self-defined quantities, or a self-citation chain. The abstract references standard facts about quantifier instantiation and monotonicity lemmas without redefining them via the present work; no equations or steps equate outputs to inputs by construction. The evaluation is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on the standard property that monotonicity of uninterpreted functions can be captured by a finite set of quantifier-free lemmas; no free parameters, new entities, or ad-hoc axioms beyond this domain assumption.

axioms (1)
  • domain assumption A finite set of quantifier-free monotonicity lemmas is sufficient to encode the monotonicity of uninterpreted functions
    Explicitly invoked as the basis for the eager instantiation approach in the abstract.

pith-pipeline@v0.9.0 · 5526 in / 991 out tokens · 47489 ms · 2026-05-10T17:15:24.823111+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 2 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Inference of Qualitative Models from Steady-State Data via Weighted MaxSMT

    q-bio.MN 2026-05 unverdicted novelty 7.0

    Weighted MaxSMT enables robust inference of qualitative biological models from uncertain steady-state data on networks of 200-1300 genes.

  2. Inference of Qualitative Models from Steady-State Data via Weighted MaxSMT

    q-bio.MN 2026-05 unverdicted novelty 7.0

    Weighted MaxSMT enables robust inference of qualitative biological models from uncertain steady-state data by relaxing conflicting observations as soft constraints.

Reference graph

Works this paper leans on

2 extracted references · 2 canonical work pages · cited by 1 Pith paper

  1. [1]

    Repository of logically consistent real-world boolean network models.bioRxiv, pages 2023–06,

    16 Samuel Pastva, David Šafránek, Nikola Beneš, Luboš Brim, and Thomas Henzinger. Repository of logically consistent real-world boolean network models.bioRxiv, pages 2023–06,

    work page 2023

  2. [2]

    Hierarchical reasoning in local theory extensions and applica- tions

    19 Viorica Sofronie-Stokkermans. Hierarchical reasoning in local theory extensions and applica- tions. In Franz Winkler, Viorel Negru, Tetsuo Ida, Tudor Jebelean, Dana Petcu, Stephen M. Watt, and Daniela Zaharie, editors,16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2014, Timisoara, Romania, September 22-...

    work page doi:10.1109/synasc.2014.13 2014