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）是指通过输入文本描述，生成对应图像的技术。文生图的整体流程: 文本编码：将输入的文本描述转换为向量表示，捕捉语义信息。 噪声生成与扩散过程：通过逐步向图像添加噪声，训练模型学习如何逆转噪声过程生成清晰图像。 采样（生成）过程：利用训练好的模型，从随机噪声开始，逐步去噪，生成符合文本描述的图像。 图像解码：将模型生成的潜在空间表示解码为真实图像。 ...
1. 引言 在机器学习领域，梯度提升树（Gradient Boosting Tree）是一种非常强大的集成学习方法，而XGBoost（eXtreme Gradient Boosting）是梯度提升树的高效实现，因其速度快、性能优异而广受欢迎，广泛应用于分类、回归、排序等任务。 ...
基础 定义 提示工程PE（Prompt Engineering）是利用自然语言处理技术，通过优化提示词（Prompt），来提高模型性能和效果的一种技术。 ...
基础 OpenManus是Manus的一套开源实现。 Hello, Manus 模型配置, 在目录config下面复制config.example.toml改名为config.toml, 然后更新模型配置信息。以使用qwen模型为例: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 # Global LLM configuration [llm] model = "qwq-plus" # The LLM model to use base_url = "https://dashscope.aliyuncs.com/compatible-mode/v1" # API endpoint URL api_key = "sk-xxxxx" # Your API key max_tokens = 8192 # Maximum number of tokens in the response temperature = 0.0 # Controls randomness # Optional configuration for specific LLM models [llm.vision] model = "qwen-vl-max" # The vision model to use base_url = "https://dashscope.aliyuncs.com/compatible-mode/v1" # API endpoint URL for vision model api_key = "sk-xxxx" # Your API key for vision model max_tokens = 8192 # Maximum number of tokens in the response temperature = 0.0 # Controls randomness for vision model 结合MCP OpenManus MCP 架构设计 MCP 主机及客户端（MCPAgent） OpenManus 中 MCP 主机及客户端相关的实现位于app/agent/mcp_agent.py和app/tool/mcp.py ...
基础 OpenAI Python库是OpenAI官方提供的开发工具包，旨在帮助开发者快速集成GPT系列模型、DALL·E图像生成等AI能力。截至2025年3月，该库已迭代至v2.x版本，支持同步/异步调用、流式响应等特性，并新增了Agent开发工具链。 ...