Harmonic, công ty khởi nghiệp AI của CEO Robinhood, mở rộng Aristotle sang xác minh thiết kế phần mềm và chip

Harmonic, công ty khởi nghiệp AI do Giám đốc điều hành Robinhood Vlad Tenev đồng sáng lập, cho biết hôm thứ Ba rằng họ đang mở rộng mô hình Aristotle của mình từ chứng minh toán học sang xác minh thiết kế phần mềm và chip, Reuters đưa tin. Động thái này diễn ra khi việc sử dụng AI ngày càng tăng trong việc phát hiện các lỗi phần mềm đang thu hút sự giám sát chặt chẽ hơn.

Từ chứng minh toán học đến mã

Harmonic cho biết Aristotle giờ đây có thể xác minh phần mềm viết bằng C và thiết kế chip viết bằng Verilog. Công ty mô tả mục tiêu của mình là siêu trí tuệ toán học: một hệ thống AI tập trung vào lý luận nhằm giảm ảo giác và sai sót thực tế.

Reuters lưu ý rằng các nhà nghiên cứu gần đây đã sử dụng loại công nghệ này để phát hiện ra các lỗi nghiêm trọng trong PHP, khiến toàn cầu phải gấp rút vá chúng. Phát hiện các khiếm khuyết ở giai đoạn thiết kế bằng kiểm tra toán học thay vì chỉ kiểm tra là thị trường mà Harmonic muốn phục vụ.

Một trường hợp hợp nhất kéo dài bốn giờ

Harmonic chỉ vào phòng thí nghiệm nhiệt hạch DIII-D của Hoa Kỳ, nơi họ cho biết đã sử dụng Aristotle để xây dựng lại một phần phần mềm điều khiển lò phản ứng của mình trong bốn giờ, từ một bài nghiên cứu và một lời nhắc dài 254 từ. Ví dụ này nhằm thể hiện một mô hình suy luận không chỉ viết mã mà còn kiểm tra nó theo đặc tả.

Bối cảnh và những gì nên xem

Harmonic đã huy động được 120 triệu USD vào tháng 11 năm ngoái với mức định giá 1,45 tỷ USD, được hỗ trợ bởi công ty liên doanh của Nvidia, Sequoia và Ribbit Capital. Báo cáo không đề cập đến nguồn tài trợ mới hoặc khách hàng mới gắn liền với việc mở rộng này. Điều quan trọng tiếp theo là liệu các công cụ xác minh có chuyển từ trình diễn nghiên cứu sang công việc phát triển hàng ngày của các công ty phần mềm và chip hay không và liệu khách hàng có trả tiền cho sự chắc chắn bổ sung đó hay không.