LLM 代码正确性验证方法论：从执行测试到形式化推理的分层验证

一、AI 代码验证的信任危机：为什么"跑通了"不代表"对了"

LLM 生成的代码能否直接用于生产？这个问题的答案取决于代码的正确性验证程度。目前最常见的验证方式是"跑通测试用例"，但这种验证存在严重的信任缺口。

一个真实的案例：AI 生成了一个二分查找函数，通过了 LeetCode 的全部测试用例。但代码中存在一个隐藏 Bug——当数组长度为 0 时，函数返回数组最后一个元素而非 -1。这个 Bug 在测试用例中没有覆盖，因为 LeetCode 的测试用例假设数组非空。

更隐蔽的问题出现在算法复杂度层面。AI 生成的代码可能通过了所有测试用例，但时间复杂度比标注的高一个量级。例如声称 O(n log n) 的排序，实际实现中嵌套了不必要的循环，复杂度为 O(n²)。在小规模测试数据上看不出差异，但生产数据量增大后性能急剧下降。

代码正确性验证需要从"跑通测试"走向分层验证：语法正确性 → 执行正确性 → 边界正确性 → 复杂度正确性 → 逻辑正确性。每一层验证覆盖不同类型的错误，层层递进。

二、LLM 代码验证的五层模型

flowchart TD
    A[LLM 生成代码] --> B[L1 语法正确性]
    B -->|通过| C[L2 执行正确性]
    C -->|通过| D[L3 边界正确性]
    D -->|通过| E[L4 复杂度正确性]
    E -->|通过| F[L5 逻辑正确性]

    B -->|失败| G[语法修复]
    G --> B

    C -->|失败| H[错误反馈重生成]
    H --> A

    D -->|失败| I[补充边界测试]
    I --> C

    E -->|失败| J[复杂度分析反馈]
    J --> A

    F -->|失败| K[人工审查]
    K --> L[最终确认]

    subgraph 自动化验证 L1-L4
        B
        C
        D
        E
    end

    subgraph 人工验证 L5
        F
        K
    end

L1 语法正确性：代码能否通过编译/解析。这是最基础的验证层，通过 AST 解析或编译器检查即可完成。AI 生成代码的语法错误率约 5-10%。

L2 执行正确性：代码能否通过给定的测试用例。通过自动化测试框架执行验证。AI 生成代码在给定测试用例上的通过率约 70-85%。

L3 边界正确性：代码在极端输入下是否正确。需要生成额外的边界测试用例（空输入、单元素、极大值、特殊字符等）。AI 生成代码的边界错误率约 15-20%。

L4 复杂度正确性：代码的实际时间/空间复杂度是否与标注一致。通过静态分析和性能测试验证。AI 标注复杂度的错误率约 15-20%。

L5 逻辑正确性：代码的逻辑推理是否正确，是否存在隐藏假设。这一层最难自动化，需要人工审查或形式化验证。

三、生产级验证框架实现

3.1 分层验证引擎

# verification_engine.py
# LLM 代码分层验证引擎

import ast
import time
import subprocess
import tempfile
from typing import List, Tuple, Optional

class VerificationResult:
    def __init__(self, level: int, passed: bool, message: str, details: dict = None):
        self.level = level
        self.passed = passed
        self.message = message
        self.details = details or {}

