跳转到内容

数学定义与职责推导

研究总览 · 2026-09-20

必要设计信息、表达与可满足域、责任转移及计算分工。

设需求为 (r=(q,H,J,L,\varepsilon)):已知参数 (q)、硬关系 (H)、软目标 (J)、允许修改域 (L)、验收误差 (\varepsilon)。(\Gamma) 是声明过的有界程序语法;(z\in Z_\Gamma(r)) 是结构选择;(x\in X_z(r)) 是连续参数;(p(z,x)) 是具体 AMIR 实现;(E_K) 是锁定环境 (K) 的几何求值。

求解任务是:

[ \operatorname{find} z,x\quad\text{s.t.}\quad H(r,z,x,E_K(p(z,x))) ]

并在已经验证可行的候选中改善 (J)。产品检查器返回 (V(r,E_K(p))\in{pass,fail,unknown})。求解器的 optimal、内核的 IsDone、程序成功运行分别属于不同层,均不能代替最终验收。

必须区分三个指标:

  1. 可表达域 (\mathcal E):能够由语言保留约定语义表达的工程模型与要求,包含可行和不可行要求。另记 (\mathcal F_\Gamma={r\mid\exists z,x:H(r,z,x,E_K(p(z,x)))}) 为声明构造域内的可满足需求集合;表达能力不能与有解混同。上述求解式描述整体工程模型中的几何/参数子问题,不声称包含全部时间行为或物理分析。
  2. 可检查域:检查器能以指定精度和证据可靠决定的谓词集合。
  3. 预算成功率 (S_{\mathcal D,B}=\Pr_{r\sim\mathcal D,\omega}[B\text{ 内找到并验证实现}]):依赖需求分布、算法、随机性及预算。

有限样本只估计第三项,不能证明前两项完备。已证无解、找到可行解和未知分别统计;确定性控制器与 AI 自主提出结构的表现分别统计。

TraceCurve、SolveConstraints、Extrude、Revolve、Sweep、Boolean、Pattern、Blend、OffsetShell、MorphG2、AlignFrame、KinematicJoint 可以组织成紧凑的能力目录。它们的数量不能证明实现复杂度、可判定性、表达完备性或求解效率。

  • Boolean 和开孔可以改变拓扑;不是单射,不能一般地逆推唯一输入。
  • Mirror 属于包含反射的欧氏变换,不能全部写成 SE(3)。
  • 残差与梯度不同;非光滑、退化及结构切换不能用一次自动微分消除。
  • 圆角、偏置、扫掠仍有自交、奇异性、相交求解与修剪拓扑问题。
  • G2 接缝、流形有效性、尺寸满足、可制造性和 Class-A 品质不是同一个谓词。

因此采用小而明确的能力契约,不采用“恰好十二个算子构成 CAD 完备基底”的理论宣称。

统一架构接收多种关系,但每种关系必须声明其求解和检查能力。机械尺寸/布局、草图、刚体装配、曲面接缝、制造规则分别注册到已有的同一契约中,不假装共有一个全能求解器。

材料强度、疲劳、热流、机床可达性等物理/工艺要求只有在指定模型、工况和验证器后才可检查。当前没有足够依据把它们纳入“全 CAD 自动验证”的承诺;对不支持的关系返回明确 unsupported/unknown。这个边界是本次范围裁决,不是待定选型。

对同一声明需求分布、精度和结果语义,首先比较 AI 的能力发现、语义理解与任务完成表现,并同时衡量内核实现/维护复杂度、端到端计算成本、可表达且可检查的设计范围。减少库数却增加大量特殊分支,或通过缩小任务范围取得更快结果,都不能自动视为改进。实现复杂度以独立数值底座、同类执行路径、特殊规则及必须维护的不变量为审查对象;代码行数只提供辅助信息。AI 面对的概念与推理负担按 §14.4 单独记录,不能从后端规模推定。

单次任务成本分解为:

[ T=T_{load}+T_{compile}+T_{search/solve}+T_{geometry}+T_{verify}+T_{commit}. ]

在保持能力、精度和失败语义的前提下,比较完整 T 的 P95 与内存;长期编辑同时考虑首次建模和重复修改的摊销。某种表示减少未知数,却使 Jacobian/Hessian 更稠密、条件数更差或编译更昂贵,可能整体更慢。这里需要寻找 Pareto 取舍,而不能将“变量最少”“库最少”“一个 API”单独当成最优目标。

