布尔基因调控网络单调调控条件的推理：一种算法方法

《Journal of Computational Science》：Reasoning about monotonic regulation conditions for Boolean Gene Regulatory Networks: An algorithmic approach

　　

# 摘要

基因调控网络（GRNs）决定基因之间如何相互作用和调节彼此，以控制生物体内的各种生物学过程。GRN 的每个组件都可能受到网络中其他组件的调节，这些组件被称为调节因子，其总体效果由一种调节函数决定。在本文中，我们研究了布尔网络（一种用于 GRN 建模的成熟形式化方法）中调节函数的可能形式。交互网络推理引擎（RE:IN）是一种基于形式验证的强大方法，已被有效用于研究发育和干细胞系统中各种 GRN 的布尔网络模型。由于其有效使用，我们对理解其关于调节函数的假设（单调性、按组对称性、一阶逻辑）以及扩展其能力产生了兴趣。我们将布尔网络中调节函数的发现问题归结为识别一种矩阵表示的问题。利用这一表示，我们研究了计数调节函数的方法，为目前已支持的方法提供了简单证明，并提出了一种系统方法，将其扩展到处理不支持的生物学情况（例如弱-强分组、阈值函数）。通过分析 Biodivine 布尔模型（BBM）库——一个由研究社区开发的布尔网络集合，我们支持了单调性假设在生物布尔网络中的有效性，识别了当前支持的调节函数带来的局限性，并展示了弱-强分组扩展对布尔网络的相关性。我们还提出了一种线性时间算法用于调节函数的识别，假设可以控制组件的敲除和过表达。基于这些扩展，我们开发了一个原型工具，纳入广义调节函数用于建模和研究复杂的 GRN。利用新开发的形式化方法，我们设计了一个最优实验设计框架，以揭示 GRN 的相互作用，在假设组件调节函数已知的情况下，以线性时间实现最优推断。

# 引言

理解控制细胞分化、发育和功能的调控过程具有重要意义。基因调控网络（GRNs）控制基因表达动力学，从而决定细胞功能。这些网络描述了细胞组分之间的相互作用。在许多情况下，GRN 通过构建能够捕获系统行为的数学模型进行研究。这些模型能够生成细胞行为的预测，这些预测可用于推荐体内实验，而这些实验可能最初未被考虑。预测随后可以被测试并证明是准确的或不准确的，在这种情况下需要对模型进行改进。利用这些模型的特征，可以推断和阐明控制 GRN 的机制和相互作用。

布尔网络[1]是计算建模中的一个重要框架，通常用于对 GRN 等生物系统中的复杂行为进行建模。布尔网络的行为由布尔更新函数决定，而在许多情况下，这些函数可能无法被完全确定。这可能是由于模糊性造成的，例如数据有限或不一致，或者涉及基因突变的实验控制存在困难。

GRN 的布尔网络中，每个组件代表一个基因、转录因子或信号，在任何时间点可以是激活（True）或失活（False）。这些组件由一个逻辑函数进行更新，该函数依赖于其他调节组件，可以视为两个组件（gi 和 gj）之间的相互作用，其中组件 gi 激活或抑制 gj。

布尔网络可以进一步推广为抽象布尔网络（ABN）[2]，它允许指定部分已知的布尔网络，其中一些相互作用被标记为"可能的"，逻辑布尔更新函数可能不完全确定。ABN 可以通过实验结果进一步约束，从而允许预测和分析不完全已知的生物系统结构和行为。这些受约束的网络称为受约束的抽象布尔网络（cABN）。

有多种工具用于 GRN 分析。其中一种方法是综合 GRN 模型，然后利用形式验证工具识别潜在的相互作用。交互网络推理引擎（RE:IN）[2], [3], [4] 是一个用于将逻辑模型合成为生物程序并分析它们的自动化推理框架。它支持利用 Z3 可满足性模块化理论（SMT）求解器[5]进行形式推理过程，以合成 cABN，这些 cABN 不仅受实验数据约束，还受一组限制布尔更新函数结构的调节条件约束。这些调节条件使用单调性假设、更新函数上激活子和抑制子的对称性假设，以及每个调节条件都可以用一阶逻辑（FOL）表示的思想来创建。这些假设通过其简洁性赋予布尔模型解释力。

