分类目录归档:离散数学

书面作业将引入人工智能技术来辅助评阅

熟悉我的同学们都知道,我是一个“系统狂魔”。平时没事的时候,我就喜欢写一些业务系统,来提升自己工作的效率。刚回到软件学院工作时,我花了大约半年的时间开发了KL平台,用于组织和管理我的教学过程。

近几年,人工智能,尤其是大语言模型,发展迅速。我也一直在思考:能否将它应用到我的教学中?学校也鼓励我们多加探索。不过,我的思路和多数老师有些不同。

很多老师设想的“AI 助教”,核心是基于检索增强生成的技术:先整理课程内容,构建知识库,再提供一个对话接口,让学生随时提问,由大语言模型结合知识库回答。

但我并不打算这么用。原因有两点:

第一,本科教学所涉及的基础知识,大语言模型已经掌握得非常好。大家在算法课上就能体会到,无论问题简单还是复杂,模型通常都能给出不错的答案。第二,从我的个人使用体验来看,模型厂商公开给用户使用的产品往往比开放出来的 API 更强大。

所以,如果学生在学习中遇到问题,他们更可能直接去问通用的大语言模型,而不是依赖老师自己开发的“AI 助教”。这一点在我的课堂上也有体现:学生们遇到问题时,大多会直接打开 ChatGPT 提问。于是,他们很快就“学会”了(这里加引号是因为,他们往往只是得到了正确答案,但未必真正理解)。更直观的例子是,KL 平台的讨论区里,关于课程和作业内容的讨论很少,大多数帖子是一些程序性问题,例如“考试能不能用计算器”、“这个题要不要写证明”、“老师,我的代码有一个隐藏样例过不了,能不能告诉我是哪一个?”——这些并不是 AI 助教能解决的。

因此,作为一个“懒人”,我思考的方向就变成了:如何利用大语言模型来减轻自己和助教的负担?这个暑假,我花了大量时间探索、设计并实现了一个自动评阅书面作业的系统。它能够根据我预设的参考答案和评分标准,对学生的作业打分并生成详细的评分理由。

得益于 KL 平台上已有的作业数据和评阅记录,我能够进行大量实验,反复调试,直到系统达到我满意的效果。目前,该系统已能较好地识别和评阅大部分作业题目,并且我已将它完整地集成进 KL 平台。

从 2025 年秋季学期开始,离散数学和算法设计与分析两门课程的书面作业,将先由自动评阅系统进行初评,再由助教人工复核,确保结果与参考答案和评分标准一致。

这样做的好处有:

  1. 减轻工作量,提升反馈质量:以往书面作业完全依赖人工评阅,助教的工作量非常大。为了快速完成批改,评语往往写得过于简略,学生有时并不清楚自己错在哪里。自动评阅系统的优势在于,它能不厌其烦地写出清晰、具体的反馈,帮助学生更好地理解问题。
  2. 统一评分尺度:人工评阅时,最棘手的问题是如何界定“扣多少分才合适”。比如同一个错误,我可能在前几份作业中扣一半分,但在后面看到类似错误时却扣掉全部分。为了保证一致性,我常常需要在评阅完成后再回头逐一检查,修正不一致之处,工作量非常大。自动评阅系统则能天然保证评分标准的一致性。

致同学们的几点提醒

为了让自动评阅系统在教学中发挥应有的作用,同时保证评分的公平与有效,我有以下几点呼吁:

  1. 答案要写得清晰、具体、完整:除非系统出现明显的事实性错误(例如把正确答案判错),否则我们不会修改评阅结果。换句话说,如果你的答案不够完整,系统可能会据此扣分,而我们在复核时也大概率会认可这一结果。请务必将答案写得条理清晰、逻辑完整。
  2. 作业必须有良好的排版:如果排版混乱,系统可能会直接判为错误,我们在复核时也会采纳这一意见,这么做的原因是,如果你考试的时候也让自己的卷面凌乱不堪,那么大概率你也是得不到这道题目的分数的。因此,请大家务必重视排版。我推荐使用LaTeX或Markdown来排版你的作业,这样不仅公式输入方便,而且效果更美观。

希望大家能够理解并配合,这样不仅能帮助我们更好地管理课程,也能让你们获得更清晰、详细的作业反馈。

该怎样理解“所有的A都是B”,“有的A是B”的谓词形式化?

本文章转载于教学平台讨论区,本学期结束后讨论区将关闭,来年新的学生无法从讨论区中看见本文章,故特此将该文章转载于博客。

各位同学,相信大家在今天的学习中可能被谓词的形式化给绕糊涂了,所以我想在这里再跟大家聊聊我们应该如何理解形如“所有的A都是B”和“有的A是B”的形式化。当然,你使用反义句去思考是一种方法,但是有没有什么语义上的理解方式能够让我们直接理解背后的原因呢?——答案是有的,请听我细细道来。