本研究已有局部证据支持:独立 HiGHS 降低 LP-only 初始化负担;持久增量模型减少重复求解成本;语义降阶减少数值工作;部分消元平衡矩阵规模与求解时间;满足条件的截面构造省去三维布尔。解析降阶的正确性由 §13.1 推导,实验与限制见 §12。尚没有真实工业任务分布的数据证明整套方案处在全局最优取舍位置。

18. 从必要信息与求解责任推导核心架构

Section titled “18. 从必要信息与求解责任推导核心架构”

用户最新裁决是:不能依靠一点点试用、遍历所有设计来寻找架构;必须推导。 本研究停止扩展 §17 的封闭试用。本节从明确前提出发,推导应保留的信息、可以委托的推理、能力组合与执行组织;已有实验用于核对实现事实和局部成本,不作为枚举 CAD 世界后才能决策的前置条件。

本节的架构裁决是:以持久设计契约作为语义权威,以带类型和条件的关系作为组合单位,以编译器承担从设计关系到施工见证的推导,按数学结构执行,验证后原子提交。 特征与程序保留为构造机制和显式控制方式;当用户没有指定施工方法时,不把编写特征历史或构造程序作为必填输入。这是基于以下前提的工程选择,不是“任意 LLM 在所有 CAD 任务上必然更快”的定理。

推导使用四项前提:

  1. 产品须保持已声明的要求、编辑规则和身份语义,不能只生成当前外形。
  2. 设计者可以指定结果与关系,也可以明确授权系统在一个域内选择实现;系统不能代替设计者发明未授权偏好。
  3. 核心对所承诺的数学片段具有明确执行和检查能力;困难或超域时可以诚实返回未知,但不能把永远返回未知叫作求解能力。
  4. 优化目标是在正确性与资源边界内,减少 AI 必须掌握和提交的施工知识。实际模型成功率与实测延迟是另一类需要观测的结论。

因此,可以现在决定架构;无需等待穷举实验。尚未实现的编译规则、语义保持和检查连接仍是具体实现义务,不能因本节给出推理就宣称产品已经完成。

18.2 推导一:压缩操作知识,不能压掉设计意义

Section titled “18.2 推导一:压缩操作知识,不能压掉设计意义”

令设计状态为 D,承诺支持的观察为 O,编辑请求为 E,编辑后允许的状态由关系 T(D,e,D′) 描述。设计等价必须相对于这组承诺定义:在允许的观察与后续编辑序列下,两状态应有相同的可观察合法行为。只比较当前几何 G(D) 不够。

§17.5 给出了更弱但直接的必要条件:如果相同请求在两个设计中的合法结果集合互不相交,整个执行系统不能丢掉区分两者的信息,否则无法保证同时正确。仅有合法集合不同还不够推出这个结论,因为两集合可能共享一个正确结果。若承诺完整保留合法选择,则需要更强的行为等价条件。

这推出两个职责,而非要求 AI 阅读全部状态:

  • 核心保存充分语义:对象身份、关系、哪些量固定、哪些量开放、偏好、保持项和编辑规则;采用关系、公式或用户指定程序均可,但不能靠旧聊天记忆补齐。
  • 接口按任务投影语义:AI 修改板宽时,只需知道板宽可改、哪些关系保持、预计影响和未解决选择;内部孔位传播可由核心完成。

信息量也给出边界:若同一上下文仍有 N 个互斥的设计结果需要设计者区分,且没有已授权策略,那么固定长度二进制编码至少需要 ⌈log₂N⌉ 位;允许变长的前缀码也不能让所有结果都短于这个最坏情况界。增加上下文或授权默认值会减少剩余选择,不能把缺少信息说成“求解器会理解”。这里是可区分性的下界,不是 token 数或 LLM 推理量定律。

**架构结果:**权威状态必须保存设计契约;对外复杂度应通过任务相关投影与执行责任分配降低。把全部设计压成 B-Rep、坐标或无保持语义的命令历史,会失去必要信息;把全部内部状态每次灌给 AI,也不是信息保真的必要条件。

18.3 推导二:把“存在实现”交给核心,而不是要求 AI 提交实现

