符号计算工具指南 — 机器人学公式验证与推理

版本: v1.0 | 日期: 2026-05-08 | 定位: 项目内部工具参考

本文档汇总了可用于机器人学教学文档中**理论公式的符号化验证与推理**的开源工具，覆盖动力学、控制、优化、Lie 群等全部方向。

---

1. 工具全景图

┌─────────────────────────────────────────────────────┐
│                  符号计算工具生态                      │
├─────────────┬──────────────┬────────────────────────┤
│  通用 CAS    │  专用领域     │  形式化证明             │
├─────────────┼──────────────┼────────────────────────┤
│ SymPy       │ PyDy         │ Lean 4 + Mathlib       │
│ SymEngine   │ python-control│                       │
│ Wolfram     │ Cadabra      │                        │
│ SageMath    │ M4E          │                        │
│ Symbolica   │ spatialmath  │                        │
│ GiNaC      │              │                        │
│ Maxima      │              │                        │
└─────────────┴──────────────┴────────────────────────┘

1.1 推荐配置

优先级	工具	安装	用途
1	SymPy	已有 (pip install sympy)	通用符号计算 + physics.mechanics + physics.control
2	PyDy	pip install pydy	多体动力学符号建模，从物理描述推导 EOM
3	SymEngine	pip install symengine	SymPy 加速后端 (10-100x)，API 兼容
4	Wolfram Engine	本地安装 + AgentTools MCP	复杂化简兜底、张量运算、微分几何
5	SageMath	conda install sage 或独立安装	微分流形、李群/李代数、数论
6	Cadabra	系统包管理器安装	张量指标运算、场论、微分几何

---

2. SymPy — 通用符号计算主力

2.1 安装

pip install sympy

2.2 基础符号运算

from sympy import *

# 定义符号变量
x, y, z = symbols('x y z')
m, k, g = symbols('m k g', positive=True)

# 化简
expr = sin(x)**2 + cos(x)**2
simplify(expr)  # → 1

# 符号微分
diff(sin(x) * exp(-x), x)  # → -sin(x)*exp(-x) + cos(x)*exp(-x)

# 符号积分
integrate(x**2 * exp(-x), (x, 0, oo))  # → 2

# 方程求解
solve(x**3 - 6*x**2 + 11*x - 6, x)  # → [1, 2, 3]

# 级数展开
series(exp(x), x, 0, 5)  # → 1 + x + x²/2 + x³/6 + x⁴/24 + O(x⁵)

2.3 矩阵符号运算

from sympy import Matrix, symbols, simplify

q1, q2 = symbols('q1 q2')
m1, m2, l1, l2 = symbols('m1 m2 l1 l2', positive=True)

# 符号质量矩阵（双连杆机械臂）
M = Matrix([
    [(m1 + m2)*l1**2 + m2*l2**2 + 2*m2*l1*l2*cos(q2),
     m2*l2**2 + m2*l1*l2*cos(q2)],
    [m2*l2**2 + m2*l1*l2*cos(q2),
     m2*l2**2]
])

# 验证对称性
assert simplify(M - M.T) == zeros(2)

# 验证正定性（符号特征值）
eigenvals = M.eigenvals()
print(eigenvals)

# 符号求逆
M_inv = M.inv()
simplify(M * M_inv)  # → eye(2)

# 符号 Jacobian
f = Matrix([l1*cos(q1) + l2*cos(q1+q2),
            l1*sin(q1) + l2*sin(q1+q2)])
J = f.jacobian([q1, q2])
print(J)

2.4 公式等价验证

# 验证文档中两个表达式是否等价
expr_doc = ...     # 文档中的公式
expr_derived = ... # 从定义推导的公式

# 方法 1: 直接化简差
result = simplify(expr_doc - expr_derived)
assert result == 0, f"公式不等价，差值: {result}"

# 方法 2: 用 trigsimp 处理三角函数
result = trigsimp(expr_doc - expr_derived)

# 方法 3: 展开后比较（更可靠）
assert expand(expr_doc) == expand(expr_derived)

# 方法 4: 带假设化简
from sympy import assuming, Q
with assuming(Q.positive(m), Q.real(q1)):
    result = simplify(expr_doc - expr_derived)

2.5 控制理论 (sympy.physics.control)

from sympy.physics.control.lti import TransferFunction
from sympy import symbols

s = symbols('s')
m, b, k = symbols('m b k', positive=True)

