什么是 ‘Knowledge Consistency Checking’：利用确定性算法验证 LLM 生成的多个事实之间是否存在数学冲突

各位同仁，各位专家，大家下午好！

今天，我们齐聚一堂，共同探讨人工智能领域一个至关重要且日益紧迫的话题——大型语言模型（LLM）生成知识的可靠性。LLM的崛起无疑是近年来AI领域最激动人心的进展之一。它们凭借庞大的参数量和海量的训练数据，展现出令人惊叹的文本生成、问答、代码编写乃至创意写作能力。它们正在深刻改变我们获取信息、处理任务的方式。

然而，伴随其强大能力而来的，是对其生成内容真实性与一致性的担忧。LLM偶尔会“幻觉”（hallucination），生成听起来合理但实际上错误或捏造的信息。更微妙也更具挑战性的是，即使LLM生成的单个事实在孤立看来是正确的，当这些事实组合在一起时，它们之间也可能存在矛盾。尤其是在涉及数量、关系、逻辑推理等需要严谨性的领域，这种内部不一致性（internal inconsistency）可能导致严重的后果。

这就是我们今天讲座的核心主题：“Knowledge Consistency Checking (KCC)”，即知识一致性检查。更具体地，我们将聚焦于如何利用确定性算法，系统地验证LLM生成的多个事实之间是否存在数学或逻辑冲突。我们将深入探讨这一概念，分析其重要性，剖析其实现机制，并通过具体的代码示例，展示如何在实践中构建这样的检查系统。

1. 什么是知识一致性检查 (KCC)?

首先，我们来明确一下什么是知识一致性检查。

知识一致性检查 (Knowledge Consistency Checking, KCC) 是一种旨在识别、定位并（在可能的情况下）纠正知识库或信息集合中矛盾或不一致的方法。对于LLM而言，KCC的目标是评估LLM所生成或提取的知识片段是否自洽，是否遵循基本的逻辑和数学原理。

KCC的目标可以概括为：

• 识别冲突：发现由LLM生成的两个或多个事实之间存在的直接或间接矛盾。
• 定位源头：指出导致冲突的具体事实或推导链。
• 提升可靠性：通过检测和报告不一致性，帮助用户或下游系统避免基于错误信息做出决策，从而增强对LLM输出的信任度。

KCC可以从两个主要维度进行分类：

1. 外部一致性检查：将LLM生成的事实与外部的、被认为是权威的知识源（如数据库、知识图谱、维基百科等）进行比对。这类似于“事实核查”。
2. 内部一致性检查：检查LLM自身生成的多个事实之间是否存在矛盾，而无需依赖外部知识源。这正是我们今天讲座的重点。我们假设LLM生成了一组事实，我们的任务是判断这组事实本身是否在逻辑上和数学上是自洽的。

为什么内部KCC对LLM至关重要？

• 信任与可信度：一个经常自相矛盾的系统是不可信的。KCC有助于建立和维护用户对LLM输出的信任。
• 下游应用安全：在金融分析、医疗诊断、工程设计等领域，基于不一致信息做出的决策可能带来灾难性后果。KCC是保障这些应用安全的关键一环。
• 调试与改进LLM：通过分析KCC发现的冲突模式，可以反过来指导LLM的训练和微调，使其生成更准确、更一致的知识。
• 复杂推理的基础：许多复杂的推理任务需要多个事实的组合。如果这些基本事实本身就不一致，那么任何基于它们进行的推理都将是不可靠的。

2. 确定性算法在KCC中的核心作用

在进行数学和逻辑冲突检查时，我们对算法的选择有着严格的要求。我们不是在寻找“可能”的冲突，而是在寻找“确实存在”的冲突。这就引出了确定性算法的核心作用。

什么是确定性算法？

一个确定性算法在给定相同的输入时，总是会产生相同的输出，并且其每一步的执行路径都是唯一确定的。它没有随机性，也没有模糊性。

确定性算法的特点：

• 可重复性 (Reproducibility)：每次运行，结果都一样。
• 可验证性 (Verifiability)：每一步都可以被逻辑推导和验证。
• 精确性 (Precision)：对于数值计算和逻辑判断，产生精确的结果。

为什么确定性算法更适合数学和逻辑验证？

考虑一下数学计算：2 + 3 总是等于 5。我们不希望一个验证系统有时说 2 + 3 = 5，有时又说 2 + 3 = 6。模糊的、概率性的或启发式的算法可能在某些情况下表现良好，但在需要绝对准确性的数学和逻辑验证中，它们是不可接受的。确定性算法为我们的KCC系统提供了坚实、可靠的基础。