Section titled “18.3 推导二:把“存在实现”交给核心,而不是要求 AI 提交实现”

沿用 §2 的结构变量 z,本节把完整施工见证记为 w=(z,x,p,G):结构选择、数值参数、构造程序与实现几何。令 d 表示已形式化的设计要求、已给定值、授权选择域、偏好与误差契约,R(d,w) 表示见证满足它们。问题是:

[ \operatorname{find}\ w\quad R(d,w),\qquad \mathcal D_{feasible}={d\mid\exists w:R(d,w)}. ]

以必须提交 (d,w) 或足以生成 w 的程序作为比较基线时,关系接口接受 d,由核心寻找并检查 w。在核心确实承担该求解职责、且原接口确有额外必填施工信息的片段内,AI 的必填实现责任严格减少。 若既有参数化接口已经承担同一计算,则不能重复计算这部分收益;首次定义关系的成本也须计入。该结论不是整体描述长度或任意模型成功率的严格改进,具体比较前提见 §22.6。

哪些量属于 w,不能按“数值就是实现”机械划分。用户锁定的孔中心、制造顺序或拓扑身份是设计语义;只有相对于全部承诺语义可以由系统选择的量才可委托。同一个变量可以在不同请求中分别为已知量、待求设计量或内部辅助量。系统可以接受可选的构造见证、初值和提示,但没有必要把它们重新设为所有请求的必填项。

如果存在多个合法解,系统按显式目标或已授权选择策略选取;没有策略且差异有设计意义时,返回缺少的选择。求解状态至少分开:得到经核验的可行解、已证无解、预算内未知、能力不支持和需求信息不足。可行解不自动标为全局最优。

**架构结果:**核心新增的关键职责是 R→数学子问题→w 的编译与求解,而不是向 AI 暴露矩阵填写接口。让 AI 自己推导孔位公式后填进声明式 JSON,没有完成责任转移。

18.4 推导三:统一语义,按未知量与关系结构决定算法

Section titled “18.4 推导三:统一语义,按未知量与关系结构决定算法”

给定 x,计算 y=f(x) 是前向求值;给定 y,寻找满足 y=f(x) 的 x 是逆向求解。它们来自同一个关系,但逆问题可能多解、无解或困难。由此不能推出“全部写程序”或“全部送进优化器”。

对每项编译变换,区分两类承诺:

  • 保留可行域的变换:例如把 x=f(y) 代入其他关系,保留 x 的原始定义域、f 的定义条件,并提供恢复映射。消元后接受的解与原解对应;消除除法时不得丢掉分母非零条件,开方时不得丢掉分支。
  • 选择一个实现的变换:例如从多个合法布局中取一个。它只保证选中结果符合契约,不能冒充完整保留可行域;选择依据必须是已授权策略,且不能提前破坏后续联合约束的可行性。

据此得到执行规则,而无需逐个产品试验决定算法:

关系与变量结构 编译执行 保证边界
根输入已知,函数依赖无环且在域内单值有定义 常量传播、按依赖直接求值 保留单位、定义域与异常;输出仍须满足全部原约束与目标策略
存在带前提的等价参数化/消元 降维后求值或求解,再恢复原量 不能删掉分支、界、偏好和身份语义
剩余 LP、MILP、连续凸 QP 唯一 HiGHS 后端 整数域、最优性状态、数值证据各自核验
草图几何约束 PlaneGCS 只承诺其已接入的约束与诊断域
支持的可微非线性关系 CasADi/IPOPT 局部求解;失败不是全局无解证明
允许的有限结构选择 组合语法、条件子问题和可靠剪枝 有界域内讨论覆盖;预算耗尽为未知
只有已知前向构造能力 保留特征/程序执行与几何检查 不承诺自动反演任意程序

这些后端沿用 §1、§3 的成熟算法裁决,不增添平行库。分解依据是类型、已知/未知角色、代数结构与依赖图,而不是产品名称。若两个子图在固定边界变量后没有共享约束,并且目标也可分解,它们的可行性可独立求解再组合;若存在共享边界或目标耦合,则必须保留协调条件。稀疏图不能自动证明几何互不影响。

**架构结果:**设计语义是统一层,直接求值、数学求解与几何构造是编译目标。程序和特征不与关系模型竞争第二份权威;显式指定的程序属于契约,未指定时生成的程序属于实现。

