在AMD平台上跑LLM的尝试

之前尝试在Intel的Lunar Lake平台上跑LLM，遇到了很多困难，性能也不够理想。趁着AMD Strix Halo新品发布，买入了一台新电脑，并且立刻用它跑起了LLM。

AMD的计算框架是ROCm。虽然比不上CUDA在业界的受欢迎程度，但还是比Intel的情况好了许多：Ollama在Strix Halo上做到了“开箱即用”，真是令人欣慰。

我的内存足够跑30B参数的模型，不过跑起来相当吃力，每秒不到10个token。跑4B参数的模型则轻轻松松，能跑到45 token/s。

我还跑了Qwen3:30b-a3b。它是一个MoE模型，是兼顾参数大小和运行速度的一个折衷选项。它令人满意地回答了我之前常用来测试AI智力的一个数学问题，这个问题是要求AI证明以下命题：

对任意0<x<π/2，cot x < 1/x - x/3。

这个问题比较简便的做法是把 cot x 展开成洛朗级数。如果叫我做的话，我必须查阅数学手册，因为我并不知道cot x的级数形式。

其他一些小模型也不知道cot x的级数形式，于是会采用传统的定义函数—求导—求值域的证明方法。这个方法大概是可行的，只是计算比较繁琐，这些模型一般算不对。还有很多模型只会硬凑答案，并不能给出严格的证明过程。实际上，就在大约一年前，ChatGPT和Gemini都没法满意地回答这个问题（当然，现在它们都足够聪明了）。

可见，技术的发展真是日新月异：一年前顶尖的云端模型无法解决的问题，一年后只需要一台小小的个人电脑就能解决了。

下面是对话内容。

USER

以下命题是否成立？
对任意0<x<π/2，cot x < 1/x - x/3。

ASSISTANT

Thought for 68 seconds

好的，我现在需要判断这个命题是否成立：对于任意0 < x < π/2，cot x < 1/x - x/3。首先，我得回忆一下cot x的定义，cot x就是cos x除以sin x，也就是cot x = cos x / sin x。而右边的表达式是1/x - x/3。我需要比较这两个表达式在0到π/2之间的大小关系。

首先，可能需要将两边的表达式进行比较，或者考虑它们的差是否小于零。也就是说，检查cot x - (1/x - x/3) < 0是否成立。或者，可能需要通过泰勒展开来近似比较这两个函数的大小。

不过，泰勒展开可能需要考虑x的范围。比如，对于x接近0的情况，cot x的泰勒展开是1/x - x/3 - x^3/45 + …，而右边的表达式是1/x - x/3。所以，如果cot x的泰勒展开是1/x -x/3 -x^3/45 + …，那么cot x应该小于1/x -x/3，因为后面的项是负的。这可能意味着在x接近0的时候，这个不等式成立。但需要确认是否在所有0 < x < π/2都成立。

不过，当x趋近于π/2时，cot x趋近于0，而右边的表达式1/x -x/3，当x接近π/2时，比如x=π/2，代入的话，1/(π/2) - (π/2)/3 = 2/π - π/6 ≈ 0.6366 - 0.5236 ≈ 0.113。而cot(π/2) = 0，所以这时候0 < 0.113，不等式成立。所以在x接近π/2时，不等式也成立。

那中间的某个点是否可能不成立呢？比如，是否存在某个x在0到π/2之间，使得cot x ≥ 1/x -x/3？

可能需要构造函数f(x) = cot x - (1/x -x/3)，然后分析f(x)的符号。如果f(x)在0到π/2之间始终小于0，那么命题成立。

或者，考虑函数f(x) = cot x + x/3 - 1/x，然后判断f(x) < 0是否成立。这时候可能需要求导，分析函数的单调性或者极值。

先尝试计算f(x) = cot x + x/3 - 1/x。求导的话，f’(x) = -csc²x + 1/3 + 1/x²。不过这个导数可能比较复杂，难以直接分析。