确定性算法在KCC中的应用场景：

1. 数据提取与标准化：将LLM生成的自然语言转换为结构化数据，需要确定性的解析规则和单位转换逻辑。
2. 事实表示：将结构化数据转换为统一的、可计算的表示形式（如数学表达式树、逻辑命题）。
3. 冲突检测规则：定义数学公理、逻辑推理规则，这些规则本身就是确定性的。
4. 数学运算和逻辑推理：执行加减乘除、比较、集合操作、布尔逻辑判断等，这些都是确定性操作。
5. 约束求解：利用确定性的算法（如SAT/SMT求解器、线性规划求解器）来检查一组事实是否满足所有约束。

接下来，我们将逐步深入，从LLM生成事实的提取与标准化开始，构建一个完整的KCC框架。

3. LLM生成事实的提取与标准化

KCC的第一步，也是至关重要的一步，是从LLM生成的自然语言文本中提取出结构化的、可计算的事实。自然语言的丰富性和模糊性是巨大的挑战。为了让确定性算法介入，我们必须将这些模糊性转化为明确的数据结构。

挑战：

• 语义多样性：同一个事实可以用多种方式表达。
• 隐式信息：某些信息可能并未明确说出，而是隐含在上下文中。
• 单位和量纲：数值可能带有不同的单位（米、厘米、英尺），需要统一。
• 关系复杂性：简单的主谓宾结构不足以表达所有关系。

使用LLM进行事实提取 (LLM-as-an-extractor)：

讽刺的是，我们可以利用LLM本身来帮助我们完成这一任务。通过精心的Prompt工程，我们可以指导LLM以特定的、机器可读的格式输出它所“理解”的事实。这通常包括JSON、YAML或结构化的文本格式。

Prompt工程示例：

假设LLM生成了以下文本：
“The length of the table is 2 meters. Its width is 150 centimeters. The area of the table is 3 square meters.”

我们可以这样Prompt LLM来提取事实：

请从以下文本中提取关于物体的属性和它们之间的数学关系。
以JSON数组的格式返回，每个对象包含 'fact_id', 'type', 'subject', 'predicate', 'object', 'unit' (如果适用) 和 'expression' (如果适用)。
如果存在一个明确的数学表达式，请将其包含在 'expression' 字段中。

文本: "The length of the table is 2 meters. Its width is 150 centimeters. The area of the table is 3 square meters."

预期输出格式:
[
  {
    "fact_id": "F1",
    "type": "property",
    "subject": "table",
    "predicate": "length",
    "object": 2,
    "unit": "meter"
  },
  {
    "fact_id": "F2",
    "type": "property",
    "subject": "table",
    "predicate": "width",
    "object": 150,
    "unit": "centimeter"
  },
  {
    "fact_id": "F3",
    "type": "property",
    "subject": "table",
    "predicate": "area",
    "object": 3,
    "unit": "square meter"
  },
  {
    "fact_id": "F4",
    "type": "relation",
    "subject": "table",
    "predicate": "area is length * width",
    "expression": "area(table) = length(table) * width(table)"
  }
]

代码示例1：模拟LLM事实提取

由于我们不能直接在这里调用一个真实的LLM API，我们将用一个函数来模拟LLM的响应，并展示如何解析它。

import json
import re

# 模拟LLM API响应的函数
def mock_llm_extract_facts(text_input: str) -> str:
    """
    模拟LLM根据输入文本提取结构化事实。
    在真实场景中，这将是一个LLM API调用，返回JSON字符串。
    """
    # 这是一个简化且硬编码的模拟，实际LLM会更智能地解析
    if "The length of the table is 2 meters. Its width is 150 centimeters. The area of the table is 3 square meters." in text_input:
        return json.dumps([
            {
                "fact_id": "F1",
                "type": "property",
                "subject": "table",
                "predicate": "length",
                "object": 2,
                "unit": "meter"
            },
            {
                "fact_id": "F2",
                "type": "property",
                "subject": "table",
                "predicate": "width",
                "object": 150,
                "unit": "centimeter"
            },
            {
                "fact_id": "F3",
                "type": "property",
                "subject": "table",
                "predicate": "area",
                "object": 3,
                "unit": "square meter"
            },
            {
                "fact_id": "F4",
                "type": "relation",
                "subject": "table",
                "predicate": "area is length * width",
                "expression": "area_table = length_table * width_table" # 使用变量名方便后续计算
            }
        ])
    elif "Company A's revenue last year was 100 million dollars. Its profit was 15 million dollars. The expenses were 80 million dollars." in text_input:
        return json.dumps([
            {
                "fact_id": "C1",
                "type": "property",
                "subject": "Company A",
                "predicate": "revenue",
                "object": 100_000_000,
                "unit": "dollar"
            },
            {
                "fact_id": "C2",
                "type": "property",
                "subject": "Company A",
                "predicate": "profit",
                "object": 15_000_000,
                "unit": "dollar"
            },
            {
                "fact_id": "C3",
                "type": "property",
                "subject": "Company A",
                "predicate": "expenses",
                "object": 80_000_000,
                "unit": "dollar"
            },
            {
                "fact_id": "C4",
                "type": "relation",
                "subject": "Company A",
                "predicate": "profit is revenue - expenses",
                "expression": "profit_company_A = revenue_company_A - expenses_company_A"
            }
        ])
    else:
        return json.dumps([])