# 质量-弹簧-阻尼传递函数
G = TransferFunction(1, m*s**2 + b*s + k, s)

# 极点
poles = G.poles()

# 阻抗控制传递函数
Md, Bd, Kd = symbols('M_d B_d K_d', positive=True)
G_imp = TransferFunction(1, Md*s**2 + Bd*s + Kd, s)

2.6 优化公式验证 (KKT 条件)

from sympy import symbols, diff, solve

x1, x2, lam = symbols('x1 x2 lambda')

# 目标函数
f = x1**2 + x2**2

# 约束 g(x) = 0
g = x1 + x2 - 1

# Lagrangian
L = f + lam * g

# KKT 条件 (∇L = 0)
kkt_1 = diff(L, x1)  # 2*x1 + lambda
kkt_2 = diff(L, x2)  # 2*x2 + lambda
kkt_3 = diff(L, lam)  # x1 + x2 - 1

# 求解
sol = solve([kkt_1, kkt_2, kkt_3], [x1, x2, lam])
print(sol)  # {x1: 1/2, x2: 1/2, lambda: -1}

---

3. SymEngine — SymPy 的 C++ 加速后端

3.1 安装

pip install symengine

3.2 使用方式

import symengine as se

x, y = se.symbols('x y')

# 基本运算 — API 与 SymPy 兼容
expr = se.sin(x)**2 + se.cos(x)**2

# 微分
d = se.diff(se.sin(x)*se.exp(-x), x)

# 展开（比 SymPy 快 ~100x）
expanded = se.expand((x + y)**10)

# 与 SymPy 互操作
from sympy import sympify
sympy_expr = sympify(se.expand((x+y)**20))  # SymEngine → SymPy

3.3 何时用 SymEngine 替代 SymPy

场景	选择
简单公式化简/微分	SymPy 够用
高阶多项式展开	SymEngine (100x 加速)
大矩阵符号运算	SymEngine
需要 physics.mechanics	SymPy (SymEngine 无此模块)
批量公式验证脚本	SymEngine + SymPy 混合

3.4 混合使用模式

import symengine as se
from sympy import simplify as sp_simplify, sympify

# SymEngine 做快速展开
x = se.Symbol('x')
fast_result = se.expand((1 + x)**50)

# 转为 SymPy 做高级化简
slow_but_smart = sp_simplify(sympify(fast_result))

---

4. PyDy — 多体动力学符号推导

4.1 安装

pip install pydy

PyDy 基于 sympy.physics.mechanics，提供上层多体建模工具。

4.2 核心概念

ReferenceFrame → 参考系（自动追踪旋转关系）
Point          → 空间点（自动追踪位置/速度）
RigidBody      → 刚体（质量 + 惯量 + 参考系 + 质心）
KanesMethod    → Kane 方法推导 EOM
LagrangesMethod→ Lagrange 方法推导 EOM

4.3 示例: 单摆 EOM 符号推导与验证

from sympy import symbols, simplify
from sympy.physics.mechanics import (
    dynamicsymbols, ReferenceFrame, Point,
    Particle, KanesMethod
)

# 广义坐标
theta = dynamicsymbols('theta')
theta_dot = dynamicsymbols('theta', 1)

# 参数
m, l, g = symbols('m l g', positive=True)

# 参考系
N = ReferenceFrame('N')                    # 惯性系
A = N.orientnew('A', 'Axis', [theta, N.z]) # 摆杆系

# 质心位置
O = Point('O')
O.set_vel(N, 0)
P = O.locatenew('P', l * A.x)
P.v2pt_theory(O, N, A)

# 质点
Pa = Particle('Pa', P, m)

# Kane 方法
kde = [theta_dot - theta.diff()]
KM = KanesMethod(N, q_ind=[theta], u_ind=[theta_dot], kd_eqs=kde)

# 外力: 重力
forces = [(P, -m * g * N.y)]

# 推导 EOM
(fr, frstar) = KM.kanes_equations([Pa], forces)

# 符号化质量矩阵和力向量
M_matrix = KM.mass_matrix       # → m*l²
forcing = KM.forcing            # → -m*g*l*sin(theta)

print("Mass matrix:", M_matrix)
print("Forcing:", forcing)

# 验证: EOM 应为 θ̈ + (g/l)*sin(θ) = 0
eom_simplified = simplify(forcing[0] / M_matrix[0, 0])
print("θ̈ =", eom_simplified)  # → -g*sin(theta)/l  ✓

