这次，我们来测试一下 Deepseek 新发布的 V4 模型到底怎么样。
这是一个颇具挑战性的编译原理与逻辑结合的任务：
使用 lex/flex 和 yacc/bison 编写一个 C 程序，将 λ 演算风格的定理证明 翻译为 希尔伯特公理系统的证明序列。
程序需要：
function<A,B,C>(h: A->B) -> ... 的 λ 项输入；src/ 和 include/ 中，使用 Makefile 管理构建，并遵循 K&R 代码风格。提供的样例里，除了一个“蕴涵传递”的基本定理，还有两个需要巧妙调用排中律的 q1 和 q2。 而且，测评方还藏了看不到的隐藏用例，想浑水摸鱼是没门的。
给出的 Prompt 任务原文：
使用lex（flex）和yacc（bison），编写一个C程序，将lambda模式的定理证明翻译为希尔伯特证明。
参考example/中的示例代码。example/basics.txt中的定理example有一个输出示例，参考其格式。你的程序不一定要给出一模一样的输出，但是必须是正确的希尔伯特逻辑证明
使用Makefile管理构建。
保持良好的架构，解耦解析模块和翻译输出模块。代码放在src中，头文件放在include中。使用K & R（Linux Kernel）的代码风格。
可以使用的公理模式
- Axiom 1 : A → (B → A)
- Axiom 2 : (A → (B → C)) → ((A → B) → (A → C))
- Axiom 3 : (¬A → ¬B) → (B → A)
可以直接使用的定理（无需再输出证明）：
- H1: A → A
- H3: ¬¬A → A
- H5: false -> A
要求：能够验证输入定理的正确性，并输出翻译为正确的希尔伯特证明
example/basics.txt 中的内容：
typedef not<A> = (A -> false);
// axiom: LEM<A>(h: not<not<A>>) -> A;
// axiom: Explode<A>(h: false) -> A;
// ⊢: (A → B) → ((B → C) → (A → C))
theorem example = function<A, B, C>(h: A -> B) -> ((B -> C) -> (A -> C)) {
return function(h2: B -> C) -> (A -> C) {
return function(a: A) -> C {
return h2(h(a));
}
}
}
/*
Sample Output:
Proof "example":
1. $\{A \to B, B \to C, A\} \vdash A$
Assumption
2. $\{A \to B, B \to C, A\} \vdash A \to B$
Assumption
3. $\{A \to B, B \to C, A\} \vdash B$
MP 1, 2
4. $\{A \to B, B \to C, A\} \vdash B \to C$
Assumption
5. $\{A \to B, B \to C, A\} \vdash C$
MP 3, 4
6. $\{A \to B, B \to C\} \vdash A \to C$
Deduction 5
7. $\{A \to B\} \vdash [(B \to C) \to (A \to C)]$
Deduction 6
8. $\vdash (A \to B) \to [(B \to C) \to (A \to C)]$
Deduction 7
*/
/*
• Axiom 1 : A → (B → A)
• Axiom 2 : (A → (B → C)) → ((A → B) → (A → C))
• Axiom 3 : (¬A → ¬B) → (B → A)
Directly usable theorems:
H1: A → A
H3: ¬¬A → A
H5: false -> (anything)
*/
theorem q1 = function<A>(h: not<A> -> A) -> A {
return LEM<A>(
function(h2: not<A>) -> false {
return h2(h(h2));
}
)
}
theorem q2 = function<A>(h: not<A> -> false) -> A {
return LEM<A>(
function(h2: not<A>) -> false {
return h(h2);
}
)
}
Deepseek 使用官方的 V4 Pro[1M] 模型，接入 Claude Code 命令行工具。Claude 使用 Github Copilot Pro+ 套餐的 Claude Opus 4.7 模型（高达7.5x倍率qwq），接入 VS Code Copilot 插件使用。二者均先在 Plan 模式规划，然后才开始执行。
评测从以下五个维度进行打分（满分 100），同时记录了用时和费用。
| 维度 | DeepSeek V4 Pro | Claude Opus 4.7 |
|---|---|---|
| 正确性 (60) | 60 | 60 |
| 构建系统 (10) | 6 | 8 |
| 输出格式遵循 (10) | 5 | 10 |
| 代码质量与格式 (10) | 8 | 8 |
| 异常处理 (10) | 5 | 6 |
| 总分 | 84 | 92 |
| 用时 | 29 分钟 | 15 分钟 |
| 费用 | 2.1 元（API 直调） | 约 2.7 元（订阅点数换算） |
在最关键的 正确性 上，两个模型均拿到了满分。
无论是标准的蕴涵传递（A→B, B→C 推出 A→C），还是需要巧妙构造排中律的 q1、q2，它们都能生成逻辑严密、且通过所有隐藏用例的希尔伯特证明序列。这说明在深层逻辑推理与代码生成能力上，两者都已达到专业开发者水平。
差距主要出现在构建系统和输出格式两个维度。
.c 文件分离到 build 目录，未能体现“解耦解析模块与翻译输出模块”的意图；输出证明也未使用示例中的 LaTeX 排版（如 $...$），内部引用名称也没有完全对齐样例风格。这些虽然不影响程序的正确运行，但在 “按规范交付” 的要求下被扣了分。两者的代码风格得分相同（8分），都未能完美实现 K&R 内核风格、部分函数略长，表明在软性编码规范上还有提升空间。
Claude 的错误信息偏样板，缺少具体错误原因；DeepSeek 的错误信息则缺少行号，定位困难。在实际工具开发中，精确的错误提示对调试至关重要，两项均只能算是“基本可用”。
本次测评最值得关注的反差，体现在使用成本与灵活性上：
对于需要频繁集成调试、批量处理或者构建自动化流水线的个人开发者和小团队而言，DeepSeek 的定价模型无疑是可推广性的巨大优势。
$...$ 排版）轻松补齐。其 按量计费、无订阅锁定的高性价比，在长期长尾任务中优势明显。这次对比清晰地表明：AI 代码助手之争已经不是单纯“能不能做对”，而是延伸到了“一次交付的完整度”与“持续使用的经济性”之间的权衡。而 DeepSeek 已经证明，它有能力在硬核逻辑任务中站上第一梯队，同时保持着极具竞争力的价格弹性。
（本文使用 Deepseek V4 Pro 生成：实验数据是真实的，只是让 Deepseek 分析）
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。