或者，考虑泰勒展开。比如，cot x的泰勒展开式在x接近0时是1/x - x/3 - x^3/45 - 2x^5/945 - …。而右边的表达式是1/x -x/3。所以，当x接近0时，cot x = 1/x -x/3 -x^3/45 + …，所以cot x - (1/x -x/3) = -x^3/45 + …，这显然是负数，所以此时不等式成立。

当x增大时，比如x趋近于π/2，cot x趋近于0，而右边的表达式是1/x -x/3。比如当x=π/4时，cot(π/4)=1，右边是1/(π/4) - (π/4)/3 = 4/π - π/12 ≈ 1.273 - 0.2618 ≈ 1.0112。此时cot x=1 < 1.0112，所以不等式成立。

再比如x=π/3≈1.047，cot(π/3)=1/√3≈0.577。右边是1/(π/3) - (π/3)/3 = 3/π - π/9 ≈ 0.9549 - 0.3491 ≈ 0.6058。所以0.577 < 0.6058，不等式成立。

再试一个x=π/6≈0.523。cot(π/6)=√3≈1.732。右边是1/(π/6) - (π/6)/3 = 6/π - π/18 ≈1.9099 - 0.1745≈1.7354。这时候cot x≈1.732 < 1.7354，所以不等式成立。

看起来在这些点上都成立，但需要更严格的证明。

另一种方法是利用已知的不等式。例如，cot x的泰勒展开式在x>0时，是否总是有cot x < 1/x -x/3？

或者，考虑使用积分或级数比较。或者寻找已知的不等式。

例如，根据一些数学文献，cot x的展开式为cot x = 1/x - x/3 - x^3/45 - 2x^5/945 - …，所以对于x>0，cot x < 1/x -x/3，因为后面的项都是负的。因此，这个不等式可能成立。

但需要确认这个泰勒展开是否正确。比如，cot x的泰勒级数展开式是否确实如此。

查一下cot x的泰勒展开式。根据数学手册，cot x的展开式在x接近0时是：

cot x = 1/x - x/3 - x^3/45 - 2x^5/945 - …

所以，对于x>0足够小，cot x = 1/x -x/3 - (x^3)/45 - …，所以cot x < 1/x -x/3，因为后面的项都是负的。因此，在x接近0时成立。

而当x增大时，比如在0到π/2之间，是否所有项都是负的？或者是否存在某些x使得后面的项可能变为正？

不过，泰勒级数的收敛性可能需要考虑。对于x在0到π/2之间，泰勒级数是否收敛？

不过，cot x的泰勒级数展开在x=0处的收敛半径是π，因为cot x在x=0处有极点，所以泰勒级数在|x| < π时收敛。因此，在x∈(0, π/2)时，泰勒级数是有效的。因此，cot x = 1/x -x/3 -x^3/45 -2x^5/945 - …，所有后面的项都是负的。因此，cot x < 1/x -x/3，因为减去了正的项。

因此，命题成立。

不过，可能需要更严谨的证明，比如通过数学归纳法或利用函数的单调性。

或者，考虑将不等式转化为cot x + x/3 < 1/x，然后两边乘以x（因为x>0），得到x cot x + x^2/3 < 1。然后分析x cot x + x^2/3 <1是否成立。

x cot x = x * cos x / sin x。而x cot x的展开式是x*(1/x -x/3 -x^3/45 - …) = 1 -x^2/3 -x^4/45 - …，所以x cot x +x^2/3 = 1 -x^4/45 - … <1。因此，x cot x +x^2/3 <1，即原式成立。

因此，命题成立。