# 原始LLM生成文本
llm_generated_text_1 = "The length of the table is 2 meters. Its width is 150 centimeters. The area of the table is 3 square meters."
llm_generated_text_2 = "Company A's revenue last year was 100 million dollars. Its profit was 15 million dollars. The expenses were 80 million dollars."

# 模拟LLM调用并解析结果
extracted_json_1 = mock_llm_extract_facts(llm_generated_text_1)
extracted_facts_1 = json.loads(extracted_json_1)

extracted_json_2 = mock_llm_extract_facts(llm_generated_text_2)
extracted_facts_2 = json.loads(extracted_json_2)

print("--- Extracted Facts 1 (Table) ---")
for fact in extracted_facts_1:
    print(fact)
print("n--- Extracted Facts 2 (Company A) ---")
for fact in extracted_facts_2:
    print(fact)

事实的标准化表示：

仅仅提取出结构化的事实还不够，我们还需要对它们进行标准化，以便确定性算法能够进行一致的比较和计算。

1. 统一单位：将所有物理量转换为一个标准单位（例如，国际单位制SI）。
2. 统一数据类型：确保所有数值都是浮点数或整数，布尔值是True/False。
3. 统一命名：对于变量或属性，使用一致的命名约定（例如，length_table 而不是 table.length）。
4. 规范化表达式：将数学表达式转换为可解析和计算的形式。

代码示例2：事实标准化处理（单位转换与变量映射）

from typing import List, Dict, Any

# 定义单位转换规则
UNIT_CONVERSION_RULES = {
    "meter": {"meter": 1, "centimeter": 0.01, "kilometer": 1000, "foot": 0.3048, "inch": 0.0254},
    "centimeter": {"meter": 100, "centimeter": 1, "kilometer": 100000, "foot": 30.48, "inch": 2.54},
    "square meter": {"square meter": 1, "square centimeter": 0.0001, "square foot": 0.092903},
    "dollar": {"dollar": 1, "million dollar": 1_000_000, "billion dollar": 1_000_000_000}
}

def convert_unit(value: float, from_unit: str, to_unit: str) -> float:
    """
    确定性地将数值从一种单位转换为另一种单位。
    """
    if from_unit == to_unit:
        return value

    # 找到基础单位
    base_unit_map = None
    for base, conversions in UNIT_CONVERSION_RULES.items():
        if from_unit in conversions:
            base_unit_map = conversions
            break

    if not base_unit_map:
        raise ValueError(f"Unknown unit: {from_unit}")

    # 转换为基础单位
    value_in_base = value * base_unit_map[from_unit]

    # 从基础单位转换为目标单位
    if to_unit in base_unit_map:
        return value_in_base / base_unit_map[to_unit]
    else:
        # 如果目标单位不在当前基础单位的转换列表中，尝试反向查找或报错
        # 更健壮的系统会有一个完整的单位图谱
        raise ValueError(f"Cannot convert from {from_unit} to {to_unit}")

