AI

GitHub Spec Kit：开启规范驱动开发新时代 概述 GitHub Spec Kit 是 GitHub 开源的一款革命性开发工具包，它彻底改变了传统的软件开发流程。不同于传统的"先编码后文档"模式，Spec Kit 采用"规范驱动开发"（Spec-Driven Development）理念，让规范成为可执行的代码，直接生成工作实现，而不仅仅是指导开发。 ...

概述 KouriChat是一个虚拟角色聊天软件，微信无缝接入（支持群聊），支持： 智能对话分段 & 情感化表情包 图像生成 & 图片识别（Kimi集成） 语音消息 & 持久记忆存储 代码结构解析 核心入口是src/main.py, 其中包含了处理私聊和处理群聊的机器人，这里只分析处理私聊的机器人, 对应类是PrivateChatBot.这其中分别初始化 ...

概述 随着人工智能和自然语言处理（NLP）的快速发展，Embedding Model（嵌入模型）已成为理解和处理文本、图像、音频等数据的核心技术之一。 ...

概述 完整的Transformer包含Embeddings、Positional encoding、AddNormal、MultiHeadAttention、DecoderLayer、attention、FeedForward、EncoderLayer等多个部分。 ...

Lean4：定理证明与函数式编程的完美融合 Lean4是一款由微软研究院开发的定理证明器和通用函数式编程语言，它结合了形式化数学证明的强大功能与现代编程语言的实用特性。作为交互式定理证明器(Interactive Theorem Prover, ITP)，Lean4允许数学家和研究者将数学定理转换为可验证的代码形式，确保证明的绝对正确性。同时，作为编程语言，它支持函数式编程范式、依赖类型系统和元编程能力，使开发者能够编写高效且类型安全的代码。Lean4以其强大的类型系统、丰富的数学库Mathlib4（已超过150万行代码）以及与Rust类似的工具链管理（elan、lake）而脱颖而出，正成为数学形式化和程序验证领域的主流工具。 ...

0. 引言 视频创作工作流 AI视频创作的工作流通常流程为： 分镜剧本 分镜画面：剧本视觉化，用AI生成分镜静态图 分镜视频：用AI生成分镜镜头片段 背景音乐&音效 剪辑合成 入门 AI视频的基础是生成画面和分镜视频。 ...

0. 引言 微调是指在预训练模型的基础上，使用少量的标注数据对模型进行微调，以提高模型在特定任务上的性能。 常见的需要进行微调的原因： LLM在特定任务上的性能还需要微调来提升: 通用模型训练数据覆盖面广，但难以深入垂直领域的知识体系和专业术语，例如医学争端需要理解病理特征、法律咨询需要熟悉法条逻辑；当模型在专业领域知识不够时会有明显的幻觉。 让模型掌握”特定风格“: 例如训练模型以幽默风格撰写广告文案、心理咨询场景需要调整输出为引导性提问还不是结论性的判断 长上下文 vs 知识库 vs 微调 长文本表示模型可以处理很长的文本内容理解，其优点是： ...

0. 引言 LangChain实现了大型语言模型及相关技术（例如嵌入模型embedding model和向量存储vector）的标准接口, 并提供与数百种模型、技术方案的集成。

0. 引言 基础的树模型主要包含： 决策树（Decision Tree） 随机森林（Random Forest） 梯度提升树（Gradient Boosting Trees） 1. 决策树（Decision Tree） 1.1 算法原理 决策树是一种树形结构的分类和回归模型，通过对数据特征进行条件判断，将数据划分成不同的区域。树的每个节点代表一个特征的判断条件，叶子节点代表最终的类别或预测值。 ...

文生图/图生图基本原理 基础 AI 文生图（Text-to-Image Generation）是指通过输入文本描述，生成对应图像的技术。文生图的整体流程: 文本编码：将输入的文本描述转换为向量表示，捕捉语义信息。 噪声生成与扩散过程：通过逐步向图像添加噪声，训练模型学习如何逆转噪声过程生成清晰图像。 采样（生成）过程：利用训练好的模型，从随机噪声开始，逐步去噪，生成符合文本描述的图像。 图像解码：将模型生成的潜在空间表示解码为真实图像。 ...