不过，可能需要验证这个推导是否正确。比如，x cot x = x * cos x / sin x。而根据泰勒展开，cos x = 1 -x^2/2 +x^4/24 -…, sin x =x -x^3/6 +x^5/120 -…, 所以cot x = cos x / sin x = [1 -x^2/2 +x^4/24 - …]/[x -x^3/6 +x^5/120 - …] = (1/x) * [1 -x^2/2 +x^4/24 - …]/[1 -x^2/6 +x^4/120 - …]。然后用泰勒展开除法，得到1/x * [1 -x^2/2 +x^4/24 - …] * [1 +x^2/6 + (x^4/6^2 + …)]，乘积后得到1/x * [1 -x^2/2 +x^4/24 +x^2/6 + …] = 1/x * [1 -x^2/3 + …]，即1/x -x/3 -x^3/45 + …。因此，x cot x = 1 -x^2/3 -x^4/45 + …，所以x cot x +x^2/3 =1 -x^4/45 + … <1。因此，对于x>0，x cot x +x^2/3 <1，即原不等式成立。

因此，命题成立。

根据数学分析，该命题成立。以下是详细推导过程：

  1. 泰勒展开分析
    对于 \(0 < x < \frac{\pi}{2}\)，\(\cot x\) 的泰勒展开式为： $$ \cot x = \frac{1}{x} - \frac{x}{3} - \frac{x^3}{45} - \frac{2x^5}{945} - \cdots $$ 右侧表达式为 \(\frac{1}{x} - \frac{x}{3}\)，而 \(\cot x\) 的展开式中后续项均为负数（如 \(-\frac{x^3}{45}\) 等），因此： $$ \cot x < \frac{1}{x} - \frac{x}{3} $$

  2. 函数构造与不等式验证
    定义函数 \(f(x) = \cot x - \left( \frac{1}{x} - \frac{x}{3} \right)\)，则： $$ f(x) = \cot x - \frac{1}{x} + \frac{x}{3} $$ 根据泰勒展开，\(f(x)\) 的展开式为： $$ f(x) = -\frac{x^3}{45} - \frac{2x^5}{945} - \cdots < 0 \quad \text{（对所有 } x > 0 \text{ 成立）} $$

  3. 边界情况验证

    • 当 \(x \to 0^+\)：\(\cot x \approx \frac{1}{x} - \frac{x}{3} - \frac{x^3}{45}\)，显然 \(\cot x < \frac{1}{x} - \frac{x}{3}\)。
    • 当 \(x \to \frac{\pi}{2}^-\)：\(\cot x \to 0\)，而 \(\frac{1}{x} - \frac{x}{3} \approx \frac{2}{\pi} - \frac{\pi}{6} \approx 0.113 > 0\)，不等式成立。

  4. 数值验证

    • 取 \(x = \frac{\pi}{4}\)：
      \(\cot\left(\frac{\pi}{4}\right) = 1\)，右侧 \(\frac{1}{\pi/4} - \frac{\pi/4}{3} \approx 1.273 - 0.262 = 1.011\)，满足 \(1 < 1.011\)。
    • 取 \(x = \frac{\pi}{6}\)：
      \(\cot\left(\frac{\pi}{6}\right) = \sqrt{3} \approx 1.732\)，右侧 \(\frac{6}{\pi} - \frac{\pi}{18} \approx 1.909 - 0.174 = 1.735\)，满足 \(1.732 < 1.735\)。

结论：对于所有 \(0 < x < \frac{\pi}{2}\)，不等式 \(\cot x < \frac{1}{x} - \frac{x}{3}\) 恒成立。

USER

你的这个分析要成立，恐怕需要严格证明 cot x 的泰勒展开式中，后续项的系数全部为负吧？

ASSISTANT

Thought for 81 seconds

好的，用户提出了一个关键点，就是需要严格证明cot x的泰勒展开式中后续项的系数都是负数。我之前只是提到了泰勒展开式，并没有详细说明为什么这些后续项都是负的。用户可能对数学分析有一定了解，所以需要更严谨的证明。

首先，我需要确认cot x的泰勒展开式是否正确。记得cot x在x=0附近的展开式确实是1/x - x/3 - x^3/45 - …，但可能用户需要更详细的推导过程。不过，用户的问题是关于这些后续项的符号是否为负，所以需要证明这些系数都是负的。