class CodeVerificationEngine:
    def __init__(self, language: str = "python"):
        self.language = language

    def verify(
        self,
        code: str,
        test_cases: List[Tuple[str, str]],
        claimed_complexity: Optional[str] = None,
    ) -> List[VerificationResult]:
        """执行分层验证"""
        results = []

        # L1: 语法正确性
        l1 = self._verify_syntax(code)
        results.append(l1)
        if not l1.passed:
            return results  # 语法错误，后续验证无法进行

        # L2: 执行正确性
        l2 = self._verify_execution(code, test_cases)
        results.append(l2)
        if not l2.passed:
            return results  # 执行失败，需要修复

        # L3: 边界正确性
        l3 = self._verify_boundary(code, test_cases)
        results.append(l3)

        # L4: 复杂度正确性
        if claimed_complexity:
            l4 = self._verify_complexity(code, claimed_complexity)
            results.append(l4)

        return results

    def _verify_syntax(self, code: str) -> VerificationResult:
        """L1: 语法正确性验证"""
        try:
            ast.parse(code)
            return VerificationResult(
                level=1, passed=True,
                message="语法检查通过",
            )
        except SyntaxError as e:
            return VerificationResult(
                level=1, passed=False,
                message=f"语法错误: 第 {e.lineno} 行, {e.msg}",
                details={"line": e.lineno, "msg": e.msg},
            )

    def _verify_execution(
        self, code: str, test_cases: List[Tuple[str, str]]
    ) -> VerificationResult:
        """L2: 执行正确性验证"""
        passed = 0
        failed = []

        with tempfile.NamedTemporaryFile(
            mode='w', suffix='.py', delete=False
        ) as f:
            f.write(code)
            code_path = f.name

        try:
            for i, (input_data, expected) in enumerate(test_cases):
                try:
                    result = subprocess.run(
                        ["python3", code_path],
                        input=input_data,
                        capture_output=True,
                        text=True,
                        timeout=5,
                    )
                    actual = result.stdout.strip()
                    expected = expected.strip()

                    if actual == expected:
                        passed += 1
                    else:
                        failed.append({
                            "case": i + 1,
                            "expected": expected[:200],
                            "actual": actual[:200],
                        })
                except subprocess.TimeoutExpired:
                    failed.append({"case": i + 1, "error": "执行超时"})
        finally:
            import os
            os.unlink(code_path)

        pass_rate = passed / max(len(test_cases), 1)
        return VerificationResult(
            level=2,
            passed=pass_rate == 1.0,
            message=f"通过 {passed}/{len(test_cases)} 个测试用例",
            details={"pass_rate": pass_rate, "failed": failed},
        )

    def _verify_boundary(
        self, code: str, test_cases: List[Tuple[str, str]]
    ) -> VerificationResult:
        """L3: 边界正确性验证，自动生成边界测试用例"""
        boundary_cases = self._generate_boundary_cases(test_cases)
        result = self._verify_execution(code, boundary_cases)

        return VerificationResult(
            level=3,
            passed=result.passed,
            message=f"边界测试: {result.message}",
            details=result.details,
        )

    def _generate_boundary_cases(
        self, test_cases: List[Tuple[str, str]]
    ) -> List[Tuple[str, str]]:
        """根据已有测试用例生成边界测试"""
        boundary = []

        # 空输入
        boundary.append(("", ""))

        # 单元素输入
        for inp, _ in test_cases[:1]:
            lines = inp.strip().split('\n')
            if len(lines) > 1:
                # 只保留第一行（通常是数组大小）
                boundary.append((lines[0] + '\n1\n', None))

        # 极大值输入
        boundary.append(("100000\n" + "1 " * 100000, None))

        return [(inp, exp) for inp, exp in boundary if exp is not None]

    def _verify_complexity(
        self, code: str, claimed: str
    ) -> VerificationResult:
        """L4: 复杂度正确性验证"""
        # 通过静态分析推断实际复杂度
        inferred = self._infer_complexity(code)
        match = self._compare_complexity(claimed, inferred)

        return VerificationResult(
            level=4,
            passed=match,
            message=f"标注: {claimed}, 推断: {inferred}",
            details={"claimed": claimed, "inferred": inferred},
        )

    def _infer_complexity(self, code: str) -> str:
        """静态分析推断时间复杂度"""
        try:
            tree = ast.parse(code)
        except SyntaxError:
            return "unknown"

        max_nesting = 0
        for node in ast.walk(tree):
            if isinstance(node, (ast.For, ast.While)):
                nesting = self._count_nesting(node)
                max_nesting = max(max_nesting, nesting)

        if max_nesting == 0:
            return "O(1)"
        elif max_nesting == 1:
            return "O(n)"
        elif max_nesting == 2:
            return "O(n²)"
        else:
            return f"O(n^{max_nesting})"

    def _count_nesting(self, node, depth=1):
        max_d = depth
        for child in ast.walk(node):
            if isinstance(child, (ast.For, ast.While)) and child != node:
                d = self._count_nesting(child, depth + 1)
                max_d = max(max_d, d)
        return max_d

    def _compare_complexity(self, claimed: str, inferred: str) -> bool:
        import re
        c1 = re.sub(r'[^a-z0-9]', '', claimed.lower())
        c2 = re.sub(r'[^a-z0-9]', '', inferred.lower())
        return c1 == c2 or c1 == "unknown" or c2 == "unknown"

四、架构权衡与适用边界

自动化深度与成本的矛盾。L1-L2 验证成本极低（毫秒级），L3 边界验证需要生成额外测试用例（秒级），L4 复杂度验证需要静态分析（秒级），L5 逻辑验证需要人工审查或形式化证明（分钟到小时级）。建议对 AI 生成的代码默认执行 L1-L4，L5 仅用于关键路径代码。

边界用例生成的覆盖度。自动生成的边界用例只能覆盖常见的边界模式（空输入、单元素、极大值），无法覆盖业务特定的边界（如"数组元素互不相同"的假设）。对于业务代码，需要人工补充领域特定的边界用例。

复杂度推断的准确性。静态分析对简单循环嵌套的复杂度推断准确率约 80%，但对递归、分治、动态规划等复杂模式的推断仍然困难。对于复杂算法，建议结合性能测试（用不同规模的数据实测运行时间）来验证复杂度。

适用边界：分层验证框架适用于 AI 生成代码被用于生产环境的场景。对于快速原型和实验性代码，L1-L2 验证已经足够。对于算法竞赛，L1-L4 验证可以覆盖大部分错误。对于金融、医疗等安全关键场景，L5 人工审查不可省略。

五、总结

LLM 代码正确性验证需要从"跑通测试"走向五层分层验证：语法正确性（AST 解析）、执行正确性（测试用例）、边界正确性（极端输入）、复杂度正确性（静态分析）、逻辑正确性（人工审查）。前四层可以自动化，覆盖 80-90% 的常见错误；第五层需要人工介入，覆盖隐藏假设和逻辑缺陷。工程落地时，建议默认执行 L1-L4 自动化验证，对关键代码增加 L5 人工审查。边界用例生成和复杂度推断是当前自动化的薄弱环节，需要持续改进。