4.4 示例: 双连杆机械臂 EOM 推导

from sympy import symbols, trigsimp
from sympy.physics.mechanics import (
    dynamicsymbols, ReferenceFrame, Point,
    RigidBody, inertia, KanesMethod
)

# 广义坐标
q1, q2 = dynamicsymbols('q1 q2')
u1, u2 = dynamicsymbols('u1 u2')

# 参数
m1, m2 = symbols('m1 m2', positive=True)
l1, l2 = symbols('l1 l2', positive=True)
lc1, lc2 = symbols('lc1 lc2', positive=True)
I1, I2 = symbols('I1 I2', positive=True)
g_val = symbols('g', positive=True)

# 参考系
N = ReferenceFrame('N')
A = N.orientnew('A', 'Axis', [q1, N.z])
B = A.orientnew('B', 'Axis', [q2, A.z])

# 关节点
O = Point('O')
O.set_vel(N, 0)

P1 = O.locatenew('P1', lc1 * A.x)
P1.v2pt_theory(O, N, A)

J2 = O.locatenew('J2', l1 * A.x)
J2.v2pt_theory(O, N, A)

P2 = J2.locatenew('P2', lc2 * B.x)
P2.v2pt_theory(J2, N, B)

# 刚体
I1_dyadic = inertia(A, 0, 0, I1)
I2_dyadic = inertia(B, 0, 0, I2)
Body1 = RigidBody('Body1', P1, A, m1, (I1_dyadic, P1))
Body2 = RigidBody('Body2', P2, B, m2, (I2_dyadic, P2))

# Kane 方法
kde = [u1 - q1.diff(), u2 - q2.diff()]
KM = KanesMethod(N, q_ind=[q1, q2], u_ind=[u1, u2], kd_eqs=kde)

forces = [
    (P1, -m1 * g_val * N.y),
    (P2, -m2 * g_val * N.y),
]

(fr, frstar) = KM.kanes_equations([Body1, Body2], forces)

# 提取符号质量矩阵和力向量
M_sym = trigsimp(KM.mass_matrix)
f_sym = trigsimp(KM.forcing)

print("M(q) =")
print(M_sym)
print("\nf(q, dq) =")
print(f_sym)

# 与文档中的公式比较
# M_doc = Matrix([...])  # 从文档抄入
# assert simplify(M_sym - M_doc) == zeros(2), "质量矩阵不匹配!"

4.5 验证工作流

1. 从文档中读取公式 → 构造 SymPy 表达式
2. 用 PyDy 从物理描述独立推导 EOM
3. simplify(文档公式 - PyDy推导) == 0 → 验证通过
4. 若不为零 → 定位差异项，检查文档错误

---

5. Wolfram Engine — 复杂符号化简兜底

5.1 安装

1. 下载 Wolfram Engine (免费开发者 License)
2. 激活: wolframscript -activate
3. 验证: wolframscript -code "1+1" → 输出 2

5.2 配置 MCP (Claude Code 集成)

(* 在 wolframscript 中执行 *)
PacletInstall["Wolfram/AgentTools"]
Needs["Wolfram`AgentTools`"]
Wolfram`AgentTools`InstallMCPServer["ClaudeCode", "Wolfram"]

自动写入 Claude Code 配置。重启即可使用。

MCP 暴露的工具: - WolframLanguageEvaluator — 执行任意 Wolfram 代码 - WolframLanguageContext — 获取上下文信息 - CodeInspector — 代码检查 - TestReport — 测试报告

5.3 通过 Python 调用 (无需 MCP)

import subprocess

def wolfram_eval(code: str) -> str:
    """调用本地 Wolfram Engine 执行符号计算"""
    result = subprocess.run(
        ['wolframscript', '-code', code],
        capture_output=True, text=True, timeout=30
    )
    return result.stdout.strip()

# 复杂化简
wolfram_eval('FullSimplify[Sin[x]^2 + Cos[x]^2]')
# → '1'

# 符号矩阵运算
wolfram_eval('''
M = {{a, b}, {b, c}};
Eigenvalues[M] // FullSimplify
''')

# 验证矩阵正定
wolfram_eval('''
Assuming[{a > 0, c > 0, a*c - b^2 > 0},
  PositiveDefiniteMatrixQ[{{a, b}, {b, c}}]]
''')
# → 'True'

5.4 Wolfram 独有优势场景