def standardize_facts(extracted_facts: List[Dict[str, Any]]) -> List[Dict[str, Any]]:
    """
    对提取的事实进行标准化处理，包括单位转换和变量命名。
    """
    standardized_list = []
    for fact in extracted_facts:
        standardized_fact = fact.copy()

        # 1. 单位转换
        if 'object' in standardized_fact and isinstance(standardized_fact['object'], (int, float)) and 'unit' in standardized_fact:
            original_unit = standardized_fact['unit']
            # 定义一个默认的基础单位，这里简单地以提取到的单位作为基础，
            # 实际系统中会有一个预定义的标准单位（如SI单位）
            target_unit = original_unit 

            # 对于长度，转换为米
            if original_unit in ["meter", "centimeter", "kilometer", "foot", "inch"]:
                target_unit = "meter"
            # 对于面积，转换为平方米
            elif original_unit in ["square meter", "square centimeter", "square foot"]:
                target_unit = "square meter"
            # 对于货币，转换为美元
            elif original_unit in ["dollar", "million dollar", "billion dollar"]:
                target_unit = "dollar"

            try:
                standardized_fact['object'] = convert_unit(
                    standardized_fact['object'], original_unit, target_unit
                )
                standardized_fact['unit'] = target_unit # 更新单位为标准化后的单位
            except ValueError as e:
                print(f"Warning: Unit conversion failed for fact {fact['fact_id']}: {e}")
                # 如果转换失败，保留原始值，但标记可能存在问题
                standardized_fact['conversion_error'] = str(e)

        # 2. 变量命名规范化 (用于数学表达式)
        if 'expression' in standardized_fact:
            # 简单地将 "subject_predicate" 作为变量名
            # 例如 "length_table", "area_table"
            # 实际中可能需要更复杂的映射，例如使用知识图谱的URI
            normalized_expression = standardized_fact['expression']

            # 替换表达式中的函数调用为变量
            # 例如 'area(table)' -> 'area_table'
            # 这是一个简单的替换，实际需要更复杂的AST解析
            for ref_fact in extracted_facts:
                if ref_fact['type'] == 'property':
                    var_name = f"{ref_fact['predicate'].lower().replace(' ', '_')}_{ref_fact['subject'].lower().replace(' ', '_')}"
                    # 尝试替换形如 'predicate(subject)' 或 'predicate_subject' 的模式
                    normalized_expression = re.sub(
                        rf"{ref_fact['predicate'].lower()}({ref_fact['subject'].lower()})",
                        var_name,
                        normalized_expression
                    )
                    normalized_expression = re.sub(
                        rf"{ref_fact['predicate'].lower()}_{ref_fact['subject'].lower()}",
                        var_name,
                        normalized_expression
                    )
            standardized_fact['expression'] = normalized_expression

        standardized_list.append(standardized_fact)
    return standardized_list

# 对之前提取的事实进行标准化
standardized_facts_1 = standardize_facts(extracted_facts_1)
standardized_facts_2 = standardize_facts(extracted_facts_2)

print("n--- Standardized Facts 1 (Table) ---")
for fact in standardized_facts_1:
    print(fact)

print("n--- Standardized Facts 2 (Company A) ---")
for fact in standardized_facts_2:
    print(fact)

通过这一步，我们将LLM生成的非结构化或半结构化信息，转化为了高度结构化、标准化且机器可计算的格式。这是后续进行确定性数学和逻辑检查的基础。

4. 数学冲突的类型与表示

在标准化事实之后，我们现在需要理解可能存在的数学冲突类型，并思考如何表示这些冲突。

常见的数学冲突类型：

1. 直接数值冲突：

   • 例如：LLM宣称 "A的值是5"，同时又宣称 "A的值是6"。
   • 本质：同一实体/属性被赋予了两个不同的、不兼容的数值。

2. 间接数值冲突 (通过运算)：

   • 例如：LLM宣称 "X=2"，"Y=3"，但又宣称 "X乘以Y等于7"。
   • 本质：通过已知的数学关系和赋值，可以推导出一个与LLM生成的事实相矛盾的结果。

3. 关系冲突 (序关系)：

   • 例如：LLM宣称 "A比B高"，"B比C高"，但同时宣称 "C比A高"。
   • 本质：违反了传递性（transitivity）等基本关系属性。

4. 集合论冲突：

   • 例如：LLM宣称 "集合S1包含元素{1, 2}"，"集合S2包含元素{2, 3}"，但又宣称 "S1和S2的并集是{1, 2, 3, 4}"。
   • 本质：违反了集合操作（并集、交集、差集）的定义。

5. 逻辑蕴含冲突：

   • 例如：LLM宣称 "如果P为真，则Q为真"，但又宣称 "P为真，且Q为假"。
   • 本质：违反了基本的逻辑推导规则。

如何表示这些事实和关系？

为了让确定性算法处理这些冲突，我们需要将它们表示为形式化的结构：

• 变量赋值：
  • length_table = 2.0 (浮点数)
  • revenue_company_A = 100000000.0 (浮点数)
• 数学表达式：
  • area_table = length_table * width_table
  • profit_company_A = revenue_company_A - expenses_company_A
