#形式化方法
共 52 篇相关文章
·8 分钟
当世界运行在无人能懂的代码上：AI代码验证与形式化方法的未来
国际数学联盟《莱顿宣言》警告AI威胁代码可验证性。本文探讨AI生成代码与传统编译的本质区别，分析形式化方法如何为不可预测的AI输出提供可信边界，以及软件工程面临的信任危机与解决路径。
阅读全文 →
·12 分钟
LLM记忆系统如何演变为程序分析工具：一次意外的技术发现
一位开发者在为大语言模型构建记忆系统时，意外发现LLM记忆管理与程序分析的本质相通性。本文深入解析从依赖追踪到数据流分析的技术演化路径，探讨程序分析方法论如何提升AI Agent记忆基础设施的可靠性。
阅读全文 →
·13 分钟
AI自主数学发现：多智能体开放世界如何重塑科研范式
探讨多智能体开放世界环境中AI自主数学发现的新范式。从开放世界设定、多智能体协作机制到形式化验证，解析AI如何从解题工具进化为自主探索者，及其对未来科研的深远影响。
阅读全文 →
·12 分钟
Gemini决策闭合基准实测：285次运行99.3%通过率解读
一份聚焦LLM决策闭合能力的基准测试，285次实测中Gemini取得99.3%语义通过率。本文解析其方法论亮点：语义正确与格式合规的分离评分，以及冻结基准跨模型对比的实验设计。
阅读全文 →
·17 分钟
告别Vibe Coding：构建可靠的AI编程工作流
深入解析Vibe Coding的陷阱与局限，探讨如何通过测试驱动开发、代码审查和需求规格化等工程方法，构建可靠、可维护的AI编程工作流，让AI真正成为提升开发效率的利器。
阅读全文 →
·13 分钟
ProofRun：为AI编程代理提供本地验证回执
ProofRun为AI编程代理提供本地验证回执，解决AI代码生成的信任危机。通过在本地真实环境中独立验证AI的工作成果，实现可审计、可追溯、可复现的AI辅助开发，适用于团队协作、CI/CD流程和合规审计场景。
阅读全文 →
·9 分钟
GitHub热榜盘点：9个值得关注的AI开源新项目
盘点GitHub Trending热榜上9个值得关注的AI开源项目，涵盖14MB边缘小模型Needle、AI Agent协作工作空间Macro与OlaOS、规格驱动开发工具SpecKit等，深度解析端侧AI、Agent工程化与开发范式转变三大技术趋势。
阅读全文 →
·14 分钟
形式化验证的困境与出路：50年争论给工程师的启示
重新审视1979年DeMillo等人对形式化验证的经典批评，探讨Coq、TLA+等现代工具是否解决了规约正确性、社会过程等根本问题，分析类型系统、模型检查等折中路线为何成为主流。
阅读全文 →
·15 分钟
为AI生成的GPU内核构建合约级验证器：解决LLM代码信任难题
探讨如何通过合约级验证器验证LLM生成的GPU内核代码正确性，解决AI代码生成中的并行竞态、边界越界等信任问题，构建生成-验证-迭代的自动化工作流。
阅读全文 →
·12 分钟
警惕LLM测试帖背后的提示注入陷阱：一次社会工程学攻击解析
深度解析Reddit上一则伪装成LLM鲁棒性研究的提示注入攻击帖子，揭示其社会工程学手法，并提供从业者应对间接提示注入的安全防护建议。
阅读全文 →
·10 分钟
Mailüfterl：欧洲首台晶体管计算机的诞生与传奇
Mailüfterl是奥地利维也纳工业大学研制的欧洲大陆最早晶体管计算机之一。本文详述这台以"五月微风"命名的先驱设备的技术特点、研发历程及其设计者Heinz Zemanek的贡献，揭示被主流计算机史忽视的欧洲计算先驱故事。
阅读全文 →
·16 分钟
医疗AI安全架构：规则引擎与机器学习混合设计实践
探讨医疗AI领域中规则引擎与机器学习的混合架构设计，分析确定性规则引擎、约束满足问题(CSP)和评分机制如何在运动处方系统中保障安全底线，同时借助ML实现智能优化。
阅读全文 →
·7 分钟
Algebruh：用形式化验证工具交叉校验AI算术断言的可靠性
Algebruh是一个开源项目，集成Z3、cvc5和Lean三大形式化验证引擎，通过多引擎交叉验证来检测AI大语言模型输出的算术断言是否正确，为LLM幻觉问题提供确定性的纠错方案。
阅读全文 →
·14 分钟
AI迁移COBOL到Java：为何连Bug也一起搬过去了
AI代码迁移工具将遗留COBOL程序转换为Java时，连原始Bug也一并复制。本文深入分析行为等价迁移的技术困境、COBOL与Java的语义差异，以及人机协作迁移的最佳实践。
阅读全文 →
·14 分钟
从动力学到世界模型：一条自学AI数学路线图
一份从动力学系统、因果推断、状态空间模型到世界模型的自学路线图，拆解理解Dreamer、JEPA等前沿AI系统所需的核心数学基础与学习顺序。
阅读全文 →
·11 分钟
GenAI软件工程八大迷思破解：AI编程的真相与误区
深入剖析生成式AI在软件工程领域的八大常见误解，涵盖AI取代程序员、代码质量、生产力提升、安全合规等核心议题，帮助开发者理性看待AI编程工具的真实能力与局限。
阅读全文 →
·13 分钟
Cloudflare用AI落地工程标准化：从规范漂移到自动执行
深入解析Cloudflare如何利用大语言模型自动执行工程标准，解决大型团队规范漂移问题。探讨AI代码评审融入CI/CD流程的核心逻辑、落地挑战及对技术团队的启示。
阅读全文 →
·16 分钟
学术社区信噪比危机：会议季如何淹没技术讨论
当ARR和EMNLP投稿季帖子占据社区90%内容，技术讨论被严重稀释。本文分析NLP学术社区信噪比下降的结构性原因，探讨内容分流、标签过滤等社区治理方案，帮助从业者应对信息过载。
阅读全文 →