接下来，我应该考虑如何证明这些系数都是负数。可能的方法包括使用已知的泰勒级数展开，或者利用函数的导数性质。比如，可以考虑cot x的泰勒级数展开式，或者利用其与伯努利数的关系。

另外，用户可能对泰勒级数的收敛性或系数的符号有疑问，所以需要更深入的分析。例如，cot x的泰勒级数展开式中的系数是否确实为负？或者是否可以通过某种不等式来证明？

可能需要查阅cot x的泰勒展开式的具体形式。根据数学资料，cot x的展开式确实可以表示为：

cot x = 1/x - x/3 - x^3/45 - 2x^5/945 - …

其中每个后续项的系数都是负的。但需要证明这一点。可能的方法是利用cot x的幂级数展开，或者通过递推公式计算系数。

另一个思路是利用cot x的导数。cot x的导数是 -csc²x，而csc²x的展开式可能有助于推导。不过这可能比较复杂。

或者，可以考虑将cot x与已知的级数展开式比较。例如，cot x的级数展开式通常与伯努利数相关，其通项公式为：

cot x = 1/x + Σ_{n=1}^∞ (-1)^n 2^{2n} B_{2n} x^{2n-1} / (2n)! )

其中B_{2n}是伯努利数。根据伯努利数的性质，B_{2n}的符号是交替的吗？或者是否有特定的规律？

查阅伯努利数的符号：伯努利数B_2n的符号是正的当n为奇数，负的当n为偶数？或者可能需要具体数值。例如，B_2 = 1/6，B_4 = -1/30，B_6 = 1/42，B_8 = -1/30，依此类推。因此，对于n≥1，B_{2n}的符号是(-1)^{n+1}？比如B_2 = +1/6，B_4 = -1/30，B_6 = +1/42，B_8 = -1/30，所以符号是交替的。因此，在cot x的展开式中，每个项的系数为：

(-1)^n * 2^{2n} * B_{2n} / (2n)!

由于B_{2n}的符号为(-1)^{n+1}，所以整个系数变为：

(-1)^n * 2^{2n} * (-1)^{n+1} / (2n)! ) = -2^{2n} / (2n)! * (-1)^{2n+1} ?

可能这里需要更仔细的计算。例如，假设B_{2n} = (-1)^{n+1} * |B_{2n}|，那么代入后：

cot x = 1/x + Σ_{n=1}^∞ [ (-1)^n * 2^{2n} * (-1)^{n+1} * |B_{2n}| / (2n)! ) ] x^{2n-1}

化简系数：

(-1)^n * (-1)^{n+1} = (-1)^{2n+1} = -1

因此，每个项的系数为 -2^{2n} |B_{2n}| / (2n)! ，所以整个展开式为：

cot x = 1/x - Σ_{n=1}^∞ [ 2^{2n} |B_{2n}| / (2n)! ) ] x^{2n-1}

因此，所有后续项的系数都是负的，因为|B_{2n}|是正数，而前面的负号使得每个项都是负的。因此，cot x的泰勒展开式中的所有x的奇次幂项的系数都是负的，这说明对于足够小的x，cot x < 1/x - x/3，因为后面的项都是负的，所以整体小于1/x -x/3。

不过，这里需要注意的是，泰勒级数的收敛性。cot x的泰勒级数在x=0附近是否收敛？可能需要确认展开式的收敛半径。不过对于x在0到π/2之间，泰勒级数可能在某个邻域内有效，但具体到整个区间0 < x < π/2，可能需要进一步分析。不过根据展开式的形式，每个项的系数都是负的，因此对于所有x>0，cot x的泰勒展开式中的各项都是负的，因此cot x = 1/x - x/3 - (x^3/45 + …) < 1/x -x/3。