18.4.1 程序为何能推导:规则、算法与 AI 的明确分工

Section titled “18.4.1 程序为何能推导:规则、算法与 AI 的明确分工”

用户进一步追问:“核心只是程序,并不是 AI,怎么会自己推导?”这里必须纠正“自己”的歧义:核心执行已定义语义上的形式推导与求解,不凭空理解自然语言、不自行发明新的几何语义或数学定理。 可算法化的推理不要求由语言模型执行;解方程、代入消元和按规则生成程序都可以由确定性程序完成。

所需机制有三层,不能用一句“交给求解器”跳过中间层:

层 输入与职责 规则从哪里来
意图形式化 将“等距、居中、边距至少……”变成带对象引用、单位、固定量和开放量的设计关系 AI/设计者表达;核心检查类型、缺项与歧义,不能靠类型检查证明已理解人的全部意图
关系编译 把每项几何关系转换为数学表达式、变量和边界,再按支持的规则代入、合并、消元 开发者定义基础对象与关系的数学语义、适用前提及检查方法;关系之间复用组合规则
求值、求解与核验 对生成的数学问题计算参数、选择授权域内的候选,构造并检查结果 成熟算法实现与已核对的构造机制;失败和未知按实际证据返回

例如 §18.5 的宽度子问题,在固定 n≥2、已声明排列方向与孔顺序后,基础定义可产生:

[ \begin{aligned} \text{圆孔横向边界}&: &&x_i-d/2,;x_i+d/2,\ \text{等距}&: &&x_{i+1}-x_i=p,\ \text{居中}&: &&x_1+x_n=W,\ \text{左右净边距}&: &&x_1-d/2\ge e,\quad W-x_n-d/2\ge e,\ \text{相邻净距}&: &&x_{i+1}-x_i-d\ge g. \end{aligned} ]

“圆孔”“等距”“居中”不是求解器认识的汉语词;它们是有上述语义的类型化关系。将等距等式相加,内部项抵消,得到 x_n−x_1=(n−1)p;结合居中与边距即可得到 §18.5 的区间。这里使用等式相加、代入和不等式整理,没有需要核心猜测的步骤。若当前编译器不能给出闭式式子,仍可把固定 n 的这些约束编译成稀疏 LP,在具体参数下求解;结果应按这一实际能力表述。

符号推导与数值求解不能混称。 §18.5 的通式是本研究对整个声明族的数学论证;若产品要自动生成同样的参数化通式和证明,就必须实现对应的符号规则、前提保持与推导记录。HiGHS 解决已建模的 LP/MIP/QP,不承担把几何意图翻译成约束;CasADi 提供表达式、自动微分及优化组件,其官方文档也明确区分它与完整计算机代数系统。不能从依赖中已有这两个库,推出关系编译或通式发现已经存在。HiGHS 官方介绍,CasADi 官方文档 §1.1

开发工作仍然存在,但粒度发生改变:定义可组合的几何关系和通用变换,供多种产品与正反向任务使用;不为每种产品、每组尺寸分别写施工流程。新需求若可用已有关系组合表达,就可复用编译与求解;若引入全新关系、未知物理规律或超出结构语法,核心不能自动获得能力。AI 可以提出新关系、构造程序或规则候选,但它们在获得明确语义与相应核验之前,只是建议,不能直接升级为可信基础规则。

因此本研究的创新是 AI 的意图表达与确定性数学编译协作:AI 保留开放问题的理解与设计选择职责,核心承担已形式化问题的可重复计算和检查。“设计关系驱动实现”是这个分工的名称,不是宣称普通程序突然具有任意创造能力。

18.5 一个符号推导覆盖整个声明族

Section titled “18.5 一个符号推导覆盖整个声明族”

以下用任意 n 推导,不再运行或增加尺寸样本。设固定整数 n≥2 个等直径 d>0 的圆孔,其中心沿平行于宽度轴的指定直线按序、等距 p 排列,板横向范围为 [0,W],孔组相对该范围居中;左右净边距至少 e≥0,相邻孔净距至少 g≥0。仅讨论这一宽度子问题,板高、厚度、通孔方向与实体有效性仍有独立条件;斜排与竖排不适用本公式。

等距与居中关系给出:

