这次，我们来测试一下 Deepseek 新发布的 V4 模型到底怎么样。

任务简介

这是一个颇具挑战性的编译原理与逻辑结合的任务：
使用 lex/flex 和 yacc/bison 编写一个 C 程序，将 λ 演算风格的定理证明 翻译为 希尔伯特公理系统的证明序列。
程序需要：

• 解析类似 function<A,B,C>(h: A->B) -> ... 的 λ 项输入；
• 利用给定的三条公理模式（A1-A3）和三个可直接引用的定理（H1, H3, H5）；
• 通过演绎定理（Deduction Theorem）和 MP 规则，逐步输出带 LaTeX 排版的希尔伯特风格证明；
• 代码需放置在 src/ 和 include/ 中，使用 Makefile 管理构建，并遵循 K&R 代码风格。

提供的样例里，除了一个“蕴涵传递”的基本定理，还有两个需要巧妙调用排中律的 q1 和 q2。 而且，测评方还藏了看不到的隐藏用例，想浑水摸鱼是没门的。

使用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

要求：能够验证输入定理的正确性，并输出翻译为正确的希尔伯特证明

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），同时记录了用时和费用。

核心能力：正确性齐平，均通过全部测试

在最关键的 正确性 上，两个模型均拿到了满分。
无论是标准的蕴涵传递（A→B, B→C 推出 A→C），还是需要巧妙构造排中律的 q1、q2，它们都能生成逻辑严密、且通过所有隐藏用例的希尔伯特证明序列。这说明在深层逻辑推理与代码生成能力上，两者都已达到专业开发者水平。

工程细节与格式遵循：Claude 更显“规矩”

差距主要出现在构建系统和输出格式两个维度。

• DeepSeek 生成的 Makefile 没有将 flex/bison 生成的 .c 文件分离到 build 目录，未能体现“解耦解析模块与翻译输出模块”的意图；输出证明也未使用示例中的 LaTeX 排版（如 $...$），内部引用名称也没有完全对齐样例风格。这些虽然不影响程序的正确运行，但在 “按规范交付” 的要求下被扣了分。
• Claude 则严格遵循了所有显式与隐式约定，Makefile 整洁、输出格式甚至与样例几乎一模一样，展现出更好的 指令细节遵循能力。

两者的代码风格得分相同（8分），都未能完美实现 K&R 内核风格、部分函数略长，表明在软性编码规范上还有提升空间。

异常处理：均不够“开发者友好”

Claude 的错误信息偏样板，缺少具体错误原因；DeepSeek 的错误信息则缺少行号，定位困难。在实际工具开发中，精确的错误提示对调试至关重要，两项均只能算是“基本可用”。

成本与灵活性：DeepSeek 的显著优势

本次测评最值得关注的反差，体现在使用成本与灵活性上：

• DeepSeek 直接通过 API 按量计费，完成一次复杂任务仅需 2.1 元，无需预付费，无每日限额，可随时并发调用。
• Claude 的测评费用约 2.7 元，但这是建立在 GitHub Copilot Pro+ 订阅（每月 260 元人民币） 的基础之上，且该订阅面临暂停新用户注册和限量等问题。实际开发中很可能遭遇用至半途被限流的窘境，且每月无论是否用完都要支付 260 元。若改为直接调用 Claude 官方 API，同等规模的 token 消耗很可能飙升至 15 元以上，成本增加数倍。

对于需要频繁集成调试、批量处理或者构建自动化流水线的个人开发者和小团队而言，DeepSeek 的定价模型无疑是可推广性的巨大优势。

综合评语

• Claude Opus 4.7 更像一位经验丰富的“交付专家”：一次生成接近成品，能精准扣住所有格式约束，适合预算充足、追求零修改的直接部署场景。
• DeepSeek V4 Pro 则是一名逻辑能力顶尖、但细节上稍显粗犷的“效率先锋”：它在核心正确性上毫不逊色，仅因工程规范与格式呈现被扣分，而这些完全可以通过更精细的提示词（例如预先提供理想的 Makefile 模板、明确要求 $...$ 排版）轻松补齐。其 按量计费、无订阅锁定的高性价比，在长期长尾任务中优势明显。

这次对比清晰地表明：AI 代码助手之争已经不是单纯“能不能做对”，而是延伸到了“一次交付的完整度”与“持续使用的经济性”之间的权衡。而 DeepSeek 已经证明，它有能力在硬核逻辑任务中站上第一梯队，同时保持着极具竞争力的价格弹性。

（本文使用 Deepseek V4 Pro 生成：实验数据是真实的，只是让 Deepseek 分析）