不过，用户可能还关心是否在x接近π/2时，这个不等式仍然成立。比如，当x接近π/2时，cot x趋近于0，而1/x -x/3的值是多少？例如，当x=π/2时，1/x ≈ 0.6366，x/3 ≈ 0.5236，所以1/x -x/3 ≈ 0.113，而cot(π/2)=0，所以0 < 0.113成立。因此，即使在x接近π/2时，不等式也成立。

另外，用户可能担心在x接近0时，泰勒展开式的截断误差是否会影响结论。例如，当x非常小时，cot x ≈1/x -x/3 -x^3/45，所以1/x -x/3 -x^3/45 <1/x -x/3，因此cot x <1/x -x/3。因此，无论x在0到π/2的哪个位置，只要泰勒展开式中的后续项都是负的，那么不等式就成立。

总结来说，通过分析cot x的泰勒级数展开式中的系数符号，可以证明后续项均为负，因此原命题成立。需要将这些步骤详细说明，确保用户理解每个步骤的正确性。

您提出的质疑非常关键。为了严格证明该不等式成立，必须证明 \(\cot x\) 的泰勒展开式中后续项的系数均为负。以下是详细的数学证明：

1. \(\cot x\) 的泰勒级数展开

\(\cot x\) 在 \(x \to 0\) 时的泰勒展开式为： $$ \cot x = \frac{1}{x} - \frac{x}{3} - \frac{x^3}{45} - \frac{2x^5}{945} - \cdots $$ 所有后续项的系数均为负数，这可以通过以下方式严格证明。

2. 利用伯努利数的性质

\(\cot x\) 的泰勒级数可以表示为： $$ \cot x = \frac{1}{x} + \sum_{n=1}^{\infty} \frac{(-1)^n 2^{2n} B_{2n} x^{2n-1}}{(2n)!} $$ 其中 \(B_{2n}\) 是第 \(2n\) 个伯努利数。根据伯努利数的性质：

  • \(B_{2n}\) 的符号为 \((-1)^{n+1}\)（即：\(B_2 = \frac{1}{6}, B_4 = -\frac{1}{30}, B_6 = \frac{1}{42}, \dots\)）。

代入后，展开式变为： $$ \cot x = \frac{1}{x} + \sum_{n=1}^{\infty} \frac{(-1)^n 2^{2n} (-1)^{n+1} |B_{2n}| x^{2n-1}}{(2n)!} $$ 化简系数： $$ (-1)^n \cdot (-1)^{n+1} = (-1)^{2n+1} = -1 $$ 因此，展开式为： $$ \cot x = \frac{1}{x} - \sum_{n=1}^{\infty} \frac{2^{2n} |B_{2n}| x^{2n-1}}{(2n)!} $$ 由于 \(|B_{2n}| > 0\)，所有后续项的系数均为负数。

3. 函数构造与不等式验证

定义函数： $$ f(x) = \cot x - \left( \frac{1}{x} - \frac{x}{3} \right) = -\frac{x^3}{45} - \frac{2x^5}{945} - \cdots $$ 显然，\(f(x) < 0\) 对所有 \(x > 0\) 成立，因此： $$ \cot x < \frac{1}{x} - \frac{x}{3} $$

4. 边界情况与数值验证

  • 当 \(x \to 0^+\)：
    \(\cot x \approx \frac{1}{x} - \frac{x}{3} - \frac{x^3}{45}\)，显然 \(\cot x < \frac{1}{x} - \frac{x}{3}\)。
  • 当 \(x \to \frac{\pi}{2}^-\)：
    \(\cot x \to 0\)，而 \(\frac{1}{x} - \frac{x}{3} \approx \frac{2}{\pi} - \frac{\pi}{6} \approx 0.113 > 0\)，不等式成立。

结论

通过伯努利数的性质和泰勒展开式的严格分析，可以证明 \(\cot x\) 的泰勒展开式中所有后续项的系数均为负数。因此，对于任意 \(0 < x < \frac{\pi}{2}\)，不等式： $$ \cot x < \frac{1}{x} - \frac{x}{3} $$ 恒成立。

分享