• 比较表达式：
  • A > B
  • C <= D
• 集合表示：
  • S1 = {1, 2}
  • S2 = {2, 3}
• 逻辑命题：
  • P (布尔变量)
  • P => Q (蕴含关系)
  • P AND NOT Q (复合命题)

这些表示可以进一步抽象为抽象语法树 (AST) 或知识图谱 (Knowledge Graph) 的形式，以便于推理引擎的解析和处理。对于数学表达式，我们通常使用表达式树；对于逻辑和关系，则可以利用符号逻辑或图数据库。

5. 基于确定性算法的数学冲突检测框架

现在我们有了标准化的事实表示和对冲突类型的理解，我们可以构建一个通用的、基于确定性算法的冲突检测框架。

框架概述：

1. 事实提取与标准化 (已完成)：将LLM生成的自然语言文本转换为结构化的、标准化的事实列表。
2. 事实存储与索引：将标准化后的事实存储在一个可查询的数据结构中（例如，变量字典、关系列表、约束集合）。
3. 定义一致性规则：明确哪些数学公理、领域知识和逻辑规则是必须满足的。这些规则本身就是确定性的。
4. 执行确定性推理引擎：利用这些规则，对存储的事实进行推理和计算，检测是否存在矛盾。
5. 冲突报告：一旦发现冲突，生成清晰的报告，指出冲突的事实ID、类型和可能的原因。

核心组件：推理引擎

推理引擎是KCC框架的心脏。它需要能够：

• 解析表达式：将字符串形式的数学表达式解析成可计算的结构。
• 评估表达式：根据已知的变量赋值，计算表达式的值。
• 检查等式/不等式：验证表达式是否满足给定的关系。
• 处理逻辑：执行布尔逻辑操作。
• 求解约束：在更复杂的场景下，可能需要求解一组变量的约束条件。

常用的确定性推理技术：

• 基于规则的推理 (Rule-Based Reasoning)：预定义一系列IF-THEN规则，当条件满足时，执行相应的操作或推断。
• 数值计算库：Python的 math 模块、NumPy等，用于执行精确的算术运算。
• 符号计算库：如SymPy，可以处理符号变量、代数方程和表达式的简化，非常适合检测代数冲突。
• 约束满足问题 (CSP) 求解器：适用于变量有特定域且需要满足一系列约束的场景。
• SAT/SMT 求解器：用于命题逻辑或一阶逻辑的满足性检查，可以检测逻辑矛盾。

6. 实践案例：数值与代数冲突检测

我们将从最常见的数值和代数冲突开始。

场景设定： LLM生成关于物理量（如长度、面积）、财务数据（如收入、支出、利润）或工程参数的事实。

检测流程：

1. 收集事实：LLM生成的事实经过提取和标准化，得到一组变量赋值和数学表达式。
   • 变量赋值：length_table = 2.0 (meter)
   • 变量赋值：width_table = 1.5 (meter) (注意，150厘米已转换为1.5米)
   • 变量赋值：area_table = 3.0 (square meter)
   • 数学关系：area_table = length_table * width_table
2. 建立变量环境：创建一个字典或符号表来存储所有已知的变量及其值。
3. 解析与评估表达式：对于每个数学关系表达式，使用确定性算法解析它，并根据变量环境计算其左侧和右侧的值。
4. 检测矛盾：
   • 如果一个变量被赋予了多个不同的值，则为直接冲突。
   • 如果一个数学关系表达式的计算结果与LLM宣称的值不一致，则为间接冲突。

代码示例3：基本数值一致性检查

这个例子将使用Python的 eval() 函数（在受控环境下使用）或更安全的表达式解析器来处理简单的算术表达式。

import operator
from typing import Dict, List, Tuple, Any

# 定义一个安全的表达式评估器，避免使用eval()直接执行任意代码
# 仅支持基本运算符和数字
SAFE_OPERATORS = {
    '+': operator.add,
    '-': operator.sub,
    '*': operator.mul,
    '/': operator.truediv,
    '==': operator.eq,
    '>': operator.gt,
    '<': operator.lt,
    '>=': operator.ge,
    '<=': operator.le
}