[ x_i=\frac W2+\left(i-\frac{n+1}{2}\right)p, \quad i=1,\ldots,n. ]

相邻孔净距要求 p−d≥g。最左与最右孔到边界的净距均为 (W−(n−1)p−d)/2,故:

[ d+g\le p\le\frac{W-2e-d}{n-1}. ]

因此这个宽度子问题可行,当且仅当:

[ \boxed{W\ge 2e+nd+(n-1)g}. ]

必要性来自区间非空;充分性是取 p=d+g 并代回全部宽度关系。若目标为最小板宽,则 W*=2e+nd+(n−1)g、p*=d+g。若 p 已被设计者固定,则检查 p≥d+g 与 W≥2e+d+(n−1)p。若 W 固定但没有选择 p 的策略,则保留整个允许区间;“可取最小 p”是可行性见证,不是自动获得的设计偏好。n=1 单独得到 x₁=W/2、W≥2e+d,不调用含 n−1 分母的规则。

该推导对任意满足前提的整数 n 和实数参数成立,不需要测试每一个 n、W、d、e、g。它从共用关系得到可行域、恢复公式和逆向最小值。e=0 或 g=0 可能发生几何接触,形式上的宽度可行不自动证明 OCCT 可交付有效实体;若要求严格分离却不给正裕量,最小值可能退化为不可达到的下确界。实际接受域须明确净距裕量、数值容差和几何检查。

这里真正需要创新的是:这些公式应由核心根据“等距、居中、边距、净距”的共同定义导出或通过带前提的规则实例化。AI 只表达关系,不手写这个推导。 只内置一个支持任意 n 的排孔函数,仍可能只是参数化模板;共同关系编译、正反向复用推导才是本架构职责。增加圆周布局时需增加圆周相关的语义与数学规则;旧线性排列的定理不能直接外推。这是按数学片段扩展语言,不是按所有产品形状逐件编程。

18.6 推导四:用契约和组合规律发现能力,不建立产品模板全集

Section titled “18.6 推导四:用契约和组合规律发现能力,不建立产品模板全集”

单项能力至少给出输入/输出类型、单位、前提 P、效果或关系 Q、读写范围、未修改部分的保证、选择语义以及失败后的状态。输出符合下一能力的类型只说明接口能连接;不说明几何前提、约束、权限和资源条件已经满足。

对于具有明确顺序执行语义的 A、B,Dijkstra 的总正确性最弱前置条件满足:

[ wp(A;B,Q)=wp(A,wp(B,Q)). ]

这个等式包含终止要求;它不是“任意程序的最弱前提都能自动算出”的算法。实际核心可在支持的片段中使用可靠的充分前提与有限证明规则;超域时保留未知,不能凭无法证明就把可用能力永久隐藏。Dijkstra,EWD418 §3

声明式联合求解与顺序调用还必须区分:A 允许 x∈[0,1],B 要求 x=1;存在共同解,但若先执行 A 并永久选 x=0,B 就失败。关系组合应保留 A∧B 一起求解,或具有明确的回溯/重新选择语义;不能把逐操作贪心当作等价实现。

由此得到能力发现的具体组织:按对象类型和所需效果检索相关关系,绑定当前对象与已知条件,显示尚缺的前提和允许的组合;详细求解算法、矩阵和构造顺序留在核心。描述、schema、前提检查、编译与诊断引用同一份语义定义,避免 AI 学会的说明与执行事实不同。

为什么不用列全产品?设语言有有限个构造与组合规则。若每个基础规则在其前提内正确,每种组合保持声明的不变量,则可对合法表达式的结构作归纳,证明该语言片段的所有有限组合具有所声明的性质。证明义务落在规则和组合处,无需列出每个产品实例。

这只给出语言片段的正确性,不证明它表达全部 CAD,也不自动解决所有组合的搜索。类型/条件能机械排除确定不适用的组合,降低无效选择;能排除多少、某个 AI 是否更快发现合法组合,不能从目录结构直接推出。

**架构结果:**核心应提供可组合的对象、属性、关系和作用规则,产品模板可作为展开到这些规则的派生便利能力。新抽象只有保存前提与效果才能获得原规则的保证;频繁出现或程序压缩成功不等于新能力已被证明。

18.7 推导五:正确性交给组合论证,困难性用边界管理

Section titled “18.7 推导五:正确性交给组合论证,困难性用边界管理”