一、“所有的A都是B的形式化

首先我们先来看课本中的例子,在限制论域为全总个体域的前提下,我们是怎样形式化“所有的素数都是整数”的呢?答案是:

$$(\forall x)(Prime(x) \Rightarrow Integer(x))$$为什么这种形式化是对的,而不是课本上写出的反例\((\forall x)(Prime(x) \wedge Integer(x))\)?

我们可以从推理的角度来理解这个问题,首先,我们先来看命题“所有的素数都是整数”,这个命题显然是真命题,也就是说,由这句话形式化而得到的谓词公式的真值应该是真!

而题目中限定了论域是全总个体域,也就是说,\(x\)是包罗万象的,它可以是整数,也可以是小数,甚至不是个数,比如是个梨子、苹果、或者你们的老师我!

我们已经学了基本的量词消去规则,所以说,我们的答案的那个蕴涵式构成的谓词公式,可以写为:

$$(Prime(梨子) \Rightarrow Integer(梨子)) \wedge (Prime(2.5) \Rightarrow Integer(2.5)) \wedge \cdots \wedge (Prime(2) \Rightarrow Integer(2))$$也就是说我把论域里的每个元素都展开来写了(实际上我不能这么做,因为全总个体域不是可数无限集——你不能把每个小数都列出来)。

那么你看,我们答案给你的基于蕴涵式构成的谓词公式的真值是真的吧?

为什么是真的呢——因为合取式的每一项都是真的!即:\(Prime(梨子) \Rightarrow Integer(梨子)\)是真的(因为前提是假的),\(Prime(2.5) \Rightarrow Integer(2.5)\)也是真的(因为前提是假的),而当前提为真的时候,结论也一定是真的,例如\(Prime(2) \Rightarrow Integer(2)\)。

而如果我们使用反例,即合取式来构造形式化后的结果,那么我们把全称量词展开来,也就是说:

$$(Prime(梨子) \wedge Integer(梨子)) \wedge (Prime(2.5) \wedge Integer(2.5)) \wedge \cdots \wedge (Prime(2) \wedge Integer(2))$$这个式子的真值为假!因为\(Prime(梨子)\)是假的,所以合取了以后整个公式的真值一定为假!这与“所有的素数都是整数”的真值应当为真相矛盾!

所以对于这种情况,我们应该使用蕴涵式来构造谓词公式。

二、“有的A是B”的形式化

我们继续看课本上的例子——“有的素数是奇数”,正确答案是:

$$(\exists x)(Prime(x) \wedge Odd(x))$$首先我们还是先理解“有的素数是奇数”是真命题还是假命题,这个命题显然是真命题,因为素数3就是一个奇数

——你看,我为了像你证明这个以存在量词开头的命题是真命题,我采用的方法是找证据法!意思就是说,我找到了一个证据,它使得这个命题成立了!

对于全称量词引导的命题,我们如果要证明它成立不太容易,但是如果我们要反驳它,只需要找一个反例即可。而存在量词引导的命题,我们要证明它成立是比较简单的,只需要找证据,而如果要反驳它,则需要看每一个元素是不是都导致假命题,所以与全称量词引导的命题相反,反驳存在量词引导的命题是比较麻烦的。

那么问题来了,我们为了证明有的素数是奇数,你就必须给我找一个证据!

这个证据可不能瞎找,比如我给你的证据是3,这个证据是足以支撑这个命题成立的,但是如果我给你一个证据是4,这个证据是不能够证明出原命题成立的!

这是什么意思呢?——我给你的证据是3,我们代入形式化的命题公式,有\(Prime(3) \wedge Integer(3)\)为真——所以这个证据足以支撑了命题的成立,而如果我说我给你个证据是4,那么我们有\(Prime(4) \wedge Integer(4)\)为假(因为\(Prime(4)\)为假),所以4作为证据不能够支撑命题的成立!

那么我们再来看典型的反例,如果你把这个语句的形式化写为:

$$(\exists x)(Prime(x) \Rightarrow Odd(x))$$这时候,我跟你说,我证明出这个命题是成立的了!那么你就会问我,那你找到的是什么数啊?我说我找到了4,你跟我说这不是胡扯吗,4又不是素数,怎么可以作为这个命题成立的证据呢?那我紧接着说:“你把4代进去试试?”,你会发现\(Prime(4) \Rightarrow Odd(4)\)的真值居然是真的(因为前提\(Prime(4)\)是假的)——这说明这个形式化的公式是不正确的。

因此,我们当形式化形如“所有的A都是B”的语句的时候,应该采用蕴涵式来构建谓词公式,而形式化形如“有的A是B”的时候,应该采用合取词来构建谓词公式,希望上面的这些分析过程能够帮助你更好的理解自然语句的形式化。