此类方法的自动化和计算效率使得能够有效构建和修订调控网络模型，直到获得足够好的模型，并利用该组模型进行可测试的预测[6], [7]。这种建模方法简洁性的另一个优势是模型的可解释性，这得益于所采用的易于理解的假设。然而，调节条件约束可能过度简化 GRN 行为，因为某些 GRN 不符合这些假设。为了将覆盖范围扩展到额外的 GRN，我们在此将对称性假设扩展为按组对称性假设。这种扩展在保持模型简洁性和可解释性的同时推广了模型。

在本工作中，我们提出了生成和枚举 RE:IN 中所用调节条件的方法，为目前支持的方法提供了简单证明，并提出了一种系统方法将这些调节条件扩展以处理更复杂的生物学情况。通过利用我们的方法分析研究社区开发的布尔网络数据库[8]，我们支持了单调性假设在 GRN 布尔网络中的有用性以及扩展调节函数的需求。

nuXmv[9] 是一个开源符号模型检查器，用于有限状态和无限状态系统的形式验证，在本工作中被用于分析布尔网络。它在著名的 NuSMV 工具[10]的基础上扩展了高级验证引擎，包括基于二元决策图（BDD）[11]、可满足性（SAT）[12], [13] 和 SMT[5] 的技术，从而提高了可扩展性和表达能力。该工具支持标准时序逻辑，如计算树逻辑（CTL）和线性时序逻辑（LTL）[14]。通过与 SMT 求解器的集成，它允许对更丰富的领域进行推理。得益于这些能力，nuXmv 已被广泛应用于硬件、软件和通信协议的验证中，在这些领域中必须确保关键系统的正确性。在此，它被用于分析带有实验约束的 GRN 的 cABN 的潜在解决方案。

本工作的简短版本作为"网络分析基础国际研讨会"的一部分发表在 2025 年 IEEE 生物信息学与生物医学国际会议（BIBM 2025）论文集[15]上。本手稿显著扩展了初步研究，引入了算法 6，展示了我们的建模框架在实际布尔网络中的适用性。此外，在第 8 节中，我们详细介绍了一种用于识别所提出的调节条件的线性时间算法。最后，第 9 节提出了一种基于这些调节条件的最优实验设计方法，提供了一个适用于湿实验实验的框架。

# 相关工作

GRN 控制基因表达的动态并决定细胞决策。这些网络由细胞中负责基因表达调控的组件组成，并描述它们之间的激活和抑制相互作用。有许多计算方法和形式化方法用于利用实验数据对 GRN 进行建模和推理，参见[16], [17]及其参考文献。

## 布尔网络

布尔网络是相互作用组件系统的数学模型。每个组件可以被赋予真（1）或假（0）的值。该状态由一个布尔函数决定，通常称为调节函数，f: B^n → B，其输入由网络组件组成。这些函数考虑了组件之间的相互作用。

在大多数情况下，组件之间的相互作用没有被完全确定，导致与布尔布尔函数层级有关的方面存在不确定性。

## 布尔函数层级

在 GRN 建模中，并非所有布尔函数都是合理的。许多函数过于复杂，在实践中不会出现，因此对特定网络中常见的小型布尔函数子集进行分类具有研究价值。在 GRN 的情况下，本文检查并定义的子集是单调的、对称的以及按组对称的布尔函数。

**符号说明：** 对于 n 个变量的布尔函数，我们写作：f(x_{n-1},…,x_{i+1}, x_i=k, x_{i-1},…,x_0) = f|_{x_i=k}

## 调节条件形式化