(* 1. 带假设的符号化简 — SymPy 经常失败的场景 *)
Assuming[{m > 0, l > 0},
  FullSimplify[Sqrt[m^2 * l^2]]]
(* → m*l *)

(* 2. 符号微分方程 *)
DSolve[m*x''[t] + b*x'[t] + k*x[t] == 0, x[t], t]

(* 3. 张量运算 (xAct 包) *)
<< xAct`xTensor`
DefManifold[M, 4, {a, b, c, d}]
DefMetric[1, g[-a, -b], cd, PrintAs -> "g"]

(* 4. 控制系统 *)
TransferFunctionModel[1/(m*s^2 + b*s + k), s]
BodePlot[%]

---

6. SageMath — 微分流形与李群

6.1 安装

# 方式 1: conda (推荐)
conda install -c conda-forge sage

# 方式 2: 系统包
sudo apt install sagemath

# 方式 3: Docker
docker run -it sagemath/sagemath

6.2 微分流形包 (01_数学方向)

# SageMath 中
M = Manifold(3, 'M')
c_xyz = M.chart('x y z')
x, y, z = c_xyz[:]

# 度量张量
g = M.riemannian_metric('g')
g[0, 0] = 1
g[1, 1] = 1
g[2, 2] = 1

# Christoffel 符号
nabla = g.connection()
print(nabla.coef()[:])

# Riemann 曲率张量
Riem = nabla.riemann()
print(Riem.display())

6.3 李群与李代数

# SageMath 中
L = LieAlgebra(QQ, cartan_type=['A', 1])
print(L.structure_coefficients())

6.4 何时用 SageMath

场景	SageMath 优势
01_数学: 流形上的计算	内建 Manifold 类，自动推导 Christoffel/Riemann
01_数学: 李群结构	内建分类与表示论
抽象代数验证	包装 GAP，群论计算最强

---

7. Cadabra — 张量指标运算

7.1 安装

# Ubuntu/Debian
sudo apt install cadabra2

# macOS
brew install cadabra2

7.2 张量计算示例

# Cadabra notebook 或 Python 脚本
from cadabra2 import *

__cdbkernel__ = create_scope()

# 声明指标与张量性质
{a, b, c, d, e}::Indices(position=free).
\partial{#}::PartialDerivative.
g_{a b}::Metric.
g^{a b}::InverseMetric.
g_{a b}::Symmetric.

# Christoffel 符号定义
ex := \Gamma^{a}_{b c} = 1/2 g^{a d} (
    \partial_{b}{g_{d c}} +
    \partial_{c}{g_{b d}} -
    \partial_{d}{g_{b c}}
);

canonicalise(_)

7.3 与机器人学的关联

• 空间向量代数中的交叉积张量: 6D 运动/力向量的叉积矩阵验证
• Adjoint 表示的指标运算: Ad_g 作用在 Lie 代数元素上的展开
• 曲率/挠率张量: 01_数学方向中微分几何内容的验证

---

8. 其他工具速览

8.1 Symbolica (Rust + Python)

pip install symbolica

from symbolica import Expression

x, y = Expression.symbol('x'), Expression.symbol('y')
e = (x + y)**3
expanded = e.expand()
print(expanded)

CERN 使用，有理数运算超 Mathematica。适合多项式密集计算。GitHub ~720 stars。

8.2 python-control

pip install control

import control as ct

# 传递函数
G = ct.tf([1], [1, 2, 1])  # 1/(s²+2s+1)

# 极点
print(ct.poles(G))

# 状态空间
A = [[0, 1], [-1, -2]]
B = [[0], [1]]
C = [[1, 0]]
D = [[0]]
sys = ct.ss(A, B, C, D)

# 可控性矩阵
print(ct.ctrb(A, B))

8.3 spatialmath-python (Peter Corke)

pip install spatialmath-python

from spatialmath import SE3, SO3

# SE(3) 变换
T = SE3.Rx(0.3) * SE3.Tz(1.0)

# Adjoint 矩阵
Ad = T.Ad()

# 李代数 (twist)
S = T.log()  # se(3) 元素

# 指数映射验证
T_recovered = SE3.Exp(S)

8.4 M4E (Multibody for Everybody)

git clone https://github.com/Project-SEA-Stack/Python_Multibody_for_Everybody

2026 年新发布。比 PyDy 更简洁 — 只需指定质心位置、关节位置、外力，自动推导符号 EOM。

---

9. 项目各方向验证方案速查

方向	验证对象	推荐工具	示例
01 数学	Lie 群公式、流形计算	SageMath / Wolfram	M.riemannian_metric()
01 数学	凸优化 KKT	SymPy	solve([diff(L,x), diff(L,lam)], ...)
03 SLAM	因子图/最小二乘	SymPy	J.T * W * J 符号运算
04 规控	轨迹优化、微分平坦	SymPy / Wolfram	变分法推导验证
05 足式	多体 EOM	PyDy	Kane 方法独立推导
05 足式	空间向量代数	SymPy + spatialmath	SE3.Ad() 矩阵验证
05 足式	QP/WBC 公式	SymPy	KKT + 矩阵正定性
05 机械臂	Jacobian/逆运动学	SymPy.mechanics	f.jacobian([q1, q2, ...])
05 机械臂	阻抗控制	SymPy + python-control	传递函数 + 稳定性
05 机械臂	力控公式	SymPy	力/力矩平衡方程
05 复合	全身动力学	PyDy	浮动基座 + 四肢建模
06 具身	RL 目标函数推导	SymPy	梯度/Hessian 验证

---

10. 自动化验证工作流

10.1 单公式验证脚本模板

#!/usr/bin/env python3
"""验证文档中的某个公式是否正确"""
from sympy import *

# 1. 定义符号
q1, q2 = symbols('q1 q2')
m, l, g = symbols('m l g', positive=True)

# 2. 文档中的公式 (手动输入)
doc_formula = ...

# 3. 从定义推导的公式
derived_formula = ...

# 4. 验证等价
diff_expr = simplify(doc_formula - derived_formula)
if diff_expr == 0:
    print("PASS: 公式验证通过")
else:
    print(f"FAIL: 公式不等价，差值: {diff_expr}")
    diff_trig = trigsimp(doc_formula - derived_formula)
    if diff_trig == 0:
        print("  (trigsimp 后通过)")
    else:
        print(f"  trigsimp 后差值: {diff_trig}")

10.2 批量验证流程

对每个教学章节:
  1. 提取关键公式 (人工标记或 LLM 辅助)
  2. 分类: 代数 / 动力学 / 控制 / 优化
  3. 路由到对应工具:
     - 代数      → SymPy/SymEngine
     - 动力学    → PyDy
     - 控制      → python-control
     - 复杂化简  → Wolfram
  4. 执行验证，输出报告

10.3 Agent 调用模式

# Claude Code 中直接通过 Bash 调用，无需 MCP

# 快速验证
python3 -c "
from sympy import *
x = Symbol('x')
print(simplify(sin(x)**2 + cos(x)**2))
"

# 文件形式
python3 verify_ch49_jacobian.py

---

11. 工具对比总表

特性	SymPy	SymEngine	PyDy	Wolfram	SageMath	Cadabra
语言	Python	C++/Py	Python	Wolfram	Python	C++/Py
安装	pip	pip	pip	独立	conda/apt	apt/brew
开源	Yes	Yes	Yes	免费License	Yes	Yes
GitHub Stars	~13k	~1.1k	~350	官方	~3.5k	~300
矩阵符号运算	Yes	Yes	via SymPy	强	Yes	—
微分/积分	Yes	Yes	—	强	Yes	—
化简能力	中	中	—	强	中-强	张量专用
多体动力学	mechanics	—	强	手动	—	—
张量指标	弱	—	—	xAct	—	强
微分几何	弱	—	—	Yes	强	Yes
控制理论	control	—	—	Yes	—	—
速度	慢	极快	取决SymPy	快	取决后端	快
Agent 可调用	Python	Python	Python	MCP/Py	Python	Python

---

附录 A: 安装一键脚本

#!/bin/bash
# 安装 Tier 1-2 符号计算工具
pip install sympy symengine pydy spatialmath-python control

echo "Tier 1-2 安装完成"
echo ""
echo "Tier 3 (可选):"
echo "  Wolfram Engine: https://www.wolfram.com/engine/"
echo "  SageMath:       conda install -c conda-forge sage"
echo "  Cadabra:        sudo apt install cadabra2"

附录 B: 参考资源

• SymPy 文档
• SymPy Mechanics
• PyDy 文档
• SymEngine
• Wolfram AgentTools
• SageMath 微分流形
• Cadabra 教程
• spatialmath-python
• python-control
• Symbolica
• M4E