def evaluate_expression(expression_str: str, variables: Dict[str, float]) -> Any:
    """
    确定性地评估一个简单的数学表达式字符串。
    为了安全和确定性，这里不使用 eval()，而是手动解析。
    这只是一个非常简化的解析器，实际应用中会使用更健壮的库。
    """
    # 替换表达式中的变量名为其数值
    for var_name, value in variables.items():
        # 确保替换的是完整的变量名，而不是部分匹配
        expression_str = re.sub(r'b' + re.escape(var_name) + r'b', str(value), expression_str)

    try:
        # 使用Python的内置eval函数（需谨慎，这里假设输入是受控的纯数学表达式）
        # 更安全的做法是使用 ast.literal_eval 或专门的数学表达式解析库
        return eval(expression_str, {"__builtins__": {}}, SAFE_OPERATORS)
    except Exception as e:
        print(f"Error evaluating expression '{expression_str}': {e}")
        return None

def check_numerical_consistency(standardized_facts: List[Dict[str, Any]]) -> List[Dict[str, Any]]:
    """
    检查标准化事实中的数值和代数一致性。
    """
    known_variables: Dict[str, float] = {} # 存储已知的变量名和值
    potential_conflicts: List[Dict[str, Any]] = []

    # 1. 处理属性赋值，填充已知变量
    for fact in standardized_facts:
        if fact['type'] == 'property':
            # 创建变量名，例如 length_table
            var_name = f"{fact['predicate'].lower().replace(' ', '_')}_{fact['subject'].lower().replace(' ', '_')}"
            value = fact['object']

            if var_name in known_variables:
                # 检查直接数值冲突
                if abs(known_variables[var_name] - value) > 1e-9: # 浮点数比较
                    potential_conflicts.append({
                        "conflict_type": "Direct Numerical Conflict",
                        "variable": var_name,
                        "fact_id_1": f"Previous assignment for {var_name}",
                        "value_1": known_variables[var_name],
                        "fact_id_2": fact['fact_id'],
                        "value_2": value,
                        "description": f"Variable '{var_name}' is assigned {known_variables[var_name]} and then {value}."
                    })
            known_variables[var_name] = float(value) # 确保是浮点数

    # 2. 处理数学关系表达式，检查间接数值冲突
    for fact in standardized_facts:
        if fact['type'] == 'relation' and 'expression' in fact:
            expression_str = fact['expression']

            # 尝试评估表达式
            # 这里需要一个更复杂的解析器来区分等式左右两边
            # 假设表达式是形如 "LHS = RHS"
            if '=' in expression_str:
                lhs_str, rhs_str = expression_str.split('=', 1)
                lhs_value = evaluate_expression(lhs_str.strip(), known_variables)
                rhs_value = evaluate_expression(rhs_str.strip(), known_variables)

                if lhs_value is not None and rhs_value is not None:
                    if abs(lhs_value - rhs_value) > 1e-9: # 浮点数比较
                        potential_conflicts.append({
                            "conflict_type": "Indirect Numerical Conflict (Mathematical Relation)",
                            "fact_id": fact['fact_id'],
                            "expression": expression_str,
                            "calculated_lhs": lhs_value,
                            "calculated_rhs": rhs_value,
                            "description": f"Expression '{expression_str}' evaluates to {lhs_value} != {rhs_value}."
                        })
                else:
                    potential_conflicts.append({
                        "conflict_type": "Expression Evaluation Error",
                        "fact_id": fact['fact_id'],
                        "expression": expression_str,
                        "description": "Could not evaluate expression due to missing variables or syntax errors."
                    })
            else:
                # 如果表达式不是等式，例如只有一边，我们目前不处理
                pass 

    return potential_conflicts, known_variables

# 运行KCC
conflicts_1, variables_1 = check_numerical_consistency(standardized_facts_1)
conflicts_2, variables_2 = check_numerical_consistency(standardized_facts_2)

print("n--- KCC Results for Table Facts ---")
print("Known Variables:", variables_1)
if conflicts_1:
    print("Conflicts Found:")
    for conflict in conflicts_1:
        print(conflict)
else:
    print("No numerical conflicts found.")

print("n--- KCC Results for Company A Facts ---")
print("Known Variables:", variables_2)
if conflicts_2:
    print("Conflicts Found:")
    for conflict in conflicts_2:
        print(conflict)
else:
    print("No numerical conflicts found.")

代码示例4：更复杂的代数表达式和约束 (使用 SymPy)

对于涉及符号变量、方程组和更复杂代数关系的场景，Python的SymPy库是理想的选择。SymPy是一个用于符号数学的Python库，它允许我们以符号方式处理表达式，而不仅仅是数值。

import sympy
from typing import Dict, List, Any