RE:IN 对表示组件相互作用的布尔更新函数做出了三个假设。第一个假设是它们是单调的，即一个激活的组件不会变失活，如果其一个激活子从失活变为激活（假设其他调节因子没有变化），反之亦然。第二个假设是对于给定的组件，激活子组和抑制子组都是两两对称的。这是按组对称性的特殊情况，其中 k=2。

## 真实世界的布尔模型

为了分析和理解系统生物学中使用的布尔调节函数类型，我们利用了 Biodivine 布尔模型（BBM）基准数据集[8]。BBM 是一个开源的布尔模型数据集，从主要模型库以及单独论文中编译而来，并经过完整性验证。BBM 旨在作为基准，可用于测试新工具和方法。

如前所述，我们假设调节函数是单调的。

## 扩展调节条件

由于我们希望扩展激活子和抑制子的级别以模拟更复杂的 GRN，我们可以使用 n×m 表，其中 n 行表示不同级别的激活子，m 列表示不同级别的抑制子。

为了定义一个新的公式来找到 n×m 表的所有分配，我们首先检查行数或列数不超过三行的表格公式。

**一行：** 对于 1×1 表，有两种分配（0 和 1）。对于 1×2 和 1×3 表，分别有三种和…

## 发现调节条件

如前所述，每个调节条件都可以描述为一个由零和一组成的矩阵，其大小取决于已知的组数。每个调节条件都有一个唯一的矩阵编码（在已知假设下，如一阶逻辑或阈值），因为这是一对一编码。

由于我们知道调节条件可以用矩阵表示，我们希望识别矩阵以识别调节条件。矩阵的每个元素都可以在运行后被发现…

## 利用调节条件进行最优实验设计

在发现生物网络中的相互作用时，主要挑战之一是所需的实验数量。给定一个具有 M 个可能激活子和 N 个可能抑制子的网络组件，在最坏情况下，需要执行 O(2^{N+M}) 次实验才能发现所有可能的相互作用。这是由于发现所有状态需要设置输入为敲除（KO）或过表达（OE），因此在 M+N 个抑制子和激活子中，我们必须考虑所有 2^{N+M} 种组合。

在此…

## 实现

我们使用 Python 和 nuXmv[9] 实现了第 7 节中的形式化方法。交互式 Python 工具[49]接收一个文本文件作为输入，该文件概述了网络组件、相互作用、状态和描述 cABN 的实验。然后根据此输入文件综合一个网络。该工具可以以两种模式使用：(i) "Rein"，即 RE:IN 中的 18 种调节条件，以及 (ii) "扩展（矩阵）"，即带有 9×9 表的弱-强设置。当使用扩展的调节条件时…

## 总结

在本工作中，我们研究了作为定义布尔网络中逻辑调节函数模板的调节条件的形式化规范。我们的方法从 RE:IN 框架中原始定义的调节条件集开始，并扩展了该表述以涵盖更广泛的复杂调控模式。这些调节条件提供了 GRN 的简洁但强大的表示，既便于直观解释，又…

# CRediT 作者贡献声明

Yuval Gerber：撰写初稿、软件、形式分析、概念化。Michelle Aluf-Medina：撰写初稿、软件、形式分析。Ori Ratzon：软件、形式分析。Leeshay Elimelech：软件、形式分析。Hillel Kugler：撰写初稿、监督、资金获取、形式分析、概念化。

# 披露声明

作者们完全负责开发研究问题、设计方法论、进行分析和解释研究结果。我们使用 ChatGPT（OpenAI）来帮助改进写作的清晰度和风格，而未影响研究的任何实质性方面。

我们监控了大语言模型的输出，以防止对内容进行任何实质性修改，仅将其限制在语法或结构方面的改进范围内。利益冲突声明：作者声明，他们不存在任何已知的相互竞争的经济利益关系或个人关系，这些关系可能会影响本文所报告的研究工作。致谢：本研究由以色列科学基金会（资助编号：190/19）和巴伊兰大学数据科学研究所（种子基金）资助。Yuval Gerber | Michelle Aluf-Medina | Ori Ratzon | Leeshay Elimelech | Hillel Kugler