对已形式化的 d,编译器生成数学问题 M_d;求解得到 v;恢复映射产生施工见证与几何。令 S 为提交前完整设计状态,S′ 为候选提交状态,G(S′) 为其中的几何;完整状态还包含持久关系、身份、编辑与历史语义。要推出已提交结果符合要求,需要逐层建立:

[ M_d(v)\land BuildOK(v,G(S’))\land Check(d,G(S’))=pass \land SemanticBind(d,v,S’)\land CommitInvariant(S,S’) ;\Longrightarrow; Contract_\varepsilon(d,S’). ]

这条蕴含式是待实现系统必须满足的组合证明义务:编译规则不能漏掉要求,求解见证应被核验,构造语义须与数学量对应;SemanticBind 要求候选状态正确保存要求、开放域、身份、引用和编辑语义,并将它们绑定到对应实现。CommitInvariant 约束前后状态的权限、保持项、原子性及历史一致性;最终验收与提交必须是同一修订的同一对象。只验证 G(S′) 不能证明完整状态正确,因为相同形状可以对应不同编辑行为。单位、误差模型和语义映射全程一致;可信构件与未经证明的环节须写明,不能只画一条流水线便声称已经完成形式验证。独立检查减少共同错误风险,但“独立”本身不是正确性证明。

语义保持的编译可让源层性质传到执行结果,CompCert 是这一思想的已有严格实现;Aira 当前没有相当的机器证明,本节不作等同宣称。CompCert 官方手册 §1

该论证主要处理交付可靠性。要证明某片段所有可行请求都能被求出,还需完整的可行域变换、完备搜索/算法及相应资源条件;有可靠检查器不代表找解器完备,返回 unknown 保证诚实而不保证有用。

一般困难性也可以推导:如果结构选择语言允许任意布尔变量及子句约束,那么可以把一个 SAT 实例直接写成该子语言的可行性问题。故对所有此类输入承诺多项式时间内完整求解,会蕴含 P=NP。这里是条件性复杂度结论,不是声称 P≠NP 已获证明。Cook,1971 原文

所以取舍点是明确的:常见结构用可证明的参数化、消元与分解降低难度;剩余任务用适用的成熟算法;一般离散选择和非凸问题保留预算与证明边界。无需用大量人类操作来“解决”计算复杂性,也不能用一个 solve 入口掩盖它。完整性、可靠性与预算效率须分别声明。

18.8 复杂度与效率的平衡,不以最少工具或最多求解为目标

Section titled “18.8 复杂度与效率的平衡,不以最少工具或最多求解为目标”

对同一正确性、能力域和需求,将成本分成 AI 的表达/发现/施工推理,以及核心的编译、搜索、构造、检查和提交。把一个推导从 AI 转给核心,减少的是 AI 的责任;是否降低总延迟取决于新增机器成本与省去的推理、交互、重复执行和修复成本之差。数学不能在没有成本模型时证明每次转移都更快。

但可以据结构作出当前设计决定:

  1. 已知量直接计算,不创建多余优化变量;用 §18.5 一类规则一次处理整个参数族。
  2. 只在保存原域、分支与语义的前提下消元;若消元导致稠密耦合或昂贵恢复,则保留边界变量。规则选择不能只最小化变量数。
  3. 只有关系、查询成员或语义保持条件受影响的部分需要重新编译/求解;几何相互作用必须包含在依赖中。已有可行状态、分解与证据在适用条件保持时复用。
  4. 新关系抽象从已有可检查规则组合而来,保存其前提与展开;检索和编译成本高于省下的工作时不强制采用。
  5. 同类成熟算法只保留一个生产后端;不同问题类的专用后端不是同义冗余。每个后端对内负责算法,对外服从同一设计契约。

本架构因此选择“设计关系清楚、施工责任可委托、执行按结构专门化”的平衡点。它没有要求最小语言覆盖一切,也没有把所有参数交给一个大优化问题。已有 §12 测量为局部成本提供证据;本节不再通过追加产品样本寻找这个职责分界。

职责推导收敛到统一持久设计图、关系编译和专用执行;具体模型、算法与构造性论证统一见 §22。能力发现与受验证约束的抽象机制见 §16,成熟算法选择见 §3。不把本节重新维护为另一份实施清单。