def check_algebraic_consistency_sympy(standardized_facts: List[Dict[str, Any]]) -> List[Dict[str, Any]]:
    """
    使用SymPy检查代数一致性，处理方程组和变量赋值。
    """
    # 存储变量的符号表示
    sympy_symbols: Dict[str, sympy.Symbol] = {}
    # 存储LLM提供的变量赋值
    llm_assignments: Dict[sympy.Symbol, float] = {}
    # 存储从LLM提取的方程
    llm_equations: List[sympy.Eq] = []

    potential_conflicts: List[Dict[str, Any]] = []

    # 1. 提取变量和方程
    for fact in standardized_facts:
        if fact['type'] == 'property':
            var_name = f"{fact['predicate'].lower().replace(' ', '_')}_{fact['subject'].lower().replace(' ', '_')}"
            symbol = sympy_symbols.get(var_name, sympy.Symbol(var_name))
            sympy_symbols[var_name] = symbol
            llm_assignments[symbol] = float(fact['object'])
        elif fact['type'] == 'relation' and 'expression' in fact:
            expr_str = fact['expression']
            try:
                # 确保所有涉及的变量都被定义为SymPy符号
                # 这里需要预先识别表达式中的所有变量并创建符号
                # 简化处理：SymPy的sympify可以自动创建符号，但最好显式管理

                # 动态识别表达式中的变量并创建SymPy符号
                # 例如 "area_table = length_table * width_table"
                # 需要提取 area_table, length_table, width_table

                # 更健壮的做法是遍历表达式并创建符号
                # 这里简单地将所有已知的变量名转换为符号
                local_symbols = {name: sympy.Symbol(name) for name in sympy_symbols}

                # 使用sympify将字符串转换为SymPy表达式
                # evalf() 用于数值评估

                # 假设表达式是 'LHS = RHS' 形式
                if '=' in expr_str:
                    lhs_str, rhs_str = expr_str.split('=', 1)
                    lhs_expr = sympy.sympify(lhs_str, locals=local_symbols)
                    rhs_expr = sympy.sympify(rhs_str, locals=local_symbols)
                    llm_equations.append(sympy.Eq(lhs_expr, rhs_expr))
                else:
                    # 如果不是等式，可以处理不等式等，这里简化
                    pass
            except Exception as e:
                potential_conflicts.append({
                    "conflict_type": "Algebraic Expression Parse Error",
                    "fact_id": fact['fact_id'],
                    "expression": expr_str,
                    "description": f"Could not parse expression with SymPy: {e}"
                })

    # 2. 检查直接数值冲突 (通过LLM赋值)
    # SymPy本身不直接处理不同赋值，我们需要在构建llm_assignments时进行检查
    # 这部分已在check_numerical_consistency中处理，这里不再重复

    # 3. 检查间接数值冲突 (通过方程组和赋值)
    # 将LLM的赋值转换为方程
    assignment_equations = []
    for symbol, value in llm_assignments.items():
        assignment_equations.append(sympy.Eq(symbol, value))

    all_equations = llm_equations + assignment_equations

    # 尝试求解方程组
    # SymPy的solve函数可以用来检查方程组的解
    # 如果方程组无解，则存在矛盾
    try:
        # 提取方程中所有的符号
        all_symbols_in_equations = set()
        for eq in all_equations:
            all_symbols_in_equations.update(eq.free_symbols)

        # 尝试求解，如果得到空集，表示无解或矛盾
        # SymPy的solve函数对于矛盾系统会返回空列表或空字典
        solution = sympy.solve(all_equations, list(all_symbols_in_equations))

        if not solution:
            potential_conflicts.append({
                "conflict_type": "Algebraic Contradiction",
                "facts_involved": [f['fact_id'] for f in standardized_facts if f['type'] in ['property', 'relation']],
                "description": "The system of equations derived from LLM facts has no consistent solution.",
                "equations": [str(eq) for eq in all_equations]
            })
        else:
            # 如果有解，我们还可以进一步检查这个解是否与LLM的原始赋值一致
            # 例如，如果solution是 {x: 5, y: 10}
            # 我们可以将这些解代回LLM的原始赋值
            for symbol, assigned_value in llm_assignments.items():
                if symbol in solution: # 如果symbol在solution的键中
                    # SymPy的solution可能是一个字典的列表 (如果有多个解)
                    # 或者单个字典 (如果只有一个解)
                    if isinstance(solution, list):
                        # 对于每个解，检查是否一致
                        for sol_dict in solution:
                            if symbol in sol_dict:
                                solved_value = sol_dict[symbol].evalf() # 数值评估
                                if abs(solved_value - assigned_value) > 1e-9:
                                    potential_conflicts.append({
                                        "conflict_type": "Assignment vs. Derived Value Conflict",
                                        "variable": str(symbol),
                                        "llm_assigned_value": assigned_value,
                                        "derived_value": solved_value,
                                        "description": f"LLM assigned '{symbol}' = {assigned_value}, but derived value is {solved_value}.",
                                        "relevant_facts": [f['fact_id'] for f in standardized_facts if f['type'] in ['property', 'relation'] and str(symbol) in f.get('expression', '')]
                                    })
                                    # 找到一个冲突即可，无需检查其他解
                                    break 
                    elif isinstance(solution, dict):
                         if symbol in solution:
                            solved_value = solution[symbol].evalf()
                            if abs(solved_value - assigned_value) > 1e-9:
                                potential_conflicts.append({
                                    "conflict_type": "Assignment vs. Derived Value Conflict",
                                    "variable": str(symbol),
                                    "llm_assigned_value": assigned_value,
                                    "derived_value": solved_value,
                                    "description": f"LLM assigned '{symbol}' = {assigned_value}, but derived value is {solved_value}.",
                                    "relevant_facts": [f['fact_id'] for f in standardized_facts if f['type'] in ['property', 'relation'] and str(symbol) in f.get('expression', '')]
                                })

    except Exception as e:
        potential_conflicts.append({
            "conflict_type": "SymPy Solver Error",
            "description": f"An error occurred during SymPy equation solving: {e}",
            "equations": [str(eq) for eq in all_equations]
        })

    return potential_conflicts

# 准备一个包含矛盾的场景
# 假设LLM生成：
# length_table = 2 meters (F1)
# width_table = 1.5 meters (F2)
# area_table = 3 square meters (F3)
# area_table = length_table * width_table (F4)
# 但LLM又错误地生成： area_table = 4 square meters (F5) - 引入矛盾

# 我们修改 standardized_facts_1 来引入一个矛盾
# 原始的 standardized_facts_1 已经是 self-consistent 的
# 为了演示SymPy的冲突检测能力，我们手动添加一个矛盾
contradictory_facts_1 = list(standardized_facts_1) # 复制一份
# 修改 F3 的 area_table 值为 4.0，而不是 3.0
for fact in contradictory_facts_1:
    if fact['fact_id'] == 'F3':
        fact['object'] = 4.0 # 引入矛盾：2 * 1.5 = 3，但这里说 area = 4
        fact['unit'] = 'square meter' # 确保单位一致

# 确保在 contradictory_facts_1 中，F4 表达式的变量名被正确替换
# 在实际集成中，这一步在 standardize_facts 内部完成
# 手动调整 F4 的表达式以匹配新的变量名约定，如果需要
for fact in contradictory_facts_1:
    if fact['fact_id'] == 'F4':
        fact['expression'] = "area_table = length_table * width_table"

print("n--- KCC Results for Contradictory Table Facts (SymPy) ---")
contradiction_conflicts = check_algebraic_consistency_sympy(contradictory_facts_1)
if contradiction_conflicts:
    print("Conflicts Found:")
    for conflict in contradiction_conflicts:
        print(conflict)
else:
    print("No algebraic conflicts found.")

# 针对 Company A 的事实进行 SymPy 检查
print("n--- KCC Results for Company A Facts (SymPy) ---")
company_a_conflicts = check_algebraic_consistency_sympy(standardized_facts_2)
if company_a_conflicts:
    print("Conflicts Found:")
    for conflict in company_a_conflicts:
        print(conflict)
else:
    print("No algebraic conflicts found.")

SymPy 示例分析：

在上面的SymPy示例中，我们首先将LLM生成的数值赋值和数学关系（等式）都转化为SymPy的符号变量和方程。然后，我们将所有这些方程组合成一个方程组，并尝试使用sympy.solve()来求解。

• 如果solve函数返回空集，这意味着方程组没有一致的解，从而表明LLM生成的事实之间存在代数上的矛盾。
• 即使有解，我们也会将SymPy计算出的变量值与LLM最初声明的变量值进行比较。如果存在显著差异，也表明了不一致。

这个方法对于检测涉及多个变量和复杂代数关系的冲突非常有效。

表格展示LLM生成的事实和检测结果

为了更清晰地展示，我们可以将LLM生成的事实、标准化结果和冲突检测结果整理成表格。

| Fact ID | Type | Subject | Predicate | Object | Unit | Expression | Standardized Object (Unit) | Derived Value | Conflict Type | Description This will be the first section of the lecture.